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) [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] : Type (max u_1 u_2)

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

• toFun : V → W

  The function underlying a NormedAddGroupHom

• map_add' (v₁ v₂ : V) : Eq (self.toFun (HAdd.hAdd v₁ v₂)) (HAdd.hAdd (self.toFun v₁) (self.toFun v₂))

  A NormedAddGroupHom is additive.

• bound' : Exists fun (C : Real) => ∀ (v : V), LE.le (Norm.norm (self.toFun v)) (HMul.hMul C (Norm.norm v))

  A NormedAddGroupHom is bounded.

def AddMonoidHom.mkNormedAddGroupHom {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f : AddMonoidHom V W) (C : Real) (h : ∀ (v : V), LE.le (Norm.norm (DFunLike.coe f v)) (HMul.hMul C (Norm.norm v))) : NormedAddGroupHom V W

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

• Eq (f.mkNormedAddGroupHom C h) { toFun := f.toFun, map_add' := ⋯, bound' := ⋯ }

def AddMonoidHom.mkNormedAddGroupHom' {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f : AddMonoidHom V W) (C : NNReal) (hC : ∀ (x : V), LE.le (NNNorm.nnnorm (DFunLike.coe f x)) (HMul.hMul C (NNNorm.nnnorm x))) : NormedAddGroupHom V W

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

• Eq (f.mkNormedAddGroupHom' C hC) { toFun := f.toFun, map_add' := ⋯, bound' := ⋯ }

theorem exists_pos_bound_of_bound {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f : V → W} (M : Real) (h : ∀ (x : V), LE.le (Norm.norm (f x)) (HMul.hMul M (Norm.norm x))) : Exists fun (N : Real) => And (LT.lt 0 N) (∀ (x : V), LE.le (Norm.norm (f x)) (HMul.hMul N (Norm.norm x)))

def NormedAddGroupHom.ofLipschitz {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) {K : NNReal} (h : LipschitzWith K (DFunLike.coe f)) : NormedAddGroupHom V₁ V₂

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

Equations

• Eq (NormedAddGroupHom.ofLipschitz f h) (f.mkNormedAddGroupHom K.toReal ⋯)

def NormedAddGroupHom.funLike {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : FunLike (NormedAddGroupHom V₁ V₂) V₁ V₂

Equations

• Eq NormedAddGroupHom.funLike { coe := NormedAddGroupHom.toFun, coe_injective' := ⋯ }

theorem NormedAddGroupHom.toAddMonoidHomClass {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V₁ V₂

theorem NormedAddGroupHom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f g : NormedAddGroupHom V₁ V₂} (H : Eq (DFunLike.coe f) (DFunLike.coe g)) : Eq f g

theorem NormedAddGroupHom.coe_injective {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Function.Injective toFun

theorem NormedAddGroupHom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f g : NormedAddGroupHom V₁ V₂} : Iff (Eq f g) (Eq (DFunLike.coe f) (DFunLike.coe g))

theorem NormedAddGroupHom.ext {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f g : NormedAddGroupHom V₁ V₂} (H : ∀ (x : V₁), Eq (DFunLike.coe f x) (DFunLike.coe g x)) : Eq f g

theorem NormedAddGroupHom.ext_iff {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f g : NormedAddGroupHom V₁ V₂} : Iff (Eq f g) (∀ (x : V₁), Eq (DFunLike.coe f x) (DFunLike.coe g x))

theorem NormedAddGroupHom.toFun_eq_coe {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Eq f.toFun (DFunLike.coe f)

theorem NormedAddGroupHom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), Eq (f (HAdd.hAdd v₁ v₂)) (HAdd.hAdd (f v₁) (f v₂))) (h₂ : Real) (h₃ : ∀ (v : V₁), LE.le (Norm.norm (f v)) (HMul.hMul h₂ (Norm.norm v))) : Eq (DFunLike.coe { toFun := f, map_add' := h₁, bound' := ⋯ }) f

theorem NormedAddGroupHom.coe_mkNormedAddGroupHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) (C : Real) (hC : ∀ (v : V₁), LE.le (Norm.norm (DFunLike.coe f v)) (HMul.hMul C (Norm.norm v))) : Eq (DFunLike.coe (f.mkNormedAddGroupHom C hC)) (DFunLike.coe f)

theorem NormedAddGroupHom.coe_mkNormedAddGroupHom' {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) (C : NNReal) (hC : ∀ (x : V₁), LE.le (NNNorm.nnnorm (DFunLike.coe f x)) (HMul.hMul C (NNNorm.nnnorm x))) : Eq (DFunLike.coe (f.mkNormedAddGroupHom' C hC)) (DFunLike.coe f)

