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), 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.

def AddMonoidHom.mkNormedAddGroupHom {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f : V →+ W) (C : ℝ) (h : ∀ (v : V), ‖f v‖ ≤ C * ‖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

• 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 : V →+ W) (C : NNReal) (hC : ∀ (x : V), ‖f x‖₊ ≤ C * ‖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

• 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 : ℝ) (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {K : NNReal} (h : LipschitzWith K ⇑f) : NormedAddGroupHom V₁ V₂

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

Equations

• NormedAddGroupHom.ofLipschitz f h = f.mkNormedAddGroupHom ↑K ⋯

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

Equations

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

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

Equations

• ⋯ = ⋯

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

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

theorem NormedAddGroupHom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f g : NormedAddGroupHom V₁ V₂} : f = g ↔ ⇑f = ⇑g

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

@[simp]

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

theorem NormedAddGroupHom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : V₁ →+ V₂

The group homomorphism underlying a bounded group homomorphism.

Equations

• f.toAddMonoidHom = AddMonoidHom.mk' ⇑f ⋯

@[simp]

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

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

@[simp]

theorem NormedAddGroupHom.mk_toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (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 = AddMonoidHom.mk' f h₁

theorem NormedAddGroupHom.bound {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : V₁), ‖f x‖ ≤ C * ‖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₁), ‖x‖ ≤ ↑K * ‖f x‖) : AntilipschitzWith K ⇑f

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

Equations

• f.SurjectiveOnWith K C = ∀ h ∈ K, ∃ (g : V₁), f g = h ∧ ‖g‖ ≤ C * ‖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' : ℝ} (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : ℝ} (h : f.SurjectiveOnWith K C) : ∃ 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 : ℝ} (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : ℝ

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

Equations

• f.opNorm = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}

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

Equations

• 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₂) : ‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}

theorem NormedAddGroupHom.bounds_nonempty {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} : ∃ (c : ℝ), c ∈ {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}

theorem NormedAddGroupHom.bounds_bddBelow {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} : BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}

theorem NormedAddGroupHom.opNorm_nonneg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : 0 ≤ ‖f‖

theorem NormedAddGroupHom.le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (x : V₁) : ‖f x‖ ≤ ‖f‖ * ‖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 : ℝ} {x : V₁} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖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 : ℝ} (h : ‖f‖ ≤ c) (x : V₁) : ‖f x‖ ≤ c * ‖x‖

theorem NormedAddGroupHom.lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : LipschitzWith ⟨‖f‖, ⋯⟩ ⇑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 ⇑f

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

theorem NormedAddGroupHom.ratio_le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (x : V₁) : ‖f x‖ / ‖x‖ ≤ ‖f‖

theorem NormedAddGroupHom.opNorm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖) : ‖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 : ℝ} (M_nonneg : 0 ≤ M) (h_above : ∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖) (h_below : ∀ N ≥ 0, (∀ (x : V₁), ‖f x‖ ≤ N * ‖x‖) → M ≤ N) : ‖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 ⇑f) : ‖f‖ ≤ ↑K

theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {K : NNReal} (h : LipschitzWith K ⇑f) : ‖NormedAddGroupHom.ofLipschitz f h‖ ≤ ↑K

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 : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖) : ‖f.mkNormedAddGroupHom C h‖ ≤ 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 : 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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖) : ‖f.mkNormedAddGroupHom C h‖ ≤ 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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Add (NormedAddGroupHom V₁ V₂)

Addition of normed group homs.

Equations

• NormedAddGroupHom.add = { add := fun (f g : NormedAddGroupHom V₁ V₂) => (f.toAddMonoidHom + g.toAddMonoidHom).mkNormedAddGroupHom (‖f‖ + ‖g‖) ⋯ }

theorem NormedAddGroupHom.opNorm_add_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) : ‖f + g‖ ≤ ‖f‖ + ‖g‖

The operator norm satisfies the triangle inequality.

@[simp]

theorem NormedAddGroupHom.coe_add {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem NormedAddGroupHom.add_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Zero (NormedAddGroupHom V₁ V₂)

Equations

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

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

Equations

• NormedAddGroupHom.inhabited = { default := 0 }

theorem NormedAddGroupHom.opNorm_zero {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : ‖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₂} : ‖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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : ⇑0 = 0

@[simp]

theorem NormedAddGroupHom.zero_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (v : V₁) : 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

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

@[simp]

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

theorem NormedAddGroupHom.norm_id_le (V : Type u_1) [SeminormedAddCommGroup V] : ‖NormedAddGroupHom.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 : ∃ (x : V), ‖x‖ ≠ 0) : ‖NormedAddGroupHom.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] : ‖NormedAddGroupHom.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] : ⇑(NormedAddGroupHom.id V) = id

The negation of a normed group hom

instance 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

• NormedAddGroupHom.neg = { neg := fun (f : NormedAddGroupHom V₁ V₂) => (-f.toAddMonoidHom).mkNormedAddGroupHom ‖f‖ ⋯ }

