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)

• toFun : V → W

  The function underlying a NormedAddGroupHom

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

  A NormedAddGroupHom is additive.

• bound' : ∃ C, ∀ (v : V), ‖NormedAddGroupHom.toFun s v‖ ≤ C * ‖v‖

  A NormedAddGroupHom is bounded.

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

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

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

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

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

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 = AddMonoidHom.mkNormedAddGroupHom f ↑K (_ : ∀ (x : V₁), ‖↑f x‖ ≤ ↑K * ‖x‖)

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

Equations

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

instance NormedAddGroupHom.coeFun {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : CoeFun (NormedAddGroupHom V₁ V₂) fun x => V₁ → V₂

Helper instance for when there are too many metavariables to apply FunLike.coeFun directly.

Equations

• NormedAddGroupHom.coeFun = { coe := FunLike.coe }

theorem NormedAddGroupHom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {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 : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₁ V₂} : f = g ↔ ↑f = ↑g

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

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

@[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' := (_ : ∃ C, ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖) } = 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‖) : ↑(AddMonoidHom.mkNormedAddGroupHom f 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‖₊) : ↑(AddMonoidHom.mkNormedAddGroupHom' f 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

• NormedAddGroupHom.toAddMonoidHom f = AddMonoidHom.mk' ↑f (_ : ∀ (v₁ v₂ : V₁), NormedAddGroupHom.toFun f (v₁ + v₂) = NormedAddGroupHom.toFun f v₁ + NormedAddGroupHom.toFun f v₂)

@[simp]

theorem NormedAddGroupHom.coe_toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) : ↑(NormedAddGroupHom.toAddMonoidHom f) = ↑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‖) : NormedAddGroupHom.toAddMonoidHom { toFun := f, map_add' := h₁, bound' := h₂ } = 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

• NormedAddGroupHom.SurjectiveOnWith f K C = ∀ (h : V₂), h ∈ K → ∃ g, ↑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 : NormedAddGroupHom.SurjectiveOnWith f K C) (H : C ≤ C') : NormedAddGroupHom.SurjectiveOnWith f 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 : NormedAddGroupHom.SurjectiveOnWith f K C) : ∃ C', C' > 0 ∧ NormedAddGroupHom.SurjectiveOnWith f 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 : NormedAddGroupHom.SurjectiveOnWith f 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

• NormedAddGroupHom.opNorm f = 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 { val := ‖f‖, property := (_ : 0 ≤ ‖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 : ℝ), 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‖) : ‖AddMonoidHom.mkNormedAddGroupHom f 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‖) : ‖AddMonoidHom.mkNormedAddGroupHom f 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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : V₁), ‖↑f x‖ ≤ C * ‖x‖) : ‖AddMonoidHom.mkNormedAddGroupHom f 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‖) : ‖AddMonoidHom.mkNormedAddGroupHom f 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} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] : Add (NormedAddGroupHom V₁ V₂)

Addition of normed group homs.

Equations

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

theorem NormedAddGroupHom.opNorm_add_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (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 : NormedAddGroupHom V₁ V₂) (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 : NormedAddGroupHom V₁ V₂) (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 (_ : ∀ (a : V₁), ‖0‖ ≤ 0 * ‖a‖) }

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

@[simp]

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

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.mkNormedAddGroupHom (AddMonoidHom.id V) 1 (_ : ∀ (a : V), ‖a‖ ≤ 1 * ‖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, ‖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 => AddMonoidHom.mkNormedAddGroupHom (-NormedAddGroupHom.toAddMonoidHom f) ‖f‖ (_ : ∀ (v : V₁), ‖-↑f v‖ ≤ ‖f‖ * ‖v‖) }