def NormedAddGroupHom.toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : AddMonoidHom V₁ V₂

The group homomorphism underlying a bounded group homomorphism.

Equations

• Eq f.toAddMonoidHom (AddMonoidHom.mk' (DFunLike.coe f) ⋯)

theorem NormedAddGroupHom.coe_toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe f.toAddMonoidHom) (DFunLike.coe f)

theorem NormedAddGroupHom.toAddMonoidHom_injective {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Function.Injective toAddMonoidHom

theorem NormedAddGroupHom.mk_toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), Eq (f (HAdd.hAdd v₁ v₂)) (HAdd.hAdd (f v₁) (f v₂))) (h₂ : Exists fun (C : Real) => ∀ (v : V₁), LE.le (Norm.norm (f v)) (HMul.hMul C (Norm.norm v))) : Eq { toFun := f, map_add' := h₁, bound' := h₂ }.toAddMonoidHom (AddMonoidHom.mk' f h₁)

theorem NormedAddGroupHom.bound {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Exists fun (C : Real) => And (LT.lt 0 C) (∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul C (Norm.norm x)))

theorem NormedAddGroupHom.antilipschitz_of_norm_ge {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {K : NNReal} (h : ∀ (x : V₁), LE.le (Norm.norm x) (HMul.hMul K.toReal (Norm.norm (DFunLike.coe f x)))) : AntilipschitzWith K (DFunLike.coe f)

def NormedAddGroupHom.SurjectiveOnWith {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (K : AddSubgroup V₂) (C : Real) : 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.

Equations

• Eq (f.SurjectiveOnWith K C) (∀ (h : V₂), Membership.mem K h → Exists fun (g : V₁) => And (Eq (DFunLike.coe f g) h) (LE.le (Norm.norm g) (HMul.hMul C (Norm.norm h))))

theorem NormedAddGroupHom.SurjectiveOnWith.mono {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C C' : Real} (h : f.SurjectiveOnWith K C) (H : LE.le C C') : f.SurjectiveOnWith K C'

theorem NormedAddGroupHom.SurjectiveOnWith.exists_pos {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : Real} (h : f.SurjectiveOnWith K C) : Exists fun (C' : Real) => And (GT.gt C' 0) (f.SurjectiveOnWith K C')

theorem NormedAddGroupHom.SurjectiveOnWith.surjOn {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : Real} (h : f.SurjectiveOnWith K C) : Set.SurjOn (DFunLike.coe f) Set.univ (SetLike.coe K)

The operator norm

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

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

Equations

• Eq f.opNorm (InfSet.sInf (setOf fun (c : Real) => And (LE.le 0 c) (∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul c (Norm.norm x)))))

def NormedAddGroupHom.hasOpNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Norm (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.hasOpNorm { norm := NormedAddGroupHom.opNorm }

theorem NormedAddGroupHom.norm_def {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Eq (Norm.norm f) (InfSet.sInf (setOf fun (c : Real) => And (LE.le 0 c) (∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul c (Norm.norm x)))))

theorem NormedAddGroupHom.bounds_nonempty {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} : Exists fun (c : Real) => Membership.mem (setOf fun (c : Real) => And (LE.le 0 c) (∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul c (Norm.norm x)))) c

theorem NormedAddGroupHom.bounds_bddBelow {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} : BddBelow (setOf fun (c : Real) => And (LE.le 0 c) (∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul c (Norm.norm x))))

theorem NormedAddGroupHom.opNorm_nonneg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : LE.le 0 (Norm.norm f)

theorem NormedAddGroupHom.le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (x : V₁) : LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul (Norm.norm f) (Norm.norm x))

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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {c : Real} {x : V₁} (h : LE.le (Norm.norm x) c) : LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul (Norm.norm f) c)

theorem NormedAddGroupHom.le_of_opNorm_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {c : Real} (h : LE.le (Norm.norm f) c) (x : V₁) : LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul c (Norm.norm x))

theorem NormedAddGroupHom.lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : LipschitzWith ⟨Norm.norm f, ⋯⟩ (DFunLike.coe f)

continuous linear maps are Lipschitz continuous.

