Normed groups homomorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file gathers definitions and elementary constructions about bounded group homomorphisms between normed (abelian) groups (abbreviated to "normed group homs").
The main lemmas relate the boundedness condition to continuity and Lipschitzness.
The main construction is to endow the type of normed group homs between two given normed groups with a group structure and a norm, giving rise to a normed group structure. We provide several simple constructions for normed group homs, like kernel, range and equalizer.
Some easy other constructions are related to subgroups of normed groups.
Since a lot of elementary properties don't require ‖x‖ = 0 → x = 0 we start setting up the
theory of seminormed_add_group_hom and we specialize to normed_add_group_hom when needed.
structure
normed_add_group_hom
(V : Type u_1)
(W : Type u_2)
[seminormed_add_comm_group V]
[seminormed_add_comm_group W] :
Type (max u_1 u_2)
- to_fun : V → W
- map_add' : ∀ (v₁ v₂ : V), self.to_fun (v₁ + v₂) = self.to_fun v₁ + self.to_fun v₂
- bound' : ∃ (C : ℝ), ∀ (v : V), ‖self.to_fun v‖ ≤ C * ‖v‖
A morphism of seminormed abelian groups is a bounded group homomorphism.
Instances for normed_add_group_hom
- normed_add_group_hom.has_sizeof_inst
- normed_add_group_hom.has_coe_to_fun
- normed_add_group_hom.add_monoid_hom_class
- normed_add_group_hom.has_op_norm
- normed_add_group_hom.has_add
- normed_add_group_hom.has_zero
- normed_add_group_hom.inhabited
- normed_add_group_hom.has_neg
- normed_add_group_hom.has_sub
- normed_add_group_hom.has_smul
- normed_add_group_hom.smul_comm_class
- normed_add_group_hom.is_scalar_tower
- normed_add_group_hom.is_central_scalar
- normed_add_group_hom.has_nat_scalar
- normed_add_group_hom.has_int_scalar
- normed_add_group_hom.add_comm_group
- normed_add_group_hom.to_seminormed_add_comm_group
- normed_add_group_hom.to_normed_add_comm_group
- normed_add_group_hom.distrib_mul_action
- normed_add_group_hom.module
def
add_monoid_hom.mk_normed_add_group_hom
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
(f : V →+ W)
(C : ℝ)
(h : ∀ (v : V), ‖⇑f v‖ ≤ C * ‖v‖) :
Associate to a group homomorphism a bounded group homomorphism under a norm control condition.
See add_monoid_hom.mk_normed_add_group_hom' for a version that uses ℝ≥0 for the bound.
def
add_monoid_hom.mk_normed_add_group_hom'
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
(f : V →+ W)
(C : nnreal)
(hC : ∀ (x : V), ‖⇑f x‖₊ ≤ C * ‖x‖₊) :
Associate to a group homomorphism a bounded group homomorphism under a norm control condition.
See add_monoid_hom.mk_normed_add_group_hom for a version that uses ℝ for the bound.
@[protected, instance]
def
normed_add_group_hom.has_coe_to_fun
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_coe_to_fun (normed_add_group_hom V₁ V₂) (λ (_x : normed_add_group_hom V₁ V₂), V₁ → V₂)
Equations
theorem
normed_add_group_hom.coe_inj
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f g : normed_add_group_hom V₁ V₂}
(H : ⇑f = ⇑g) :
f = g
theorem
normed_add_group_hom.coe_injective
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
theorem
normed_add_group_hom.coe_inj_iff
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f g : normed_add_group_hom V₁ V₂} :
@[ext]
theorem
normed_add_group_hom.ext
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f g : normed_add_group_hom V₁ V₂}
(H : ∀ (x : V₁), ⇑f x = ⇑g x) :
f = g
theorem
normed_add_group_hom.ext_iff
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f g : normed_add_group_hom V₁ V₂} :
@[simp]
theorem
normed_add_group_hom.to_fun_eq_coe
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
@[simp]
@[simp]
theorem
normed_add_group_hom.coe_mk_normed_add_group_hom
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : V₁ →+ V₂)
(C : ℝ)
(hC : ∀ (v : V₁), ‖⇑f v‖ ≤ C * ‖v‖) :
⇑(f.mk_normed_add_group_hom C hC) = ⇑f
@[simp]
theorem
normed_add_group_hom.coe_mk_normed_add_group_hom'
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : V₁ →+ V₂)
(C : nnreal)
(hC : ∀ (x : V₁), ‖⇑f x‖₊ ≤ C * ‖x‖₊) :
⇑(f.mk_normed_add_group_hom' C hC) = ⇑f
def
normed_add_group_hom.to_add_monoid_hom
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
V₁ →+ V₂
The group homomorphism underlying a bounded group homomorphism.
Equations
@[simp]
theorem
normed_add_group_hom.coe_to_add_monoid_hom
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
⇑(f.to_add_monoid_hom) = ⇑f
theorem
normed_add_group_hom.to_add_monoid_hom_injective
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
@[simp]
theorem
normed_add_group_hom.mk_to_add_monoid_hom
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : V₁ → V₂)
(h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂)
(h₂ : ∃ (C : ℝ), ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖) :
{to_fun := f, map_add' := h₁, bound' := h₂}.to_add_monoid_hom = add_monoid_hom.mk' f h₁
@[protected, instance]
def
normed_add_group_hom.add_monoid_hom_class
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
add_monoid_hom_class (normed_add_group_hom V₁ V₂) V₁ V₂
Equations
- normed_add_group_hom.add_monoid_hom_class = {coe := coe_fn normed_add_group_hom.has_coe_to_fun, coe_injective' := _, map_add := _, map_zero := _}
theorem
normed_add_group_hom.bound
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.antilipschitz_of_norm_ge
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
{K : nnreal}
(h : ∀ (x : V₁), ‖x‖ ≤ ↑K * ‖⇑f x‖) :
def
normed_add_group_hom.surjective_on_with
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
(K : add_subgroup V₂)
(C : ℝ) :
Prop
A normed group hom is surjective on the subgroup K with constant C if every element
x of K has a preimage whose norm is bounded above by C*‖x‖. This is a more
abstract version of f having a right inverse defined on K with operator norm
at most C.
theorem
normed_add_group_hom.surjective_on_with.mono
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f : normed_add_group_hom V₁ V₂}
{K : add_subgroup V₂}
{C C' : ℝ}
(h : f.surjective_on_with K C)
(H : C ≤ C') :
f.surjective_on_with K C'
theorem
normed_add_group_hom.surjective_on_with.exists_pos
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f : normed_add_group_hom V₁ V₂}
{K : add_subgroup V₂}
{C : ℝ}
(h : f.surjective_on_with K C) :
∃ (C' : ℝ) (H : C' > 0), f.surjective_on_with K C'
theorem
normed_add_group_hom.surjective_on_with.surj_on
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f : normed_add_group_hom V₁ V₂}
{K : add_subgroup V₂}
{C : ℝ}
(h : f.surjective_on_with K C) :
The operator norm #
noncomputable
def
normed_add_group_hom.op_norm
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
The operator norm of a seminormed group homomorphism is the inf of all its bounds.
@[protected, instance]
noncomputable
def
normed_add_group_hom.has_op_norm
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_norm (normed_add_group_hom V₁ V₂)
Equations
theorem
normed_add_group_hom.norm_def
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.bounds_bdd_below
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f : normed_add_group_hom V₁ V₂} :
theorem
normed_add_group_hom.op_norm_nonneg
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.le_op_norm
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
(x : V₁) :
The fundamental property of the operator norm: ‖f x‖ ≤ ‖f‖ * ‖x‖.
theorem
normed_add_group_hom.le_op_norm_of_le
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
{c : ℝ}
{x : V₁}
(h : ‖x‖ ≤ c) :
theorem
normed_add_group_hom.le_of_op_norm_le
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
{c : ℝ}
(h : ‖f‖ ≤ c)
(x : V₁) :
theorem
normed_add_group_hom.lipschitz
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
lipschitz_with ⟨‖f‖, _⟩ ⇑f
continuous linear maps are Lipschitz continuous.
@[protected]
theorem
normed_add_group_hom.uniform_continuous
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
@[protected, continuity]
theorem
normed_add_group_hom.continuous
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.ratio_le_op_norm
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
(x : V₁) :
theorem
normed_add_group_hom.op_norm_le_bound
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
{M : ℝ}
(hMp : 0 ≤ M)
(hM : ∀ (x : V₁), ‖⇑f x‖ ≤ M * ‖x‖) :
If one controls the norm of every f x, then one controls the norm of f.
theorem
normed_add_group_hom.op_norm_eq_of_bounds
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
{M : ℝ}
(M_nonneg : 0 ≤ M)
(h_above : ∀ (x : V₁), ‖⇑f x‖ ≤ M * ‖x‖)
(h_below : ∀ (N : ℝ), N ≥ 0 → (∀ (x : V₁), ‖⇑f x‖ ≤ N * ‖x‖) → M ≤ N) :
theorem
normed_add_group_hom.op_norm_le_of_lipschitz
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f : normed_add_group_hom V₁ V₂}
{K : nnreal}
(hf : lipschitz_with K ⇑f) :
theorem
normed_add_group_hom.mk_normed_add_group_hom_norm_le
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : V₁ →+ V₂)
{C : ℝ}
(hC : 0 ≤ C)
(h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :
‖f.mk_normed_add_group_hom C h‖ ≤ C
If a bounded group homomorphism map is constructed from a group homomorphism via the constructor
mk_normed_add_group_hom, then its norm is bounded by the bound given to the constructor if it is
nonnegative.
theorem
normed_add_group_hom.mk_normed_add_group_hom_norm_le'
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : V₁ →+ V₂)
{C : ℝ}
(h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :
‖f.mk_normed_add_group_hom C h‖ ≤ linear_order.max C 0
If a bounded group homomorphism map is constructed from a group homomorphism
via the constructor mk_normed_add_group_hom, then its norm is bounded by the bound
given to the constructor or zero if this bound is negative.
theorem
add_monoid_hom.mk_normed_add_group_hom_norm_le
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : V₁ →+ V₂)
{C : ℝ}
(hC : 0 ≤ C)
(h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :
‖f.mk_normed_add_group_hom C h‖ ≤ C
Alias of normed_add_group_hom.mk_normed_add_group_hom_norm_le.
theorem
add_monoid_hom.mk_normed_add_group_hom_norm_le'
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : V₁ →+ V₂)
{C : ℝ}
(h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :
‖f.mk_normed_add_group_hom C h‖ ≤ linear_order.max C 0
Alias of normed_add_group_hom.mk_normed_add_group_hom_norm_le'.
Addition of normed group homs #
@[protected, instance]
noncomputable
def
normed_add_group_hom.has_add
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_add (normed_add_group_hom V₁ V₂)
Addition of normed group homs.
Equations
- normed_add_group_hom.has_add = {add := λ (f g : normed_add_group_hom V₁ V₂), (f.to_add_monoid_hom + g.to_add_monoid_hom).mk_normed_add_group_hom (‖f‖ + ‖g‖) _}
theorem
normed_add_group_hom.op_norm_add_le
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f g : normed_add_group_hom V₁ V₂) :
The operator norm satisfies the triangle inequality.
Terms containing @has_add.add (has_coe_to_fun.F ...) pi.has_add
seem to cause leanchecker to crash due to an out-of-memory
condition.
As a workaround, we add a type annotation: (f + g : V₁ → V₂)
@[simp]
theorem
normed_add_group_hom.coe_add
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f g : normed_add_group_hom V₁ V₂) :
@[simp]
theorem
normed_add_group_hom.add_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f g : normed_add_group_hom V₁ V₂)
(v : V₁) :
The zero normed group hom #
@[protected, instance]
def
normed_add_group_hom.has_zero
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_zero (normed_add_group_hom V₁ V₂)
Equations
- normed_add_group_hom.has_zero = {zero := 0.mk_normed_add_group_hom 0 normed_add_group_hom.has_zero._proof_1}
@[protected, instance]
def
normed_add_group_hom.inhabited
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
inhabited (normed_add_group_hom V₁ V₂)
Equations
theorem
normed_add_group_hom.op_norm_zero
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
The norm of the 0 operator is 0.
theorem
normed_add_group_hom.op_norm_zero_iff
{V₁ : Type u_1}
{V₂ : Type u_2}
[normed_add_comm_group V₁]
[normed_add_comm_group V₂]
{f : normed_add_group_hom V₁ V₂} :
For normed groups, an operator is zero iff its norm vanishes.
@[simp]
theorem
normed_add_group_hom.coe_zero
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
@[simp]
theorem
normed_add_group_hom.zero_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(v : V₁) :
The identity normed group hom #
@[simp]
theorem
normed_add_group_hom.id_apply
(V : Type u_1)
[seminormed_add_comm_group V]
(ᾰ : V) :
⇑(normed_add_group_hom.id V) ᾰ = ᾰ
The identity as a continuous normed group hom.
Equations
The norm of the identity is at most 1. It is in fact 1, except when the norm of every
element vanishes, where it is 0. (Since we are working with seminorms this can happen even if the
space is non-trivial.) It means that one can not do better than an inequality in general.
theorem
normed_add_group_hom.norm_id_of_nontrivial_seminorm
(V : Type u_1)
[seminormed_add_comm_group V]
(h : ∃ (x : V), ‖x‖ ≠ 0) :
If there is an element with norm different from 0, then the norm of the identity equals 1.
(Since we are working with seminorms supposing that the space is non-trivial is not enough.)
If a normed space is non-trivial, then the norm of the identity equals 1.
The negation of a normed group hom #
@[protected, instance]
noncomputable
def
normed_add_group_hom.has_neg
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_neg (normed_add_group_hom V₁ V₂)
Opposite of a normed group hom.
Equations
- normed_add_group_hom.has_neg = {neg := λ (f : normed_add_group_hom V₁ V₂), (-f.to_add_monoid_hom).mk_normed_add_group_hom ‖f‖ _}
@[simp]
theorem
normed_add_group_hom.coe_neg
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
@[simp]
theorem
normed_add_group_hom.neg_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
(v : V₁) :
theorem
normed_add_group_hom.op_norm_neg
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
Subtraction of normed group homs #
@[protected, instance]
def
normed_add_group_hom.has_sub
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_sub (normed_add_group_hom V₁ V₂)
Subtraction of normed group homs.
Equations
- normed_add_group_hom.has_sub = {sub := λ (f g : normed_add_group_hom V₁ V₂), {to_fun := (f.to_add_monoid_hom - g.to_add_monoid_hom).to_fun, map_add' := _, bound' := _}}
@[simp]
theorem
normed_add_group_hom.coe_sub
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f g : normed_add_group_hom V₁ V₂) :
@[simp]
theorem
normed_add_group_hom.sub_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f g : normed_add_group_hom V₁ V₂)
(v : V₁) :
Scalar actions on normed group homs #
@[protected, instance]
def
normed_add_group_hom.has_smul
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_5}
[monoid_with_zero R]
[distrib_mul_action R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂] :
has_smul R (normed_add_group_hom V₁ V₂)
@[simp]
theorem
normed_add_group_hom.coe_smul
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_5}
[monoid_with_zero R]
[distrib_mul_action R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂]
(r : R)
(f : normed_add_group_hom V₁ V₂) :
@[simp]
theorem
normed_add_group_hom.smul_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_5}
[monoid_with_zero R]
[distrib_mul_action R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂]
(r : R)
(f : normed_add_group_hom V₁ V₂)
(v : V₁) :
@[protected, instance]
def
normed_add_group_hom.smul_comm_class
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_5}
{R' : Type u_6}
[monoid_with_zero R]
[distrib_mul_action R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂]
[monoid_with_zero R']
[distrib_mul_action R' V₂]
[pseudo_metric_space R']
[has_bounded_smul R' V₂]
[smul_comm_class R R' V₂] :
smul_comm_class R R' (normed_add_group_hom V₁ V₂)
@[protected, instance]
def
normed_add_group_hom.is_scalar_tower
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_5}
{R' : Type u_6}
[monoid_with_zero R]
[distrib_mul_action R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂]
[monoid_with_zero R']
[distrib_mul_action R' V₂]
[pseudo_metric_space R']
[has_bounded_smul R' V₂]
[has_smul R R']
[is_scalar_tower R R' V₂] :
is_scalar_tower R R' (normed_add_group_hom V₁ V₂)
@[protected, instance]
def
normed_add_group_hom.is_central_scalar
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_5}
[monoid_with_zero R]
[distrib_mul_action R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂]
[distrib_mul_action Rᵐᵒᵖ V₂]
[is_central_scalar R V₂] :
is_central_scalar R (normed_add_group_hom V₁ V₂)
@[protected, instance]
def
normed_add_group_hom.has_nat_scalar
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_smul ℕ (normed_add_group_hom V₁ V₂)
@[simp]
theorem
normed_add_group_hom.coe_nsmul
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(r : ℕ)
(f : normed_add_group_hom V₁ V₂) :
@[simp]
theorem
normed_add_group_hom.nsmul_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(r : ℕ)
(f : normed_add_group_hom V₁ V₂)
(v : V₁) :
@[protected, instance]
def
normed_add_group_hom.has_int_scalar
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
has_smul ℤ (normed_add_group_hom V₁ V₂)
@[simp]
theorem
normed_add_group_hom.coe_zsmul
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(r : ℤ)
(f : normed_add_group_hom V₁ V₂) :
@[simp]
theorem
normed_add_group_hom.zsmul_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(r : ℤ)
(f : normed_add_group_hom V₁ V₂)
(v : V₁) :
Normed group structure on normed group homs #
@[protected, instance]
noncomputable
def
normed_add_group_hom.add_comm_group
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
add_comm_group (normed_add_group_hom V₁ V₂)
Homs between two given normed groups form a commutative additive group.
Equations
- normed_add_group_hom.add_comm_group = function.injective.add_comm_group coe_fn normed_add_group_hom.coe_injective normed_add_group_hom.add_comm_group._proof_1 normed_add_group_hom.add_comm_group._proof_2 normed_add_group_hom.add_comm_group._proof_3 normed_add_group_hom.add_comm_group._proof_4 normed_add_group_hom.add_comm_group._proof_5 normed_add_group_hom.add_comm_group._proof_6
@[protected, instance]
noncomputable
def
normed_add_group_hom.to_seminormed_add_comm_group
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
Normed group homomorphisms themselves form a seminormed group with respect to the operator norm.
Equations
- normed_add_group_hom.to_seminormed_add_comm_group = {to_fun := normed_add_group_hom.op_norm _inst_3, map_zero' := _, add_le' := _, neg' := _}.to_seminormed_add_comm_group
@[protected, instance]
noncomputable
def
normed_add_group_hom.to_normed_add_comm_group
{V₁ : Type u_1}
{V₂ : Type u_2}
[normed_add_comm_group V₁]
[normed_add_comm_group V₂] :
Normed group homomorphisms themselves form a normed group with respect to the operator norm.
def
normed_add_group_hom.coe_fn_add_hom
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
normed_add_group_hom V₁ V₂ →+ V₁ → V₂
Coercion of a normed_add_group_hom is an add_monoid_hom. Similar to add_monoid_hom.coe_fn.
Equations
@[simp]
theorem
normed_add_group_hom.coe_fn_add_hom_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(x : normed_add_group_hom V₁ V₂)
(ᾰ : V₁) :
@[simp]
theorem
normed_add_group_hom.coe_sum
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{ι : Type u_1}
(s : finset ι)
(f : ι → normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.sum_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{ι : Type u_1}
(s : finset ι)
(f : ι → normed_add_group_hom V₁ V₂)
(v : V₁) :
Module structure on normed group homs #
@[protected, instance]
noncomputable
def
normed_add_group_hom.distrib_mul_action
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_1}
[monoid_with_zero R]
[distrib_mul_action R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂] :
distrib_mul_action R (normed_add_group_hom V₁ V₂)
@[protected, instance]
noncomputable
def
normed_add_group_hom.module
{V₁ : Type u_2}
{V₂ : Type u_3}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{R : Type u_1}
[semiring R]
[module R V₂]
[pseudo_metric_space R]
[has_bounded_smul R V₂] :
module R (normed_add_group_hom V₁ V₂)
Equations
- normed_add_group_hom.module = function.injective.module R normed_add_group_hom.coe_fn_add_hom normed_add_group_hom.coe_injective normed_add_group_hom.module._proof_1
Composition of normed group homs #
@[protected]
noncomputable
def
normed_add_group_hom.comp
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(g : normed_add_group_hom V₂ V₃)
(f : normed_add_group_hom V₁ V₂) :
normed_add_group_hom V₁ V₃
The composition of continuous normed group homs.
Equations
- g.comp f = (g.to_add_monoid_hom.comp f.to_add_monoid_hom).mk_normed_add_group_hom (‖g‖ * ‖f‖) _
@[simp]
theorem
normed_add_group_hom.comp_apply
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(g : normed_add_group_hom V₂ V₃)
(f : normed_add_group_hom V₁ V₂)
(ᾰ : V₁) :
theorem
normed_add_group_hom.norm_comp_le
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(g : normed_add_group_hom V₂ V₃)
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.norm_comp_le_of_le
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
{f : normed_add_group_hom V₁ V₂}
{g : normed_add_group_hom V₂ V₃}
{C₁ C₂ : ℝ}
(hg : ‖g‖ ≤ C₂)
(hf : ‖f‖ ≤ C₁) :
theorem
normed_add_group_hom.norm_comp_le_of_le'
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
{f : normed_add_group_hom V₁ V₂}
{g : normed_add_group_hom V₂ V₃}
(C₁ C₂ C₃ : ℝ)
(h : C₃ = C₂ * C₁)
(hg : ‖g‖ ≤ C₂)
(hf : ‖f‖ ≤ C₁) :
noncomputable
def
normed_add_group_hom.comp_hom
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃] :
normed_add_group_hom V₂ V₃ →+ normed_add_group_hom V₁ V₂ →+ normed_add_group_hom V₁ V₃
Composition of normed groups hom as an additive group morphism.
Equations
- normed_add_group_hom.comp_hom = add_monoid_hom.mk' (λ (g : normed_add_group_hom V₂ V₃), add_monoid_hom.mk' (λ (f : normed_add_group_hom V₁ V₂), g.comp f) _) normed_add_group_hom.comp_hom._proof_2
@[simp]
theorem
normed_add_group_hom.comp_zero
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(f : normed_add_group_hom V₂ V₃) :
@[simp]
theorem
normed_add_group_hom.zero_comp
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.comp_assoc
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
{V₄ : Type u_1}
[seminormed_add_comm_group V₄]
(h : normed_add_group_hom V₃ V₄)
(g : normed_add_group_hom V₂ V₃)
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.coe_comp
{V₁ : Type u_2}
{V₂ : Type u_3}
{V₃ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(f : normed_add_group_hom V₁ V₂)
(g : normed_add_group_hom V₂ V₃) :
The inclusion of an add_subgroup, as bounded group homomorphism.
Equations
- normed_add_group_hom.incl s = {to_fun := coe coe_to_lift, map_add' := _, bound' := _}
@[simp]
theorem
normed_add_group_hom.incl_apply
{V : Type u_1}
[seminormed_add_comm_group V]
(s : add_subgroup V)
(ᾰ : ↥s) :
⇑(normed_add_group_hom.incl s) ᾰ = ↑ᾰ
theorem
normed_add_group_hom.norm_incl
{V : Type u_1}
[seminormed_add_comm_group V]
{V' : add_subgroup V}
(x : ↥V') :
Kernel #
def
normed_add_group_hom.ker
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
add_subgroup V₁
The kernel of a bounded group homomorphism. Naturally endowed with a
seminormed_add_comm_group instance.
Equations
- f.ker = f.to_add_monoid_hom.ker
theorem
normed_add_group_hom.mem_ker
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
(v : V₁) :
@[simp]
theorem
normed_add_group_hom.ker.lift_apply_coe
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(f : normed_add_group_hom V₁ V₂)
(g : normed_add_group_hom V₂ V₃)
(h : g.comp f = 0)
(v : V₁) :
↑(⇑(normed_add_group_hom.ker.lift f g h) v) = ⇑f v
def
normed_add_group_hom.ker.lift
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(f : normed_add_group_hom V₁ V₂)
(g : normed_add_group_hom V₂ V₃)
(h : g.comp f = 0) :
normed_add_group_hom V₁ ↥(g.ker)
Given a normed group hom f : V₁ → V₂ satisfying g.comp f = 0 for some g : V₂ → V₃,
the corestriction of f to the kernel of g.
@[simp]
theorem
normed_add_group_hom.ker.incl_comp_lift
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(f : normed_add_group_hom V₁ V₂)
(g : normed_add_group_hom V₂ V₃)
(h : g.comp f = 0) :
(normed_add_group_hom.incl g.ker).comp (normed_add_group_hom.ker.lift f g h) = f
@[simp]
theorem
normed_add_group_hom.ker_zero
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
theorem
normed_add_group_hom.coe_ker
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
theorem
normed_add_group_hom.is_closed_ker
{V₁ : Type u_3}
[seminormed_add_comm_group V₁]
{V₂ : Type u_1}
[normed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
Range #
def
normed_add_group_hom.range
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
add_subgroup V₂
The image of a bounded group homomorphism. Naturally endowed with a
seminormed_add_comm_group instance.
Equations
- f.range = f.to_add_monoid_hom.range
theorem
normed_add_group_hom.mem_range
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
(v : V₂) :
@[simp]
theorem
normed_add_group_hom.mem_range_self
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂)
(v : V₁) :
theorem
normed_add_group_hom.comp_range
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
(f : normed_add_group_hom V₁ V₂)
(g : normed_add_group_hom V₂ V₃) :
(g.comp f).range = add_subgroup.map g.to_add_monoid_hom f.range
theorem
normed_add_group_hom.incl_range
{V₁ : Type u_3}
[seminormed_add_comm_group V₁]
(s : add_subgroup V₁) :
(normed_add_group_hom.incl s).range = s
@[simp]
theorem
normed_add_group_hom.range_comp_incl_top
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
(f : normed_add_group_hom V₁ V₂) :
def
normed_add_group_hom.norm_noninc
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
(f : normed_add_group_hom V W) :
Prop
A normed_add_group_hom is norm-nonincreasing if ‖f v‖ ≤ ‖v‖ for all v.
theorem
normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
{f : normed_add_group_hom V W} :
f.norm_noninc ↔ ‖f‖ ≤ 1
theorem
normed_add_group_hom.norm_noninc.zero
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂] :
theorem
normed_add_group_hom.norm_noninc.comp
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
{g : normed_add_group_hom V₂ V₃}
{f : normed_add_group_hom V₁ V₂}
(hg : g.norm_noninc)
(hf : f.norm_noninc) :
(g.comp f).norm_noninc
@[simp]
theorem
normed_add_group_hom.norm_noninc.neg_iff
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{f : normed_add_group_hom V₁ V₂} :
(-f).norm_noninc ↔ f.norm_noninc
theorem
normed_add_group_hom.norm_eq_of_isometry
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
{f : normed_add_group_hom V W}
(hf : isometry ⇑f)
(v : V) :
theorem
normed_add_group_hom.isometry_comp
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
{g : normed_add_group_hom V₂ V₃}
{f : normed_add_group_hom V₁ V₂}
(hg : isometry ⇑g)
(hf : isometry ⇑f) :
theorem
normed_add_group_hom.norm_noninc_of_isometry
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
{f : normed_add_group_hom V W}
(hf : isometry ⇑f) :
def
normed_add_group_hom.equalizer
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
(f g : normed_add_group_hom V W) :
The equalizer of two morphisms f g : normed_add_group_hom V W.
def
normed_add_group_hom.equalizer.ι
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
(f g : normed_add_group_hom V W) :
normed_add_group_hom ↥(f.equalizer g) V
The inclusion of f.equalizer g as a normed_add_group_hom.
Equations
theorem
normed_add_group_hom.equalizer.comp_ι_eq
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
(f g : normed_add_group_hom V W) :
f.comp (normed_add_group_hom.equalizer.ι f g) = g.comp (normed_add_group_hom.equalizer.ι f g)
@[simp]
theorem
normed_add_group_hom.equalizer.lift_apply_coe
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W}
(φ : normed_add_group_hom V₁ V)
(h : f.comp φ = g.comp φ)
(v : V₁) :
↑(⇑(normed_add_group_hom.equalizer.lift φ h) v) = ⇑φ v
def
normed_add_group_hom.equalizer.lift
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W}
(φ : normed_add_group_hom V₁ V)
(h : f.comp φ = g.comp φ) :
normed_add_group_hom V₁ ↥(f.equalizer g)
If φ : normed_add_group_hom V₁ V is such that f.comp φ = g.comp φ, the induced morphism
normed_add_group_hom V₁ (f.equalizer g).
@[simp]
theorem
normed_add_group_hom.equalizer.ι_comp_lift
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W}
(φ : normed_add_group_hom V₁ V)
(h : f.comp φ = g.comp φ) :
noncomputable
def
normed_add_group_hom.equalizer.lift_equiv
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W} :
The lifting property of the equalizer as an equivalence.
Equations
- normed_add_group_hom.equalizer.lift_equiv = {to_fun := λ (φ : {φ // f.comp φ = g.comp φ}), normed_add_group_hom.equalizer.lift ↑φ _, inv_fun := λ (ψ : normed_add_group_hom V₁ ↥(f.equalizer g)), ⟨(normed_add_group_hom.equalizer.ι f g).comp ψ, _⟩, left_inv := _, right_inv := _}
@[simp]
theorem
normed_add_group_hom.equalizer.lift_equiv_symm_apply_coe
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W}
(ψ : normed_add_group_hom V₁ ↥(f.equalizer g)) :
@[simp]
theorem
normed_add_group_hom.equalizer.lift_equiv_apply
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W}
(φ : {φ // f.comp φ = g.comp φ}) :
noncomputable
def
normed_add_group_hom.equalizer.map
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{W₁ : Type u_6}
{W₂ : Type u_7}
[seminormed_add_comm_group W₁]
[seminormed_add_comm_group W₂]
{f₁ g₁ : normed_add_group_hom V₁ W₁}
{f₂ g₂ : normed_add_group_hom V₂ W₂}
(φ : normed_add_group_hom V₁ V₂)
(ψ : normed_add_group_hom W₁ W₂)
(hf : ψ.comp f₁ = f₂.comp φ)
(hg : ψ.comp g₁ = g₂.comp φ) :
normed_add_group_hom ↥(f₁.equalizer g₁) ↥(f₂.equalizer g₂)
Given φ : normed_add_group_hom V₁ V₂ and ψ : normed_add_group_hom W₁ W₂ such that
ψ.comp f₁ = f₂.comp φ and ψ.comp g₁ = g₂.comp φ, the induced morphism
normed_add_group_hom (f₁.equalizer g₁) (f₂.equalizer g₂).
Equations
- normed_add_group_hom.equalizer.map φ ψ hf hg = normed_add_group_hom.equalizer.lift (φ.comp (normed_add_group_hom.equalizer.ι f₁ g₁)) _
@[simp]
theorem
normed_add_group_hom.equalizer.ι_comp_map
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{W₁ : Type u_6}
{W₂ : Type u_7}
[seminormed_add_comm_group W₁]
[seminormed_add_comm_group W₂]
{f₁ g₁ : normed_add_group_hom V₁ W₁}
{f₂ g₂ : normed_add_group_hom V₂ W₂}
{φ : normed_add_group_hom V₁ V₂}
{ψ : normed_add_group_hom W₁ W₂}
(hf : ψ.comp f₁ = f₂.comp φ)
(hg : ψ.comp g₁ = g₂.comp φ) :
(normed_add_group_hom.equalizer.ι f₂ g₂).comp (normed_add_group_hom.equalizer.map φ ψ hf hg) = φ.comp (normed_add_group_hom.equalizer.ι f₁ g₁)
@[simp]
theorem
normed_add_group_hom.equalizer.map_id
{V₁ : Type u_3}
[seminormed_add_comm_group V₁]
{W₁ : Type u_6}
[seminormed_add_comm_group W₁]
{f₁ g₁ : normed_add_group_hom V₁ W₁} :
theorem
normed_add_group_hom.equalizer.comm_sq₂
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
{W₁ : Type u_6}
{W₂ : Type u_7}
{W₃ : Type u_8}
[seminormed_add_comm_group W₁]
[seminormed_add_comm_group W₂]
[seminormed_add_comm_group W₃]
{f₁ : normed_add_group_hom V₁ W₁}
{f₂ : normed_add_group_hom V₂ W₂}
{f₃ : normed_add_group_hom V₃ W₃}
{φ : normed_add_group_hom V₁ V₂}
{ψ : normed_add_group_hom W₁ W₂}
{φ' : normed_add_group_hom V₂ V₃}
{ψ' : normed_add_group_hom W₂ W₃}
(hf : ψ.comp f₁ = f₂.comp φ)
(hf' : ψ'.comp f₂ = f₃.comp φ') :
theorem
normed_add_group_hom.equalizer.map_comp_map
{V₁ : Type u_3}
{V₂ : Type u_4}
{V₃ : Type u_5}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
[seminormed_add_comm_group V₃]
{W₁ : Type u_6}
{W₂ : Type u_7}
{W₃ : Type u_8}
[seminormed_add_comm_group W₁]
[seminormed_add_comm_group W₂]
[seminormed_add_comm_group W₃]
{f₁ g₁ : normed_add_group_hom V₁ W₁}
{f₂ g₂ : normed_add_group_hom V₂ W₂}
{f₃ g₃ : normed_add_group_hom V₃ W₃}
{φ : normed_add_group_hom V₁ V₂}
{ψ : normed_add_group_hom W₁ W₂}
{φ' : normed_add_group_hom V₂ V₃}
{ψ' : normed_add_group_hom W₂ W₃}
(hf : ψ.comp f₁ = f₂.comp φ)
(hg : ψ.comp g₁ = g₂.comp φ)
(hf' : ψ'.comp f₂ = f₃.comp φ')
(hg' : ψ'.comp g₂ = g₃.comp φ') :
(normed_add_group_hom.equalizer.map φ' ψ' hf' hg').comp (normed_add_group_hom.equalizer.map φ ψ hf hg) = normed_add_group_hom.equalizer.map (φ'.comp φ) (ψ'.comp ψ) _ _
theorem
normed_add_group_hom.equalizer.ι_norm_noninc
{V : Type u_1}
{W : Type u_2}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
{f g : normed_add_group_hom V W} :
theorem
normed_add_group_hom.equalizer.lift_norm_noninc
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W}
(φ : normed_add_group_hom V₁ V)
(h : f.comp φ = g.comp φ)
(hφ : φ.norm_noninc) :
The lifting of a norm nonincreasing morphism is norm nonincreasing.
theorem
normed_add_group_hom.equalizer.norm_lift_le
{V : Type u_1}
{W : Type u_2}
{V₁ : Type u_3}
[seminormed_add_comm_group V]
[seminormed_add_comm_group W]
[seminormed_add_comm_group V₁]
{f g : normed_add_group_hom V W}
(φ : normed_add_group_hom V₁ V)
(h : f.comp φ = g.comp φ)
(C : ℝ)
(hφ : ‖φ‖ ≤ C) :
If φ satisfies ‖φ‖ ≤ C, then the same is true for the lifted morphism.
theorem
normed_add_group_hom.equalizer.map_norm_noninc
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{W₁ : Type u_6}
{W₂ : Type u_7}
[seminormed_add_comm_group W₁]
[seminormed_add_comm_group W₂]
{f₁ g₁ : normed_add_group_hom V₁ W₁}
{f₂ g₂ : normed_add_group_hom V₂ W₂}
{φ : normed_add_group_hom V₁ V₂}
{ψ : normed_add_group_hom W₁ W₂}
(hf : ψ.comp f₁ = f₂.comp φ)
(hg : ψ.comp g₁ = g₂.comp φ)
(hφ : φ.norm_noninc) :
(normed_add_group_hom.equalizer.map φ ψ hf hg).norm_noninc
theorem
normed_add_group_hom.equalizer.norm_map_le
{V₁ : Type u_3}
{V₂ : Type u_4}
[seminormed_add_comm_group V₁]
[seminormed_add_comm_group V₂]
{W₁ : Type u_6}
{W₂ : Type u_7}
[seminormed_add_comm_group W₁]
[seminormed_add_comm_group W₂]
{f₁ g₁ : normed_add_group_hom V₁ W₁}
{f₂ g₂ : normed_add_group_hom V₂ W₂}
{φ : normed_add_group_hom V₁ V₂}
{ψ : normed_add_group_hom W₁ W₂}
(hf : ψ.comp f₁ = f₂.comp φ)
(hg : ψ.comp g₁ = g₂.comp φ)
(C : ℝ)
(hφ : ‖φ.comp (normed_add_group_hom.equalizer.ι f₁ g₁)‖ ≤ C) :
‖normed_add_group_hom.equalizer.map φ ψ hf hg‖ ≤ C