@[simp]

theorem NormedAddGroupHom.coe_neg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : ⇑(-f) = -⇑f

@[simp]

theorem NormedAddGroupHom.neg_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) : (-f) v = -f v

theorem NormedAddGroupHom.opNorm_neg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : ‖-f‖ = ‖f‖

Subtraction of normed group homs

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

Subtraction of normed group homs.

Equations

• NormedAddGroupHom.sub = { sub := fun (f g : NormedAddGroupHom V₁ V₂) => 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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem NormedAddGroupHom.sub_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f g : NormedAddGroupHom V₁ V₂) (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] : SMul R (NormedAddGroupHom V₁ V₂)

Equations

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

@[simp]

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] [BoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) : ⇑(r • f) = r • ⇑f

@[simp]

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] [BoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) (v : V₁) : (r • f) v = r • f v

instance 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] [BoundedSMul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R'] [BoundedSMul R' V₂] [SMulCommClass R R' V₂] : SMulCommClass R R' (NormedAddGroupHom V₁ V₂)

Equations

• ⋯ = ⋯

instance 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] [BoundedSMul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R'] [BoundedSMul R' V₂] [SMul R R'] [IsScalarTower R R' V₂] : IsScalarTower R R' (NormedAddGroupHom V₁ V₂)

Equations

• ⋯ = ⋯

instance 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] [BoundedSMul R V₂] [DistribMulAction Rᵐᵒᵖ V₂] [IsCentralScalar R V₂] : IsCentralScalar R (NormedAddGroupHom V₁ V₂)

Equations

• ⋯ = ⋯

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

Equations

• NormedAddGroupHom.nsmul = { smul := fun (n : ℕ) (f : NormedAddGroupHom V₁ V₂) => { toFun := n • ⇑f, map_add' := ⋯, bound' := ⋯ } }

@[simp]

theorem NormedAddGroupHom.coe_nsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ℕ) (f : NormedAddGroupHom V₁ V₂) : ⇑(r • f) = r • ⇑f

@[simp]

theorem NormedAddGroupHom.nsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ℕ) (f : NormedAddGroupHom V₁ V₂) (v : V₁) : (r • f) v = r • f v

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

Equations

• NormedAddGroupHom.zsmul = { smul := fun (z : ℤ) (f : NormedAddGroupHom V₁ V₂) => { toFun := z • ⇑f, map_add' := ⋯, bound' := ⋯ } }

@[simp]

theorem NormedAddGroupHom.coe_zsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ℤ) (f : NormedAddGroupHom V₁ V₂) : ⇑(r • f) = r • ⇑f

@[simp]

theorem NormedAddGroupHom.zsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ℤ) (f : NormedAddGroupHom V₁ V₂) (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : AddCommGroup (NormedAddGroupHom V₁ V₂)

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

Equations

• NormedAddGroupHom.toAddCommGroup = Function.Injective.addCommGroup NormedAddGroupHom.toFun ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance 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

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

instance 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

• 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₂] : NormedAddGroupHom V₁ V₂ →+ V₁ → V₂

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

Equations

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

@[simp]

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

@[simp]

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₂) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(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₁) : (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v

Module structure on normed group homs

instance 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] [BoundedSMul R V₂] : DistribMulAction R (NormedAddGroupHom V₁ V₂)

Equations

• NormedAddGroupHom.distribMulAction = Function.Injective.distribMulAction NormedAddGroupHom.coeAddHom ⋯ ⋯

instance 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] [BoundedSMul R V₂] : Module R (NormedAddGroupHom V₁ V₂)

Equations

• 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

• g.comp f = (g.toAddMonoidHom.comp f.toAddMonoidHom).mkNormedAddGroupHom (‖g‖ * ‖f‖) ⋯

@[simp]

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₁) : (g.comp f) a✝ = g (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₂) : ‖g.comp f‖ ≤ ‖g‖ * ‖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₂ : ℝ} (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₂ V₃} (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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] : NormedAddGroupHom V₂ V₃ →+ NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃

Composition of normed groups hom as an additive group morphism.

Equations

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

@[simp]

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₃) : f.comp 0 = 0

@[simp]

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₂) : 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₂) : (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₃) : ⇑(g.comp f) = ⇑g ∘ ⇑f

def NormedAddGroupHom.incl {V : Type u_1} [SeminormedAddCommGroup V] (s : AddSubgroup V) : NormedAddGroupHom (↥s) V

The inclusion of an AddSubgroup, as bounded group homomorphism.

Equations

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

@[simp]

theorem NormedAddGroupHom.incl_apply {V : Type u_1} [SeminormedAddCommGroup V] (s : AddSubgroup V) (self : ↥s) : (NormedAddGroupHom.incl s) self = ↑self