theorem NormedAddGroupHom.uniformContinuous {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : UniformContinuous (DFunLike.coe f)

theorem NormedAddGroupHom.continuous {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Continuous (DFunLike.coe f)

theorem NormedAddGroupHom.instContinuousMapClass {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : ContinuousMapClass (NormedAddGroupHom V₁ V₂) V₁ V₂

theorem NormedAddGroupHom.ratio_le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (x : V₁) : LE.le (HDiv.hDiv (Norm.norm (DFunLike.coe f x)) (Norm.norm x)) (Norm.norm f)

theorem NormedAddGroupHom.opNorm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {M : Real} (hMp : LE.le 0 M) (hM : ∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul M (Norm.norm x))) : LE.le (Norm.norm f) M

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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {M : Real} (M_nonneg : LE.le 0 M) (h_above : ∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul M (Norm.norm x))) (h_below : ∀ (N : Real), GE.ge N 0 → (∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul N (Norm.norm x))) → LE.le M N) : Eq (Norm.norm f) M

theorem NormedAddGroupHom.opNorm_le_of_lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {K : NNReal} (hf : LipschitzWith K (DFunLike.coe f)) : LE.le (Norm.norm f) K.toReal

theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) {C : Real} (hC : LE.le 0 C) (h : ∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul C (Norm.norm x))) : LE.le (Norm.norm (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) {K : NNReal} (h : LipschitzWith K (DFunLike.coe f)) : LE.le (Norm.norm (ofLipschitz f h)) K.toReal

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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) {C : Real} (h : ∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul C (Norm.norm x))) : LE.le (Norm.norm (f.mkNormedAddGroupHom C h)) (Max.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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) {C : Real} (hC : LE.le 0 C) (h : ∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul C (Norm.norm x))) : LE.le (Norm.norm (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : AddMonoidHom V₁ V₂) {C : Real} (h : ∀ (x : V₁), LE.le (Norm.norm (DFunLike.coe f x)) (HMul.hMul C (Norm.norm x))) : LE.le (Norm.norm (f.mkNormedAddGroupHom C h)) (Max.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

def NormedAddGroupHom.add {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Add (NormedAddGroupHom V₁ V₂)

Addition of normed group homs.

Equations

• Eq NormedAddGroupHom.add { add := fun (f g : NormedAddGroupHom V₁ V₂) => (HAdd.hAdd f.toAddMonoidHom g.toAddMonoidHom).mkNormedAddGroupHom (HAdd.hAdd (Norm.norm f) (Norm.norm g)) ⋯ }

theorem NormedAddGroupHom.opNorm_add_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) : LE.le (Norm.norm (HAdd.hAdd f g)) (HAdd.hAdd (Norm.norm f) (Norm.norm g))

The operator norm satisfies the triangle inequality.

theorem NormedAddGroupHom.coe_add {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe (HAdd.hAdd f g)) (HAdd.hAdd (DFunLike.coe f) (DFunLike.coe g))

theorem NormedAddGroupHom.add_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) (v : V₁) : Eq (DFunLike.coe (HAdd.hAdd f g) v) (HAdd.hAdd (DFunLike.coe f v) (DFunLike.coe g v))

The zero normed group hom

def NormedAddGroupHom.zero {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Zero (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.zero { zero := AddMonoidHom.mkNormedAddGroupHom 0 0 ⋯ }

def NormedAddGroupHom.inhabited {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Inhabited (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.inhabited { default := 0 }

theorem NormedAddGroupHom.opNorm_zero {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Eq (Norm.norm 0) 0

The norm of the 0 operator is 0.

theorem NormedAddGroupHom.opNorm_zero_iff {V₁ : Type u_5} {V₂ : Type u_6} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} : Iff (Eq (Norm.norm f) 0) (Eq f 0)

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

theorem NormedAddGroupHom.coe_zero {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Eq (DFunLike.coe 0) 0

theorem NormedAddGroupHom.zero_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (v : V₁) : Eq (DFunLike.coe 0 v) 0

The identity normed group hom

def NormedAddGroupHom.id (V : Type u_1) [SeminormedAddCommGroup V] : NormedAddGroupHom V V

The identity as a continuous normed group hom.

Equations

• Eq (NormedAddGroupHom.id V) ((AddMonoidHom.id V).mkNormedAddGroupHom 1 ⋯)

theorem NormedAddGroupHom.id_apply (V : Type u_1) [SeminormedAddCommGroup V] (a✝ : V) : Eq (DFunLike.coe (id V) a✝) a✝

theorem NormedAddGroupHom.norm_id_le (V : Type u_1) [SeminormedAddCommGroup V] : LE.le (Norm.norm (id V)) 1

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) [SeminormedAddCommGroup V] (h : Exists fun (x : V) => Ne (Norm.norm x) 0) : Eq (Norm.norm (id V)) 1

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} [NormedAddCommGroup V] [Nontrivial V] : Eq (Norm.norm (id V)) 1

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

theorem NormedAddGroupHom.coe_id (V : Type u_1) [SeminormedAddCommGroup V] : Eq (DFunLike.coe (id V)) _root_.id

The negation of a normed group hom

def NormedAddGroupHom.neg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Neg (NormedAddGroupHom V₁ V₂)

Opposite of a normed group hom.

Equations

• Eq NormedAddGroupHom.neg { neg := fun (f : NormedAddGroupHom V₁ V₂) => (Neg.neg f.toAddMonoidHom).mkNormedAddGroupHom (Norm.norm f) ⋯ }

theorem NormedAddGroupHom.coe_neg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe (Neg.neg f)) (Neg.neg (DFunLike.coe f))

theorem NormedAddGroupHom.neg_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) : Eq (DFunLike.coe (Neg.neg f) v) (Neg.neg (DFunLike.coe f v))

theorem NormedAddGroupHom.opNorm_neg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Eq (Norm.norm (Neg.neg f)) (Norm.norm f)

Subtraction of normed group homs

def NormedAddGroupHom.sub {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Sub (NormedAddGroupHom V₁ V₂)

Subtraction of normed group homs.

Equations

• One or more equations did not get rendered due to their size.

theorem NormedAddGroupHom.coe_sub {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe (HSub.hSub f g)) (HSub.hSub (DFunLike.coe f) (DFunLike.coe g))

theorem NormedAddGroupHom.sub_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) (v : V₁) : Eq (DFunLike.coe (HSub.hSub f g) v) (HSub.hSub (DFunLike.coe f v) (DFunLike.coe g v))

Scalar actions on normed group homs

def NormedAddGroupHom.smul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] : SMul R (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.smul { smul := fun (r : R) (f : NormedAddGroupHom V₁ V₂) => { toFun := HSMul.hSMul r (DFunLike.coe f), map_add' := ⋯, bound' := ⋯ } }

theorem NormedAddGroupHom.coe_smul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe (HSMul.hSMul r f)) (HSMul.hSMul r (DFunLike.coe f))

theorem NormedAddGroupHom.smul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) (v : V₁) : Eq (DFunLike.coe (HSMul.hSMul r f) v) (HSMul.hSMul r (DFunLike.coe f v))

