Lifts of maps to separation quotients of seminormed groups

For any SeminormedAddCommGroup M, a NormedAddCommGroup instance has been defined in Mathlib/Analysis/Normed/Group/Uniform.lean.

Main definitions

We use M and N to denote seminormed groups. All the following definitions are in the SeparationQuotient namespace. Hence we can access SeparationQuotient.normedMk as normedMk.

• normedMk : the normed group hom from M to SeparationQuotient M.

• liftNormedAddGroupHom : any bounded group hom f : M → N such that ∀ x, ‖x‖ = 0 → f x = 0 descends to a bounded group hom SeparationQuotient M → N. Here, (f : NormedAddGroupHom M N), (hf : ∀ x : M, ‖x‖ = 0 → f x = 0) and liftNormedAddGroupHom f hf : NormedAddGroupHom (SeparationQuotient M) N such that liftNormedAddGroupHom f hf (mk x) = f x.

Main results

• norm_normedMk_eq_one : the operator norm of the projection is 1if the subspace is not⊤`.

• norm_liftNormedAddGroupHom_le : ‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖.

noncomputable def SeparationQuotient.normedMk {M : Type u_1} [SeminormedAddCommGroup M] : NormedAddGroupHom M (SeparationQuotient M)

The morphism from a seminormed group to the quotient by the inseparable setoid.

@[simp]

theorem SeparationQuotient.normedMk_apply {M : Type u_1} [SeminormedAddCommGroup M] (a✝ : M) : normedMk a✝ = (↑mkAddMonoidHom).toFun a✝

theorem SeparationQuotient.norm_normedMk_le {M : Type u_1} [SeminormedAddCommGroup M] : ‖normedMk‖ ≤ 1

The operator norm of the projection is at most 1.

theorem SeparationQuotient.apply_eq_apply_of_inseparable {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] {F : Type u_3} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (hf : ∀ (x : M), ‖x‖ = 0 → f x = 0) (x y : M) : Inseparable x y → f x = f y

noncomputable def SeparationQuotient.liftNormedAddGroupHom {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (hf : ∀ (x : M), ‖x‖ = 0 → f x = 0) : NormedAddGroupHom (SeparationQuotient M) N

The lift of a group hom to the separation quotient as a group hom.

@[simp]

theorem SeparationQuotient.liftNormedAddGroupHom_apply {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (hf : ∀ (x : M), ‖x‖ = 0 → f x = 0) (a : SeparationQuotient M) : (liftNormedAddGroupHom f hf) a = (liftContinuousAddMonoidHom ↑f ⋯) a

theorem SeparationQuotient.norm_liftNormedAddGroupHom_apply_le {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (hf : ∀ (x : M), ‖x‖ = 0 → f x = 0) (x : SeparationQuotient M) : ‖(liftNormedAddGroupHom f hf) x‖ ≤ ‖f‖ * ‖x‖

noncomputable def SeparationQuotient.liftNormedAddGroupHomEquiv {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] : { f : NormedAddGroupHom M N // ∀ (x : M), ‖x‖ = 0 → f x = 0 } ≃ NormedAddGroupHom (SeparationQuotient M) N

The equivalence between NormedAddGroupHom M N vanishing on the inseparable setoid and NormedAddGroupHom (SeparationQuotient M) N.

@[simp]

theorem SeparationQuotient.liftNormedAddGroupHomEquiv_symm_apply_coe {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (g : NormedAddGroupHom (SeparationQuotient M) N) : ↑(liftNormedAddGroupHomEquiv.symm g) = g.comp normedMk

@[simp]

theorem SeparationQuotient.liftNormedAddGroupHomEquiv_apply {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (f : { f : NormedAddGroupHom M N // ∀ (x : M), ‖x‖ = 0 → f x = 0 }) : liftNormedAddGroupHomEquiv f = liftNormedAddGroupHom ↑f ⋯

theorem SeparationQuotient.norm_liftNormedAddGroupHom_le {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0) : ‖liftNormedAddGroupHom f hf‖ ≤ ‖f‖

For a norm-continuous group homomorphism f, its lift to the separation quotient is bounded by the norm of f.

theorem SeparationQuotient.liftNormedAddGroupHom_norm_le {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0) {c : NNReal} (fb : ‖f‖ ≤ ↑c) : ‖liftNormedAddGroupHom f hf‖ ≤ ↑c

theorem SeparationQuotient.liftNormedAddGroupHom_normNoninc {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0) (fb : f.NormNoninc) : (liftNormedAddGroupHom f hf).NormNoninc

theorem SeparationQuotient.norm_normedMk_eq_one {M : Type u_1} [SeminormedAddCommGroup M] (h : ∃ (x : M), ‖x‖ ≠ 0) : ‖normedMk‖ = 1

The operator norm of the projection is 1 if there is an element whose norm is different from 0.

theorem SeparationQuotient.normedMk_eq_zero_iff {M : Type u_1} [SeminormedAddCommGroup M] : normedMk = 0 ↔ ∀ (x : M), ‖x‖ = 0

The projection is 0 if and only if all the elements have norm 0.