theorem NormedAddGroupHom.norm_incl {V : Type u_1} [SeminormedAddCommGroup V] {V' : AddSubgroup V} (x : ↥V') : ‖(NormedAddGroupHom.incl V') x‖ = ‖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

• 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₁) : v ∈ f.ker ↔ 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 : g.comp f = 0) : NormedAddGroupHom 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.

Equations

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

@[simp]

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 : g.comp f = 0) (v : V₁) : ↑((NormedAddGroupHom.ker.lift f g h) v) = f v

@[simp]

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 : g.comp f = 0) : (NormedAddGroupHom.incl g.ker).comp (NormedAddGroupHom.ker.lift f g h) = f

@[simp]

theorem NormedAddGroupHom.ker_zero {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : NormedAddGroupHom.ker 0 = ⊤

theorem NormedAddGroupHom.coe_ker {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : ↑f.ker = ⇑f ⁻¹' {0}

theorem NormedAddGroupHom.isClosed_ker {V₁ : Type u_3} [SeminormedAddCommGroup V₁] {V₂ : Type u_6} [NormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : IsClosed ↑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

• 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₂) : v ∈ f.range ↔ ∃ (w : V₁), f w = v

@[simp]

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

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₃) : (g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range

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

@[simp]

theorem NormedAddGroupHom.range_comp_incl_top {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : (f.comp (NormedAddGroupHom.incl ⊤)).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

• f.NormNoninc = ∀ (v : V), ‖f v‖ ≤ ‖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} : f.NormNoninc ↔ ‖f‖ ≤ 1

theorem NormedAddGroupHom.NormNoninc.zero {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : NormedAddGroupHom.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

@[simp]

theorem NormedAddGroupHom.NormNoninc.neg_iff {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} : (-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 ⇑f) (v : V) : ‖f v‖ = ‖v‖

theorem NormedAddGroupHom.isometry_id {V : Type u_1} [SeminormedAddCommGroup V] : Isometry ⇑(NormedAddGroupHom.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 ⇑g) (hf : Isometry ⇑f) : Isometry ⇑(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 ⇑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

• f.equalizer g = (f - g).ker

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

The inclusion of f.equalizer g as a NormedAddGroupHom.

Equations

• 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) : f.comp (NormedAddGroupHom.Equalizer.ι f g) = g.comp (NormedAddGroupHom.Equalizer.ι 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 : 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

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

@[simp]

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 : f.comp φ = g.comp φ) (v : V₁) : ↑((NormedAddGroupHom.Equalizer.lift φ h) v) = φ v

@[simp]

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 : f.comp φ = g.comp φ) : (NormedAddGroupHom.Equalizer.ι f g).comp (NormedAddGroupHom.Equalizer.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} : { φ : NormedAddGroupHom V₁ V // 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.

@[simp]

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} (φ : { φ : NormedAddGroupHom V₁ V // f.comp φ = g.comp φ }) : NormedAddGroupHom.Equalizer.liftEquiv φ = NormedAddGroupHom.Equalizer.lift ↑φ ⋯

@[simp]

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₁ ↥(f.equalizer g)) : ↑(NormedAddGroupHom.Equalizer.liftEquiv.symm ψ) = (NormedAddGroupHom.Equalizer.ι f g).comp ψ

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 : ψ.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

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

@[simp]

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 : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) : (NormedAddGroupHom.Equalizer.ι f₂ g₂).comp (NormedAddGroupHom.Equalizer.map φ ψ hf hg) = φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)

@[simp]

theorem NormedAddGroupHom.Equalizer.map_id {V₁ : Type u_3} [SeminormedAddCommGroup V₁] {W₁ : Type u_6} [SeminormedAddCommGroup W₁] {f₁ g₁ : NormedAddGroupHom V₁ W₁} : NormedAddGroupHom.Equalizer.map (NormedAddGroupHom.id V₁) (NormedAddGroupHom.id W₁) ⋯ ⋯ = NormedAddGroupHom.id ↥(f₁.equalizer g₁)

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 : ψ.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} [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 : ψ.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 φ ψ hf hg) = NormedAddGroupHom.Equalizer.map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯

theorem NormedAddGroupHom.Equalizer.ι_normNoninc {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f g : NormedAddGroupHom V W} : (NormedAddGroupHom.Equalizer.ι 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 : f.comp φ = g.comp φ) (hφ : φ.NormNoninc) : (NormedAddGroupHom.Equalizer.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 : f.comp φ = g.comp φ) (C : ℝ) (hφ : ‖φ‖ ≤ C) : ‖NormedAddGroupHom.Equalizer.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 : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hφ : φ.NormNoninc) : (NormedAddGroupHom.Equalizer.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 : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (C : ℝ) (hφ : ‖φ.comp (NormedAddGroupHom.Equalizer.ι f₁ g₁)‖ ≤ C) : ‖NormedAddGroupHom.Equalizer.map φ ψ hf hg‖ ≤ C