theorem NormedAddGroupHom.smulCommClass {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} {R' : Type u_6} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R'] [IsBoundedSMul R' V₂] [SMulCommClass R R' V₂] : SMulCommClass R R' (NormedAddGroupHom V₁ V₂)

theorem NormedAddGroupHom.isScalarTower {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} {R' : Type u_6} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R'] [IsBoundedSMul R' V₂] [SMul R R'] [IsScalarTower R R' V₂] : IsScalarTower R R' (NormedAddGroupHom V₁ V₂)

theorem NormedAddGroupHom.isCentralScalar {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] [DistribMulAction (MulOpposite R) V₂] [IsCentralScalar R V₂] : IsCentralScalar R (NormedAddGroupHom V₁ V₂)

def NormedAddGroupHom.nsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : SMul Nat (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.nsmul { smul := fun (n : Nat) (f : NormedAddGroupHom V₁ V₂) => { toFun := HSMul.hSMul n (DFunLike.coe f), map_add' := ⋯, bound' := ⋯ } }

theorem NormedAddGroupHom.coe_nsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : Nat) (f : NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe (HSMul.hSMul r f)) (HSMul.hSMul r (DFunLike.coe f))

theorem NormedAddGroupHom.nsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : Nat) (f : NormedAddGroupHom V₁ V₂) (v : V₁) : Eq (DFunLike.coe (HSMul.hSMul r f) v) (HSMul.hSMul r (DFunLike.coe f v))

