# Normed groups homomorphisms #

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 SeminormedAddGroupHom and we specialize to NormedAddGroupHom when needed.

structure NormedAddGroupHom (V : Type u_1) (W : Type u_2) :
Type (max u_1 u_2)

A morphism of seminormed abelian groups is a bounded group homomorphism.

• toFun : VW

The function underlying a NormedAddGroupHom

• map_add' : ∀ (v₁ v₂ : V), self.toFun (v₁ + v₂) = self.toFun v₁ + self.toFun v₂

A NormedAddGroupHom is additive.

• bound' : ∃ (C : ), ∀ (v : V), self.toFun v C * v

A NormedAddGroupHom is bounded.

Instances For
theorem NormedAddGroupHom.map_add' {V : Type u_1} {W : Type u_2} (self : ) (v₁ : V) (v₂ : V) :
self.toFun (v₁ + v₂) = self.toFun v₁ + self.toFun v₂

A NormedAddGroupHom is additive.

theorem NormedAddGroupHom.bound' {V : Type u_1} {W : Type u_2} (self : ) :
∃ (C : ), ∀ (v : V), self.toFun v C * v

A NormedAddGroupHom is bounded.

def AddMonoidHom.mkNormedAddGroupHom {V : Type u_1} {W : Type u_2} (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 AddMonoidHom.mkNormedAddGroupHom' for a version that uses ℝ≥0 for the bound.

Equations
• f.mkNormedAddGroupHom C h = { toFun := (f).toFun, map_add' := , bound' := }
Instances For
def AddMonoidHom.mkNormedAddGroupHom' {V : Type u_1} {W : Type u_2} (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 AddMonoidHom.mkNormedAddGroupHom for a version that uses ℝ for the bound.

Equations
• f.mkNormedAddGroupHom' C hC = { toFun := (f).toFun, map_add' := , bound' := }
Instances For
theorem exists_pos_bound_of_bound {V : Type u_1} {W : Type u_2} {f : VW} (M : ) (h : ∀ (x : V), f x M * x) :
∃ (N : ), 0 < N ∀ (x : V), f x N * x
def NormedAddGroupHom.ofLipschitz {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {K : NNReal} (h : ) :

A Lipschitz continuous additive homomorphism is a normed additive group homomorphism.

Equations
• = f.mkNormedAddGroupHom K
Instances For
instance NormedAddGroupHom.funLike {V₁ : Type u_2} {V₂ : Type u_3} :
FunLike () V₁ V₂
Equations
• NormedAddGroupHom.funLike = { coe := NormedAddGroupHom.toFun, coe_injective' := }
instance NormedAddGroupHom.toAddMonoidHomClass {V₁ : Type u_2} {V₂ : Type u_3} :
AddMonoidHomClass () V₁ V₂
Equations
• =
theorem NormedAddGroupHom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} {f : } {g : } (H : f = g) :
f = g
theorem NormedAddGroupHom.coe_injective {V₁ : Type u_2} {V₂ : Type u_3} :
theorem NormedAddGroupHom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} {f : } {g : } :
f = g f = g
theorem NormedAddGroupHom.ext {V₁ : Type u_2} {V₂ : Type u_3} {f : } {g : } (H : ∀ (x : V₁), f x = g x) :
f = g
theorem NormedAddGroupHom.ext_iff {V₁ : Type u_2} {V₂ : Type u_3} {f : } {g : } :
f = g ∀ (x : V₁), f x = g x
@[simp]
theorem NormedAddGroupHom.toFun_eq_coe {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
f.toFun = f
theorem NormedAddGroupHom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ) (h₃ : ∀ (v : V₁), f v h₂ * v) :
{ toFun := f, map_add' := h₁, bound' := } = f
@[simp]
theorem NormedAddGroupHom.coe_mkNormedAddGroupHom {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) (C : ) (hC : ∀ (v : V₁), f v C * v) :
(f.mkNormedAddGroupHom C hC) = f
@[simp]
theorem NormedAddGroupHom.coe_mkNormedAddGroupHom' {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) (C : NNReal) (hC : ∀ (x : V₁), f x‖₊ C * x‖₊) :
(f.mkNormedAddGroupHom' C hC) = f
def NormedAddGroupHom.toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
V₁ →+ V₂

The group homomorphism underlying a bounded group homomorphism.

Equations
Instances For
@[simp]
theorem NormedAddGroupHom.coe_toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
theorem NormedAddGroupHom.toAddMonoidHom_injective {V₁ : Type u_2} {V₂ : Type u_3} :
@[simp]
theorem NormedAddGroupHom.mk_toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ∃ (C : ), ∀ (v : V₁), f v C * v) :
{ toFun := f, map_add' := h₁, bound' := h₂ }.toAddMonoidHom =
theorem NormedAddGroupHom.bound {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
∃ (C : ), 0 < C ∀ (x : V₁), f x C * x
theorem NormedAddGroupHom.antilipschitz_of_norm_ge {V₁ : Type u_2} {V₂ : Type u_3} (f : ) {K : NNReal} (h : ∀ (x : V₁), x K * f x) :
def NormedAddGroupHom.SurjectiveOnWith {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (K : ) (C : ) :

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.

Equations
Instances For
theorem NormedAddGroupHom.SurjectiveOnWith.mono {V₁ : Type u_2} {V₂ : Type u_3} {f : } {K : } {C : } {C' : } (h : f.SurjectiveOnWith K C) (H : C C') :
f.SurjectiveOnWith K C'
theorem NormedAddGroupHom.SurjectiveOnWith.exists_pos {V₁ : Type u_2} {V₂ : Type u_3} {f : } {K : } {C : } (h : f.SurjectiveOnWith K C) :
C' > 0, f.SurjectiveOnWith K C'
theorem NormedAddGroupHom.SurjectiveOnWith.surjOn {V₁ : Type u_2} {V₂ : Type u_3} {f : } {K : } {C : } (h : f.SurjectiveOnWith K C) :
Set.SurjOn (f) Set.univ K

### The operator norm #

def NormedAddGroupHom.opNorm {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :

The operator norm of a seminormed group homomorphism is the inf of all its bounds.

Equations
Instances For
instance NormedAddGroupHom.hasOpNorm {V₁ : Type u_2} {V₂ : Type u_3} :
Norm ()
Equations
• NormedAddGroupHom.hasOpNorm = { norm := NormedAddGroupHom.opNorm }
theorem NormedAddGroupHom.norm_def {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
f = sInf {c : | 0 c ∀ (x : V₁), f x c * x}
theorem NormedAddGroupHom.bounds_nonempty {V₁ : Type u_2} {V₂ : Type u_3} {f : } :
∃ (c : ), c {c : | 0 c ∀ (x : V₁), f x c * x}
theorem NormedAddGroupHom.bounds_bddBelow {V₁ : Type u_2} {V₂ : Type u_3} {f : } :
BddBelow {c : | 0 c ∀ (x : V₁), f x c * x}
theorem NormedAddGroupHom.opNorm_nonneg {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
theorem NormedAddGroupHom.le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (x : V₁) :

The fundamental property of the operator norm: ‖f x‖ ≤ ‖f‖ * ‖x‖.

theorem NormedAddGroupHom.le_opNorm_of_le {V₁ : Type u_2} {V₂ : Type u_3} (f : ) {c : } {x : V₁} (h : x c) :
theorem NormedAddGroupHom.le_of_opNorm_le {V₁ : Type u_2} {V₂ : Type u_3} (f : ) {c : } (h : f c) (x : V₁) :
theorem NormedAddGroupHom.lipschitz {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
LipschitzWith f, f

continuous linear maps are Lipschitz continuous.

theorem NormedAddGroupHom.uniformContinuous {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
theorem NormedAddGroupHom.continuous {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
theorem NormedAddGroupHom.ratio_le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (x : V₁) :
theorem NormedAddGroupHom.opNorm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} (f : ) {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 NormedAddGroupHom.opNorm_eq_of_bounds {V₁ : Type u_2} {V₂ : Type u_3} (f : ) {M : } (M_nonneg : 0 M) (h_above : ∀ (x : V₁), f x M * x) (h_below : N0, (∀ (x : V₁), f x N * x)M N) :
theorem NormedAddGroupHom.opNorm_le_of_lipschitz {V₁ : Type u_2} {V₂ : Type u_3} {f : } {K : NNReal} (hf : ) :
f K
theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {C : } (hC : 0 C) (h : ∀ (x : V₁), f x C * x) :
f.mkNormedAddGroupHom C h C

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor if it is nonnegative.

theorem NormedAddGroupHom.ofLipschitz_norm_le {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {K : NNReal} (h : ) :

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor NormedAddGroupHom.ofLipschitz, then its norm is bounded by the bound given to the constructor.

theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {C : } (h : ∀ (x : V₁), f x C * x) :
f.mkNormedAddGroupHom C h max C 0

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor or zero if this bound is negative.

theorem AddMonoidHom.mkNormedAddGroupHom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {C : } (hC : 0 C) (h : ∀ (x : V₁), f x C * x) :
f.mkNormedAddGroupHom C h C

Alias of NormedAddGroupHom.mkNormedAddGroupHom_norm_le.

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor if it is nonnegative.

theorem AddMonoidHom.mkNormedAddGroupHom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {C : } (h : ∀ (x : V₁), f x C * x) :
f.mkNormedAddGroupHom C h max C 0

Alias of NormedAddGroupHom.mkNormedAddGroupHom_norm_le'.

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor or zero if this bound is negative.

### Addition of normed group homs #

instance NormedAddGroupHom.add {V₁ : Type u_2} {V₂ : Type u_3} :

Addition of normed group homs.

Equations
theorem NormedAddGroupHom.opNorm_add_le {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (g : ) :

The operator norm satisfies the triangle inequality.

@[simp]
theorem NormedAddGroupHom.coe_add {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (g : ) :
(f + g) = f + g
@[simp]
theorem NormedAddGroupHom.add_apply {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (g : ) (v : V₁) :
(f + g) v = f v + g v

### The zero normed group hom #

instance NormedAddGroupHom.zero {V₁ : Type u_2} {V₂ : Type u_3} :
Zero ()
Equations
• NormedAddGroupHom.zero = { zero := }
instance NormedAddGroupHom.inhabited {V₁ : Type u_2} {V₂ : Type u_3} :
Equations
• NormedAddGroupHom.inhabited = { default := 0 }
theorem NormedAddGroupHom.opNorm_zero {V₁ : Type u_2} {V₂ : Type u_3} :

The norm of the 0 operator is 0.

theorem NormedAddGroupHom.opNorm_zero_iff {V₁ : Type u_5} {V₂ : Type u_6} [] [] {f : } :
f = 0 f = 0

For normed groups, an operator is zero iff its norm vanishes.

@[simp]
theorem NormedAddGroupHom.coe_zero {V₁ : Type u_2} {V₂ : Type u_3} :
0 = 0
@[simp]
theorem NormedAddGroupHom.zero_apply {V₁ : Type u_2} {V₂ : Type u_3} (v : V₁) :
0 v = 0

### The identity normed group hom #

@[simp]
theorem NormedAddGroupHom.id_apply (V : Type u_1) :
∀ (a : V), a = a
def NormedAddGroupHom.id (V : Type u_1) :

The identity as a continuous normed group hom.

Equations
• = ().mkNormedAddGroupHom 1
Instances For

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 NormedAddGroupHom.norm_id_of_nontrivial_seminorm (V : Type u_1) (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.)

theorem NormedAddGroupHom.norm_id {V : Type u_5} [] :

If a normed space is non-trivial, then the norm of the identity equals 1.

theorem NormedAddGroupHom.coe_id (V : Type u_1) :
= id

### The negation of a normed group hom #

instance NormedAddGroupHom.neg {V₁ : Type u_2} {V₂ : Type u_3} :
Neg ()

Opposite of a normed group hom.

Equations
• NormedAddGroupHom.neg = { neg := fun (f : ) => (-f.toAddMonoidHom).mkNormedAddGroupHom f }
@[simp]
theorem NormedAddGroupHom.coe_neg {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :
(-f) = -f
@[simp]
theorem NormedAddGroupHom.neg_apply {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (v : V₁) :
(-f) v = -f v
theorem NormedAddGroupHom.opNorm_neg {V₁ : Type u_2} {V₂ : Type u_3} (f : ) :

### Subtraction of normed group homs #

instance NormedAddGroupHom.sub {V₁ : Type u_2} {V₂ : Type u_3} :
Sub ()

Subtraction of normed group homs.

Equations
• NormedAddGroupHom.sub = { sub := fun (f g : ) => let __src := f.toAddMonoidHom - g.toAddMonoidHom; { toFun := (__src).toFun, map_add' := , bound' := } }
@[simp]
theorem NormedAddGroupHom.coe_sub {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (g : ) :
(f - g) = f - g
@[simp]
theorem NormedAddGroupHom.sub_apply {V₁ : Type u_2} {V₂ : Type u_3} (f : ) (g : ) (v : V₁) :
(f - g) v = f v - g v

### Scalar actions on normed group homs #

instance NormedAddGroupHom.smul {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} [] [] [BoundedSMul R V₂] :
SMul R ()
Equations
• NormedAddGroupHom.smul = { smul := fun (r : R) (f : ) => { toFun := r f, map_add' := , bound' := } }
@[simp]
theorem NormedAddGroupHom.coe_smul {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} [] [] [BoundedSMul R V₂] (r : R) (f : ) :
(r f) = r f
@[simp]
theorem NormedAddGroupHom.smul_apply {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} [] [] [BoundedSMul R V₂] (r : R) (f : ) (v : V₁) :
(r f) v = r f v
instance NormedAddGroupHom.smulCommClass {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} {R' : Type u_6} [] [] [BoundedSMul R V₂] [] [DistribMulAction R' V₂] [] [BoundedSMul R' V₂] [SMulCommClass R R' V₂] :
Equations
• =
instance NormedAddGroupHom.isScalarTower {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} {R' : Type u_6} [] [] [BoundedSMul R V₂] [] [DistribMulAction R' V₂] [] [BoundedSMul R' V₂] [SMul R R'] [IsScalarTower R R' V₂] :
Equations
• =
instance NormedAddGroupHom.isCentralScalar {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} [] [] [BoundedSMul R V₂] [] [] :
Equations
• =
instance NormedAddGroupHom.nsmul {V₁ : Type u_2} {V₂ : Type u_3} :
Equations
• NormedAddGroupHom.nsmul = { smul := fun (n : ) (f : ) => { toFun := n f, map_add' := , bound' := } }
@[simp]
theorem NormedAddGroupHom.coe_nsmul {V₁ : Type u_2} {V₂ : Type u_3} (r : ) (f : ) :
(r f) = r f
@[simp]
theorem NormedAddGroupHom.nsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} (r : ) (f : ) (v : V₁) :
(r f) v = r f v
instance NormedAddGroupHom.zsmul {V₁ : Type u_2} {V₂ : Type u_3} :
Equations
• NormedAddGroupHom.zsmul = { smul := fun (z : ) (f : ) => { toFun := z f, map_add' := , bound' := } }
@[simp]
theorem NormedAddGroupHom.coe_zsmul {V₁ : Type u_2} {V₂ : Type u_3} (r : ) (f : ) :
(r f) = r f
@[simp]
theorem NormedAddGroupHom.zsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} (r : ) (f : ) (v : V₁) :
(r f) v = r f v

### Normed group structure on normed group homs #

instance NormedAddGroupHom.toAddCommGroup {V₁ : Type u_2} {V₂ : Type u_3} :

Homs between two given normed groups form a commutative additive group.

Equations
instance NormedAddGroupHom.toSeminormedAddCommGroup {V₁ : Type u_2} {V₂ : Type u_3} :

Normed group homomorphisms themselves form a seminormed group with respect to the operator norm.

Equations
instance NormedAddGroupHom.toNormedAddCommGroup {V₁ : Type u_5} {V₂ : Type u_6} [] [] :

Normed group homomorphisms themselves form a normed group with respect to the operator norm.

Equations
• NormedAddGroupHom.toNormedAddCommGroup = { toFun := NormedAddGroupHom.opNorm, map_zero' := , add_le' := , neg' := , eq_zero_of_map_eq_zero' := }.toNormedAddCommGroup
@[simp]
theorem NormedAddGroupHom.coeAddHom_apply {V₁ : Type u_2} {V₂ : Type u_3} :
∀ (a : ) (a_1 : V₁), NormedAddGroupHom.coeAddHom a a_1 = a a_1
def NormedAddGroupHom.coeAddHom {V₁ : Type u_2} {V₂ : Type u_3} :
→+ V₁V₂

Coercion of a NormedAddGroupHom is an AddMonoidHom. Similar to AddMonoidHom.coeFn.

Equations
• NormedAddGroupHom.coeAddHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
@[simp]
theorem NormedAddGroupHom.coe_sum {V₁ : Type u_2} {V₂ : Type u_3} {ι : Type u_5} (s : ) (f : ι) :
(is, f i) = is, (f i)
theorem NormedAddGroupHom.sum_apply {V₁ : Type u_2} {V₂ : Type u_3} {ι : Type u_5} (s : ) (f : ι) (v : V₁) :
(is, f i) v = is, (f i) v

### Module structure on normed group homs #

instance NormedAddGroupHom.distribMulAction {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} [] [] [BoundedSMul R V₂] :
Equations
instance NormedAddGroupHom.module {V₁ : Type u_2} {V₂ : Type u_3} {R : Type u_5} [] [Module R V₂] [BoundedSMul R V₂] :
Module R ()
Equations

### Composition of normed group homs #

@[simp]
theorem NormedAddGroupHom.comp_apply {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} (g : ) (f : ) :
∀ (a : V₁), (g.comp f) a = g (f a)
def NormedAddGroupHom.comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} (g : ) (f : ) :

The composition of continuous normed group homs.

Equations
Instances For
theorem NormedAddGroupHom.norm_comp_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} (g : ) (f : ) :
theorem NormedAddGroupHom.norm_comp_le_of_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {f : } {g : } {C₁ : } {C₂ : } (hg : g C₂) (hf : f C₁) :
g.comp f C₂ * C₁
theorem NormedAddGroupHom.norm_comp_le_of_le' {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {f : } {g : } (C₁ : ) (C₂ : ) (C₃ : ) (h : C₃ = C₂ * C₁) (hg : g C₂) (hf : f C₁) :
g.comp f C₃
def NormedAddGroupHom.compHom {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} :

Composition of normed groups hom as an additive group morphism.

Equations
Instances For
@[simp]
theorem NormedAddGroupHom.comp_zero {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} (f : ) :
f.comp 0 = 0
@[simp]
theorem NormedAddGroupHom.zero_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} (f : ) :
theorem NormedAddGroupHom.comp_assoc {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {V₄ : Type u_5} (h : ) (g : ) (f : ) :
(h.comp g).comp f = h.comp (g.comp f)
theorem NormedAddGroupHom.coe_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} (f : ) (g : ) :
(g.comp f) = g f
@[simp]
theorem NormedAddGroupHom.incl_apply {V : Type u_1} (s : ) (self : s) :
self = self
def NormedAddGroupHom.incl {V : Type u_1} (s : ) :

The inclusion of an AddSubgroup, as bounded group homomorphism.

Equations
• = { toFun := Subtype.val, map_add' := , bound' := }
Instances For
theorem NormedAddGroupHom.norm_incl {V : Type u_1} {V' : } (x : V') :

### Kernel #

def NormedAddGroupHom.ker {V₁ : Type u_3} {V₂ : Type u_4} (f : ) :

The kernel of a bounded group homomorphism. Naturally endowed with a SeminormedAddCommGroup instance.

Equations
• f.ker = f.toAddMonoidHom.ker
Instances For
theorem NormedAddGroupHom.mem_ker {V₁ : Type u_3} {V₂ : Type u_4} (f : ) (v : V₁) :
v f.ker f v = 0
@[simp]
theorem NormedAddGroupHom.ker.lift_apply_coe {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} (f : ) (g : ) (h : g.comp f = 0) (v : V₁) :
(() v) = f v
def NormedAddGroupHom.ker.lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} (f : ) (g : ) (h : g.comp f = 0) :

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.

Equations
• = { toFun := fun (v : V₁) => f v, , map_add' := , bound' := }
Instances For
@[simp]
theorem NormedAddGroupHom.ker.incl_comp_lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} (f : ) (g : ) (h : g.comp f = 0) :
().comp () = f
@[simp]
theorem NormedAddGroupHom.ker_zero {V₁ : Type u_3} {V₂ : Type u_4} :
theorem NormedAddGroupHom.coe_ker {V₁ : Type u_3} {V₂ : Type u_4} (f : ) :
f.ker = f ⁻¹' {0}
theorem NormedAddGroupHom.isClosed_ker {V₁ : Type u_3} {V₂ : Type u_6} [] (f : ) :
IsClosed f.ker

### Range #

def NormedAddGroupHom.range {V₁ : Type u_3} {V₂ : Type u_4} (f : ) :

The image of a bounded group homomorphism. Naturally endowed with a SeminormedAddCommGroup instance.

Equations
• f.range = f.toAddMonoidHom.range
Instances For
theorem NormedAddGroupHom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} (f : ) (v : V₂) :
v f.range ∃ (w : V₁), f w = v
@[simp]
theorem NormedAddGroupHom.mem_range_self {V₁ : Type u_3} {V₂ : Type u_4} (f : ) (v : V₁) :
f v f.range
theorem NormedAddGroupHom.comp_range {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} (f : ) (g : ) :
theorem NormedAddGroupHom.incl_range {V₁ : Type u_3} (s : ) :
.range = s
@[simp]
theorem NormedAddGroupHom.range_comp_incl_top {V₁ : Type u_3} {V₂ : Type u_4} (f : ) :
(f.comp ).range = f.range
def NormedAddGroupHom.NormNoninc {V : Type u_1} {W : Type u_2} (f : ) :

A NormedAddGroupHom is norm-nonincreasing if ‖f v‖ ≤ ‖v‖ for all v.

Equations
Instances For
theorem NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one {V : Type u_1} {W : Type u_2} {f : } :
f.NormNoninc f 1
theorem NormedAddGroupHom.NormNoninc.zero {V₁ : Type u_3} {V₂ : Type u_4} :
theorem NormedAddGroupHom.NormNoninc.id {V : Type u_1} :
.NormNoninc
theorem NormedAddGroupHom.NormNoninc.comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {g : } {f : } (hg : g.NormNoninc) (hf : f.NormNoninc) :
(g.comp f).NormNoninc
@[simp]
theorem NormedAddGroupHom.NormNoninc.neg_iff {V₁ : Type u_3} {V₂ : Type u_4} {f : } :
(-f).NormNoninc f.NormNoninc
theorem NormedAddGroupHom.norm_eq_of_isometry {V : Type u_1} {W : Type u_2} {f : } (hf : Isometry f) (v : V) :
theorem NormedAddGroupHom.isometry_comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {g : } {f : } (hg : Isometry g) (hf : Isometry f) :
Isometry (g.comp f)
theorem NormedAddGroupHom.normNoninc_of_isometry {V : Type u_1} {W : Type u_2} {f : } (hf : Isometry f) :
f.NormNoninc
def NormedAddGroupHom.equalizer {V : Type u_1} {W : Type u_2} (f : ) (g : ) :

The equalizer of two morphisms f g : NormedAddGroupHom V W.

Equations
• f.equalizer g = (f - g).ker
Instances For
def NormedAddGroupHom.Equalizer.ι {V : Type u_1} {W : Type u_2} (f : ) (g : ) :
NormedAddGroupHom ((f.equalizer g)) V

The inclusion of f.equalizer g as a NormedAddGroupHom.

Equations
Instances For
theorem NormedAddGroupHom.Equalizer.comp_ι_eq {V : Type u_1} {W : Type u_2} (f : ) (g : ) :
f.comp = g.comp
@[simp]
theorem NormedAddGroupHom.Equalizer.lift_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } (φ : ) (h : f.comp φ = g.comp φ) (v : V₁) :
() = φ v
def NormedAddGroupHom.Equalizer.lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } (φ : ) (h : f.comp φ = g.comp φ) :
NormedAddGroupHom V₁ (f.equalizer g)

If φ : NormedAddGroupHom V₁ V is such that f.comp φ = g.comp φ, the induced morphism NormedAddGroupHom V₁ (f.equalizer g).

Equations
• = { toFun := fun (v : V₁) => φ v, , map_add' := , bound' := }
Instances For
@[simp]
theorem NormedAddGroupHom.Equalizer.ι_comp_lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } (φ : ) (h : f.comp φ = g.comp φ) :
.comp = φ
@[simp]
theorem NormedAddGroupHom.Equalizer.liftEquiv_symm_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } (ψ : NormedAddGroupHom V₁ (f.equalizer g)) :
(NormedAddGroupHom.Equalizer.liftEquiv.symm ψ) = .comp ψ
@[simp]
theorem NormedAddGroupHom.Equalizer.liftEquiv_apply {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } (φ : { φ : // f.comp φ = g.comp φ }) :
def NormedAddGroupHom.Equalizer.liftEquiv {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } :
{ φ : // f.comp φ = g.comp φ } NormedAddGroupHom V₁ (f.equalizer g)

The lifting property of the equalizer as an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def NormedAddGroupHom.Equalizer.map {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ : } {g₁ : } {f₂ : } {g₂ : } (φ : ) (ψ : ) (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :
NormedAddGroupHom (f₁.equalizer g₁) (f₂.equalizer g₂)

Given φ : NormedAddGroupHom V₁ V₂ and ψ : NormedAddGroupHom W₁ W₂ such that ψ.comp f₁ = f₂.comp φ and ψ.comp g₁ = g₂.comp φ, the induced morphism NormedAddGroupHom (f₁.equalizer g₁) (f₂.equalizer g₂).

Equations
Instances For
@[simp]
theorem NormedAddGroupHom.Equalizer.ι_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ : } {g₁ : } {f₂ : } {g₂ : } {φ : } {ψ : } (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :
().comp () = φ.comp ()
@[simp]
theorem NormedAddGroupHom.Equalizer.map_id {V₁ : Type u_3} {W₁ : Type u_6} {f₁ : } {g₁ : } :
= NormedAddGroupHom.id (f₁.equalizer g₁)
theorem NormedAddGroupHom.Equalizer.comm_sq₂ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} {f₁ : } {f₂ : } {f₃ : } {φ : } {ψ : } {φ' : } {ψ' : } (hf : ψ.comp f₁ = f₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') :
(ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
theorem NormedAddGroupHom.Equalizer.map_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} {f₁ : } {g₁ : } {f₂ : } {g₂ : } {f₃ : } {g₃ : } {φ : } {ψ : } {φ' : } {ψ' : } (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ') :
(NormedAddGroupHom.Equalizer.map φ' ψ' hf' hg').comp () = NormedAddGroupHom.Equalizer.map (φ'.comp φ) (ψ'.comp ψ)
theorem NormedAddGroupHom.Equalizer.ι_normNoninc {V : Type u_1} {W : Type u_2} {f : } {g : } :
.NormNoninc
theorem NormedAddGroupHom.Equalizer.lift_normNoninc {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } (φ : ) (h : f.comp φ = g.comp φ) (hφ : φ.NormNoninc) :
.NormNoninc

The lifting of a norm nonincreasing morphism is norm nonincreasing.

theorem NormedAddGroupHom.Equalizer.norm_lift_le {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f : } {g : } (φ : ) (h : f.comp φ = g.comp φ) (C : ) (hφ : φ C) :

If φ satisfies ‖φ‖ ≤ C, then the same is true for the lifted morphism.

theorem NormedAddGroupHom.Equalizer.map_normNoninc {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ : } {g₁ : } {f₂ : } {g₂ : } {φ : } {ψ : } (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hφ : φ.NormNoninc) :
().NormNoninc
theorem NormedAddGroupHom.Equalizer.norm_map_le {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ : } {g₁ : } {f₂ : } {g₂ : } {φ : } {ψ : } (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (C : ) (hφ : φ.comp () C) :