@[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

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

@[simp]

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

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

@[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

• @NormedAddGroupHom.smulCommClass = @NormedAddGroupHom.smulCommClass.proof_1

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

• @NormedAddGroupHom.isScalarTower = @NormedAddGroupHom.isScalarTower.proof_1

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

• @NormedAddGroupHom.isCentralScalar = @NormedAddGroupHom.isCentralScalar.proof_1

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

Equations

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

@[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

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

@[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

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

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

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

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

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

@[simp]

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

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 = { toZeroHom := { toFun := FunLike.coe, map_zero' := (_ : ↑0 = 0) }, map_add' := (_ : ∀ (f g : NormedAddGroupHom V₁ V₂), ↑(f + g) = ↑f + ↑g) }

@[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₂) : ↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(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₁) : ↑(Finset.sum s fun i => f i) v = Finset.sum s fun i => ↑(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

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

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

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

Composition of normed group homs

@[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₁), ↑(NormedAddGroupHom.comp g f) a = ↑g (↑f a)

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

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

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₂) : ‖NormedAddGroupHom.comp g 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₁) : ‖NormedAddGroupHom.comp g 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₁) : ‖NormedAddGroupHom.comp g 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

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

@[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₃) : NormedAddGroupHom.comp f 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₂) : NormedAddGroupHom.comp (NormedAddGroupHom.comp h g) f = NormedAddGroupHom.comp h (NormedAddGroupHom.comp g 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₃) : ↑(NormedAddGroupHom.comp g f) = ↑g ∘ ↑f

@[simp]

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

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

The inclusion of an AddSubgroup, as bounded group homomorphism.

Equations

• NormedAddGroupHom.incl s = { toFun := Subtype.val, map_add' := (_ : ∀ (v w : { x // x ∈ s }), ↑(v + w) = ↑v + ↑w), bound' := (_ : ∃ C, ∀ (v : { x // x ∈ s }), ‖↑v‖ ≤ C * ‖v‖) }

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

• NormedAddGroupHom.ker f = AddMonoidHom.ker (NormedAddGroupHom.toAddMonoidHom f)

theorem NormedAddGroupHom.mem_ker {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) : v ∈ NormedAddGroupHom.ker f ↔ ↑f v = 0

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

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 : NormedAddGroupHom.comp g f = 0) : NormedAddGroupHom V₁ { x // x ∈ NormedAddGroupHom.ker g }

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

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

@[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 : NormedAddGroupHom.comp g f = 0) : NormedAddGroupHom.comp (NormedAddGroupHom.incl (NormedAddGroupHom.ker g)) (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₂) : ↑(NormedAddGroupHom.ker f) = ↑f ⁻¹' {0}

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

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

• NormedAddGroupHom.range f = AddMonoidHom.range (NormedAddGroupHom.toAddMonoidHom f)

theorem NormedAddGroupHom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₂) : v ∈ NormedAddGroupHom.range f ↔ ∃ w, ↑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 ∈ NormedAddGroupHom.range f

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

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

@[simp]

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

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

• NormedAddGroupHom.NormNoninc f = ∀ (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} : NormedAddGroupHom.NormNoninc f ↔ ‖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.NormNoninc (NormedAddGroupHom.id V)

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 : NormedAddGroupHom.NormNoninc g) (hf : NormedAddGroupHom.NormNoninc f) : NormedAddGroupHom.NormNoninc (NormedAddGroupHom.comp g f)

@[simp]

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

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 ↑(NormedAddGroupHom.comp g 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) : NormedAddGroupHom.NormNoninc f

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

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

Equations

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

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

The inclusion of f.equalizer g as a NormedAddGroupHom.

Equations

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

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

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

def NormedAddGroupHom.Equalizer.lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f : NormedAddGroupHom V W} {g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V) (h : NormedAddGroupHom.comp f φ = NormedAddGroupHom.comp g φ) : NormedAddGroupHom V₁ { x // x ∈ NormedAddGroupHom.equalizer f g }

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

Equations

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

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

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

@[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 : NormedAddGroupHom V W} {g : NormedAddGroupHom V W} (ψ : NormedAddGroupHom V₁ { x // x ∈ NormedAddGroupHom.equalizer f g }) : ↑(↑NormedAddGroupHom.Equalizer.liftEquiv.symm ψ) = NormedAddGroupHom.comp (NormedAddGroupHom.Equalizer.ι f g) ψ

def NormedAddGroupHom.Equalizer.liftEquiv {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f : NormedAddGroupHom V W} {g : NormedAddGroupHom V W} : { φ // NormedAddGroupHom.comp f φ = NormedAddGroupHom.comp g φ } ≃ NormedAddGroupHom V₁ { x // x ∈ NormedAddGroupHom.equalizer f g }

The lifting property of the equalizer as an equivalence.

Equations

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

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₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} (φ : NormedAddGroupHom V₁ V₂) (ψ : NormedAddGroupHom W₁ W₂) (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) : NormedAddGroupHom { x // x ∈ NormedAddGroupHom.equalizer f₁ g₁ } { x // x ∈ NormedAddGroupHom.equalizer f₂ 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

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

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

@[simp]

theorem NormedAddGroupHom.Equalizer.map_id {V₁ : Type u_3} [SeminormedAddCommGroup V₁] {W₁ : Type u_6} [SeminormedAddCommGroup W₁] {f₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} : NormedAddGroupHom.Equalizer.map (NormedAddGroupHom.id V₁) (NormedAddGroupHom.id W₁) (_ : NormedAddGroupHom.comp (NormedAddGroupHom.id W₁) f₁ = NormedAddGroupHom.comp (NormedAddGroupHom.id W₁) f₁) (_ : NormedAddGroupHom.comp (NormedAddGroupHom.id W₁) g₁ = NormedAddGroupHom.comp (NormedAddGroupHom.id W₁) g₁) = NormedAddGroupHom.id { x // x ∈ NormedAddGroupHom.equalizer f₁ 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 : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ') : NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) f₁ = NormedAddGroupHom.comp f₃ (NormedAddGroupHom.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₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} {f₃ : NormedAddGroupHom V₃ W₃} {g₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃} (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) (hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ') (hg' : NormedAddGroupHom.comp ψ' g₂ = NormedAddGroupHom.comp g₃ φ') : NormedAddGroupHom.comp (NormedAddGroupHom.Equalizer.map φ' ψ' hf' hg') (NormedAddGroupHom.Equalizer.map φ ψ hf hg) = NormedAddGroupHom.Equalizer.map (NormedAddGroupHom.comp φ' φ) (NormedAddGroupHom.comp ψ' ψ) (_ : NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) f₁ = NormedAddGroupHom.comp f₃ (NormedAddGroupHom.comp φ' φ)) (_ : NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) g₁ = NormedAddGroupHom.comp g₃ (NormedAddGroupHom.comp φ' φ))

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

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

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 : NormedAddGroupHom V W} {g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V) (h : NormedAddGroupHom.comp f φ = NormedAddGroupHom.comp g φ) (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₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) (hφ : NormedAddGroupHom.NormNoninc φ) : NormedAddGroupHom.NormNoninc (NormedAddGroupHom.Equalizer.map φ ψ hf hg)

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₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) (C : ℝ) (hφ : ‖NormedAddGroupHom.comp φ (NormedAddGroupHom.Equalizer.ι f₁ g₁)‖ ≤ C) : ‖NormedAddGroupHom.Equalizer.map φ ψ hf hg‖ ≤ C