def NormedAddGroupHom.zsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : SMul Int (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.zsmul { smul := fun (z : Int) (f : NormedAddGroupHom V₁ V₂) => { toFun := HSMul.hSMul z (DFunLike.coe f), map_add' := ⋯, bound' := ⋯ } }

theorem NormedAddGroupHom.coe_zsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : Int) (f : NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe (HSMul.hSMul r f)) (HSMul.hSMul r (DFunLike.coe f))

theorem NormedAddGroupHom.zsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : Int) (f : NormedAddGroupHom V₁ V₂) (v : V₁) : Eq (DFunLike.coe (HSMul.hSMul r f) v) (HSMul.hSMul r (DFunLike.coe f v))

Normed group structure on normed group homs

def NormedAddGroupHom.toAddCommGroup {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : AddCommGroup (NormedAddGroupHom V₁ V₂)

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

Equations

• Eq NormedAddGroupHom.toAddCommGroup (Function.Injective.addCommGroup NormedAddGroupHom.toFun ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)

def NormedAddGroupHom.toSeminormedAddCommGroup {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : SeminormedAddCommGroup (NormedAddGroupHom V₁ V₂)

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

Equations

• Eq NormedAddGroupHom.toSeminormedAddCommGroup { toFun := NormedAddGroupHom.opNorm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }.toSeminormedAddCommGroup

def NormedAddGroupHom.toNormedAddCommGroup {V₁ : Type u_5} {V₂ : Type u_6} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] : NormedAddCommGroup (NormedAddGroupHom V₁ V₂)

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

Equations

• Eq NormedAddGroupHom.toNormedAddCommGroup { toFun := NormedAddGroupHom.opNorm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }.toNormedAddCommGroup

def NormedAddGroupHom.coeAddHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : AddMonoidHom (NormedAddGroupHom V₁ V₂) (V₁ → V₂)

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

Equations

• Eq NormedAddGroupHom.coeAddHom { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

theorem NormedAddGroupHom.coeAddHom_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (a✝ : NormedAddGroupHom V₁ V₂) (a : V₁) : Eq (DFunLike.coe coeAddHom a✝ a) (DFunLike.coe a✝ a)

theorem NormedAddGroupHom.coe_sum {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {ι : Type u_5} (s : Finset ι) (f : ι → NormedAddGroupHom V₁ V₂) : Eq (DFunLike.coe (s.sum fun (i : ι) => f i)) (s.sum fun (i : ι) => DFunLike.coe (f i))

theorem NormedAddGroupHom.sum_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {ι : Type u_5} (s : Finset ι) (f : ι → NormedAddGroupHom V₁ V₂) (v : V₁) : Eq (DFunLike.coe (s.sum fun (i : ι) => f i) v) (s.sum fun (i : ι) => DFunLike.coe (f i) v)

Module structure on normed group homs

def NormedAddGroupHom.distribMulAction {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] : DistribMulAction R (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.distribMulAction (Function.Injective.distribMulAction NormedAddGroupHom.coeAddHom ⋯ ⋯)

def NormedAddGroupHom.module {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [Semiring R] [Module R V₂] [PseudoMetricSpace R] [IsBoundedSMul R V₂] : Module R (NormedAddGroupHom V₁ V₂)

Equations

• Eq NormedAddGroupHom.module (Function.Injective.module R NormedAddGroupHom.coeAddHom ⋯ ⋯)

Composition of normed group homs

def NormedAddGroupHom.comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) : NormedAddGroupHom V₁ V₃

The composition of continuous normed group homs.

Equations

• Eq (g.comp f) ((g.toAddMonoidHom.comp f.toAddMonoidHom).mkNormedAddGroupHom (HMul.hMul (Norm.norm g) (Norm.norm f)) ⋯)

theorem NormedAddGroupHom.comp_apply {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) (a✝ : V₁) : Eq (DFunLike.coe (g.comp f) a✝) (DFunLike.coe g (DFunLike.coe f a✝))

theorem NormedAddGroupHom.norm_comp_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) : LE.le (Norm.norm (g.comp f)) (HMul.hMul (Norm.norm g) (Norm.norm f))

theorem NormedAddGroupHom.norm_comp_le_of_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₂ V₃} {C₁ C₂ : Real} (hg : LE.le (Norm.norm g) C₂) (hf : LE.le (Norm.norm f) C₁) : LE.le (Norm.norm (g.comp f)) (HMul.hMul C₂ C₁)

theorem NormedAddGroupHom.norm_comp_le_of_le' {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₂ V₃} (C₁ C₂ C₃ : Real) (h : Eq C₃ (HMul.hMul C₂ C₁)) (hg : LE.le (Norm.norm g) C₂) (hf : LE.le (Norm.norm f) C₁) : LE.le (Norm.norm (g.comp f)) C₃

def NormedAddGroupHom.compHom {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] : AddMonoidHom (NormedAddGroupHom V₂ V₃) (AddMonoidHom (NormedAddGroupHom V₁ V₂) (NormedAddGroupHom V₁ V₃))

Composition of normed groups hom as an additive group morphism.

Equations

• Eq NormedAddGroupHom.compHom (AddMonoidHom.mk' (fun (g : NormedAddGroupHom V₂ V₃) => AddMonoidHom.mk' (fun (f : NormedAddGroupHom V₁ V₂) => g.comp f) ⋯) ⋯)

theorem NormedAddGroupHom.comp_zero {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₂ V₃) : Eq (f.comp 0) 0

theorem NormedAddGroupHom.zero_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) : Eq (NormedAddGroupHom.comp 0 f) 0

theorem NormedAddGroupHom.comp_assoc {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {V₄ : Type u_5} [SeminormedAddCommGroup V₄] (h : NormedAddGroupHom V₃ V₄) (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) : Eq ((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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) : Eq (DFunLike.coe (g.comp f)) (Function.comp (DFunLike.coe g) (DFunLike.coe f))

def NormedAddGroupHom.incl {V : Type u_1} [SeminormedAddCommGroup V] (s : AddSubgroup V) : NormedAddGroupHom (Subtype fun (x : V) => Membership.mem s x) V

The inclusion of an AddSubgroup, as bounded group homomorphism.

Equations

• Eq (NormedAddGroupHom.incl s) { toFun := Subtype.val, map_add' := ⋯, bound' := ⋯ }

theorem NormedAddGroupHom.incl_apply {V : Type u_1} [SeminormedAddCommGroup V] (s : AddSubgroup V) (self : Subtype fun (x : V) => Membership.mem s x) : Eq (DFunLike.coe (incl s) self) self.val

theorem NormedAddGroupHom.norm_incl {V : Type u_1} [SeminormedAddCommGroup V] {V' : AddSubgroup V} (x : Subtype fun (x : V) => Membership.mem V' x) : Eq (Norm.norm (DFunLike.coe (incl V') x)) (Norm.norm x)

Kernel

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

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

Equations

• Eq f.ker f.toAddMonoidHom.ker

theorem NormedAddGroupHom.mem_ker {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) : Iff (Membership.mem f.ker v) (Eq (DFunLike.coe f v) 0)

def NormedAddGroupHom.ker.lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) (h : Eq (g.comp f) 0) : NormedAddGroupHom V₁ (Subtype fun (x : V₂) => Membership.mem g.ker x)

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

• Eq (NormedAddGroupHom.ker.lift f g h) { toFun := fun (v : V₁) => ⟨DFunLike.coe f v, ⋯⟩, map_add' := ⋯, bound' := ⋯ }

theorem NormedAddGroupHom.ker.lift_apply_coe {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) (h : Eq (g.comp f) 0) (v : V₁) : Eq (DFunLike.coe (lift f g h) v).val (DFunLike.coe f v)

theorem NormedAddGroupHom.ker.incl_comp_lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) (h : Eq (g.comp f) 0) : Eq ((incl g.ker).comp (lift f g h)) f

theorem NormedAddGroupHom.ker_zero {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Eq (ker 0) Top.top

theorem NormedAddGroupHom.coe_ker {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Eq (SetLike.coe f.ker) (Set.preimage (DFunLike.coe f) (Singleton.singleton 0))

theorem NormedAddGroupHom.isClosed_ker {V₁ : Type u_3} [SeminormedAddCommGroup V₁] {V₂ : Type u_6} [NormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : IsClosed (SetLike.coe f.ker)

Range

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

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

Equations

• Eq f.range f.toAddMonoidHom.range

theorem NormedAddGroupHom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₂) : Iff (Membership.mem f.range v) (Exists fun (w : V₁) => Eq (DFunLike.coe f w) v)

theorem NormedAddGroupHom.mem_range_self {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) : Membership.mem f.range (DFunLike.coe f v)

theorem NormedAddGroupHom.comp_range {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) : Eq (g.comp f).range (AddSubgroup.map g.toAddMonoidHom f.range)

theorem NormedAddGroupHom.incl_range {V₁ : Type u_3} [SeminormedAddCommGroup V₁] (s : AddSubgroup V₁) : Eq (incl s).range s

theorem NormedAddGroupHom.range_comp_incl_top {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : Eq (f.comp (incl Top.top)).range f.range

def NormedAddGroupHom.NormNoninc {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f : NormedAddGroupHom V W) : Prop

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

Equations

• Eq f.NormNoninc (∀ (v : V), LE.le (Norm.norm (DFunLike.coe f v)) (Norm.norm v))

theorem NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f : NormedAddGroupHom V W} : Iff f.NormNoninc (LE.le (Norm.norm f) 1)

theorem NormedAddGroupHom.NormNoninc.zero {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : NormNoninc 0

theorem NormedAddGroupHom.NormNoninc.id {V : Type u_1} [SeminormedAddCommGroup V] : (NormedAddGroupHom.id V).NormNoninc

theorem NormedAddGroupHom.NormNoninc.comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {g : NormedAddGroupHom V₂ V₃} {f : NormedAddGroupHom V₁ V₂} (hg : g.NormNoninc) (hf : f.NormNoninc) : (g.comp f).NormNoninc

theorem NormedAddGroupHom.NormNoninc.neg_iff {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} : Iff (Neg.neg f).NormNoninc f.NormNoninc

theorem NormedAddGroupHom.norm_eq_of_isometry {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f : NormedAddGroupHom V W} (hf : Isometry (DFunLike.coe f)) (v : V) : Eq (Norm.norm (DFunLike.coe f v)) (Norm.norm v)

theorem NormedAddGroupHom.isometry_id {V : Type u_1} [SeminormedAddCommGroup V] : Isometry (DFunLike.coe (id V))

theorem NormedAddGroupHom.isometry_comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {g : NormedAddGroupHom V₂ V₃} {f : NormedAddGroupHom V₁ V₂} (hg : Isometry (DFunLike.coe g)) (hf : Isometry (DFunLike.coe f)) : Isometry (DFunLike.coe (g.comp f))

theorem NormedAddGroupHom.normNoninc_of_isometry {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f : NormedAddGroupHom V W} (hf : Isometry (DFunLike.coe f)) : f.NormNoninc

def NormedAddGroupHom.equalizer {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f g : NormedAddGroupHom V W) : AddSubgroup V

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

Equations

• Eq (f.equalizer g) (HSub.hSub f g).ker

def NormedAddGroupHom.Equalizer.ι {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f g : NormedAddGroupHom V W) : NormedAddGroupHom (Subtype fun (x : V) => Membership.mem (f.equalizer g) x) V

The inclusion of f.equalizer g as a NormedAddGroupHom.

Equations

• Eq (NormedAddGroupHom.Equalizer.ι f g) (NormedAddGroupHom.incl (f.equalizer g))

theorem NormedAddGroupHom.Equalizer.comp_ι_eq {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f g : NormedAddGroupHom V W) : Eq (f.comp (ι f g)) (g.comp (ι f g))

def NormedAddGroupHom.Equalizer.lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V) (h : Eq (f.comp φ) (g.comp φ)) : NormedAddGroupHom V₁ (Subtype fun (x : V) => Membership.mem (f.equalizer g) x)

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

Equations

• Eq (NormedAddGroupHom.Equalizer.lift φ h) { toFun := fun (v : V₁) => ⟨DFunLike.coe φ v, ⋯⟩, map_add' := ⋯, bound' := ⋯ }

theorem NormedAddGroupHom.Equalizer.lift_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V) (h : Eq (f.comp φ) (g.comp φ)) (v : V₁) : Eq (DFunLike.coe (lift φ h) v).val (DFunLike.coe φ v)

theorem NormedAddGroupHom.Equalizer.ι_comp_lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V) (h : Eq (f.comp φ) (g.comp φ)) : Eq ((ι f g).comp (lift φ h)) φ

def NormedAddGroupHom.Equalizer.liftEquiv {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} : Equiv (Subtype fun (φ : NormedAddGroupHom V₁ V) => Eq (f.comp φ) (g.comp φ)) (NormedAddGroupHom V₁ (Subtype fun (x : V) => Membership.mem (f.equalizer g) x))

The lifting property of the equalizer as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem NormedAddGroupHom.Equalizer.liftEquiv_symm_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (ψ : NormedAddGroupHom V₁ (Subtype fun (x : V) => Membership.mem (f.equalizer g) x)) : Eq (DFunLike.coe liftEquiv.symm ψ).val ((ι f g).comp ψ)

theorem NormedAddGroupHom.Equalizer.liftEquiv_apply {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : Subtype fun (φ : NormedAddGroupHom V₁ V) => Eq (f.comp φ) (g.comp φ)) : Eq (DFunLike.coe liftEquiv φ) (lift φ.val ⋯)

def NormedAddGroupHom.Equalizer.map {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {W₁ : Type u_6} {W₂ : Type u_7} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} (φ : NormedAddGroupHom V₁ V₂) (ψ : NormedAddGroupHom W₁ W₂) (hf : Eq (ψ.comp f₁) (f₂.comp φ)) (hg : Eq (ψ.comp g₁) (g₂.comp φ)) : NormedAddGroupHom (Subtype fun (x : V₁) => Membership.mem (f₁.equalizer g₁) x) (Subtype fun (x : V₂) => Membership.mem (f₂.equalizer g₂) x)

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

• Eq (NormedAddGroupHom.Equalizer.map φ ψ hf hg) (NormedAddGroupHom.Equalizer.lift (φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)) ⋯)

theorem NormedAddGroupHom.Equalizer.ι_comp_map {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {W₁ : Type u_6} {W₂ : Type u_7} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} (hf : Eq (ψ.comp f₁) (f₂.comp φ)) (hg : Eq (ψ.comp g₁) (g₂.comp φ)) : Eq ((ι f₂ g₂).comp (map φ ψ hf hg)) (φ.comp (ι f₁ g₁))

theorem NormedAddGroupHom.Equalizer.map_id {V₁ : Type u_3} [SeminormedAddCommGroup V₁] {W₁ : Type u_6} [SeminormedAddCommGroup W₁] {f₁ g₁ : NormedAddGroupHom V₁ W₁} : Eq (map (id V₁) (id W₁) ⋯ ⋯) (id (Subtype fun (x : V₁) => Membership.mem (f₁.equalizer g₁) x))

theorem NormedAddGroupHom.Equalizer.comm_sq₂ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] [SeminormedAddCommGroup W₃] {f₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {f₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃} (hf : Eq (ψ.comp f₁) (f₂.comp φ)) (hf' : Eq (ψ'.comp f₂) (f₃.comp φ')) : Eq ((ψ'.comp ψ).comp f₁) (f₃.comp (φ'.comp φ))

theorem NormedAddGroupHom.Equalizer.map_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] [SeminormedAddCommGroup W₃] {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {f₃ g₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃} (hf : Eq (ψ.comp f₁) (f₂.comp φ)) (hg : Eq (ψ.comp g₁) (g₂.comp φ)) (hf' : Eq (ψ'.comp f₂) (f₃.comp φ')) (hg' : Eq (ψ'.comp g₂) (g₃.comp φ')) : Eq ((map φ' ψ' hf' hg').comp (map φ ψ hf hg)) (map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯)

theorem NormedAddGroupHom.Equalizer.ι_normNoninc {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f g : NormedAddGroupHom V W} : (ι f g).NormNoninc

theorem NormedAddGroupHom.Equalizer.lift_normNoninc {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V) (h : Eq (f.comp φ) (g.comp φ)) (hφ : φ.NormNoninc) : (lift φ h).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} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V) (h : Eq (f.comp φ) (g.comp φ)) (C : Real) (hφ : LE.le (Norm.norm φ) C) : LE.le (Norm.norm (lift φ 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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {W₁ : Type u_6} {W₂ : Type u_7} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} (hf : Eq (ψ.comp f₁) (f₂.comp φ)) (hg : Eq (ψ.comp g₁) (g₂.comp φ)) (hφ : φ.NormNoninc) : (map φ ψ hf hg).NormNoninc

theorem NormedAddGroupHom.Equalizer.norm_map_le {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {W₁ : Type u_6} {W₂ : Type u_7} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] {f₁ g₁ : NormedAddGroupHom V₁ W₁} {f₂ g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} (hf : Eq (ψ.comp f₁) (f₂.comp φ)) (hg : Eq (ψ.comp g₁) (g₂.comp φ)) (C : Real) (hφ : LE.le (Norm.norm (φ.comp (ι f₁ g₁))) C) : LE.le (Norm.norm (map φ ψ hf hg)) C