mathlib3documentation

analysis.normed.group.quotient

Quotients of seminormed groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For any seminormed_add_comm_group M and any S : add_subgroup M, we provide a seminormed_add_comm_group, the group quotient M ⧸ S. If S is closed, we provide normed_add_comm_group (M ⧸ S) (regardless of whether M itself is separated). The two main properties of these structures are the underlying topology is the quotient topology and the projection is a normed group homomorphism which is norm non-increasing (better, it has operator norm exactly one unless S is dense in M). The corresponding universal property is that every normed group hom defined on M which vanishes on S descends to a normed group hom defined on M ⧸ S.

This file also introduces a predicate is_quotient characterizing normed group homs that are isomorphic to the canonical projection onto a normed group quotient.

In addition, this file also provides normed structures for quotients of modules by submodules, and of (commutative) rings by ideals. The seminormed_add_comm_group and normed_add_comm_group instances described above are transferred directly, but we also define instances of normed_space, semi_normed_comm_ring, normed_comm_ring and normed_algebra under appropriate type class assumptions on the original space. Moreover, while quotient_add_group.complete_space works out-of-the-box for quotients of normed_add_comm_groups by add_subgroups, we need to transfer this instance in submodule.quotient.complete_space so that it applies to these other quotients.

Main definitions #

We use M and N to denote seminormed groups and S : add_subgroup M. All the following definitions are in the add_subgroup namespace. Hence we can access add_subgroup.normed_mk S as S.normed_mk.

• seminormed_add_comm_group_quotient : The seminormed group structure on the quotient by an additive subgroup. This is an instance so there is no need to explictly use it.

• normed_add_comm_group_quotient : The normed group structure on the quotient by a closed additive subgroup. This is an instance so there is no need to explictly use it.

• normed_mk S : the normed group hom from M to M ⧸ S.

• lift S f hf: implements the universal property of M ⧸ S. Here (f : normed_add_group_hom M N), (hf : ∀ s ∈ S, f s = 0) and lift S f hf : normed_add_group_hom (M ⧸ S) N.

• is_quotient: given f : normed_add_group_hom M N, is_quotient f means N is isomorphic to a quotient of M by a subgroup, with projection f. Technically it asserts f is surjective and the norm of f x is the infimum of the norms of x + m for m in f.ker.

Main results #

• norm_normed_mk : the operator norm of the projection is 1 if the subspace is not dense.

• is_quotient.norm_lift: Provided f : normed_hom M N satisfies is_quotient f, for every n : N and positive ε, there exists m such that f m = n ∧ ‖m‖ < ‖n‖ + ε.

Implementation details #

For any seminormed_add_comm_group M and any S : add_subgroup M we define a norm on M ⧸ S by ‖x‖ = Inf (norm '' {m | mk' S m = x}). This formula is really an implementation detail, it shouldn't be needed outside of this file setting up the theory.

Since M ⧸ S is automatically a topological space (as any quotient of a topological space), one needs to be careful while defining the seminormed_add_comm_group instance to avoid having two different topologies on this quotient. This is not purely a technological issue. Mathematically there is something to prove. The main point is proved in the auxiliary lemma quotient_nhd_basis that has no use beyond this verification and states that zero in the quotient admits as basis of neighborhoods in the quotient topology the sets {x | ‖x‖ < ε} for positive ε.

Once this mathematical point it settled, we have two topologies that are propositionaly equal. This is not good enough for the type class system. As usual we ensure definitional equality using forgetful inheritance, see Note [forgetful inheritance]. A (semi)-normed group structure includes a uniform space structure which includes a topological space structure, together with propositional fields asserting compatibility conditions. The usual way to define a seminormed_add_comm_group is to let Lean build a uniform space structure using the provided norm, and then trivially build a proof that the norm and uniform structure are compatible. Here the uniform structure is provided using topological_add_group.to_uniform_space which uses the topological structure and the group structure to build the uniform structure. This uniform structure induces the correct topological structure by construction, but the fact that it is compatible with the norm is not obvious; this is where the mathematical content explained in the previous paragraph kicks in.

@[protected, instance]
noncomputable def norm_on_quotient {M : Type u_1} (S : add_subgroup M) :

The definition of the norm on the quotient by an additive subgroup.

Equations
theorem add_subgroup.quotient_norm_eq {M : Type u_1} {S : add_subgroup M} (x : M S) :
theorem image_norm_nonempty {M : Type u_1} {S : add_subgroup M} (x : M S) :
(has_norm.norm '' {m : M | = x}).nonempty
theorem bdd_below_image_norm {M : Type u_1} (s : set M) :
theorem quotient_norm_neg {M : Type u_1} {S : add_subgroup M} (x : M S) :

The norm on the quotient satisfies ‖-x‖ = ‖x‖.

theorem quotient_norm_sub_rev {M : Type u_1} {S : add_subgroup M} (x y : M S) :
x - y = y - x
theorem quotient_norm_mk_le {M : Type u_1} (S : add_subgroup M) (m : M) :

The norm of the projection is smaller or equal to the norm of the original element.

theorem quotient_norm_mk_le' {M : Type u_1} (S : add_subgroup M) (m : M) :

The norm of the projection is smaller or equal to the norm of the original element.

theorem quotient_norm_mk_eq {M : Type u_1} (S : add_subgroup M) (m : M) :
= has_Inf.Inf ((λ (x : M), m + x) '' S)

The norm of the image under the natural morphism to the quotient.

theorem quotient_norm_nonneg {M : Type u_1} (S : add_subgroup M) (x : M S) :

The quotient norm is nonnegative.

theorem norm_mk_nonneg {M : Type u_1} (S : add_subgroup M) (m : M) :
0

The quotient norm is nonnegative.

theorem quotient_norm_eq_zero_iff {M : Type u_1} (S : add_subgroup M) (m : M) :
= 0 m

The norm of the image of m : M in the quotient by S is zero if and only if m belongs to the closure of S.

theorem norm_mk_lt {M : Type u_1} {S : add_subgroup M} (x : M S) {ε : } (hε : 0 < ε) :
(m : M), = x m < x + ε

For any x : M ⧸ S and any 0 < ε, there is m : M such that mk' S m = x and ‖m‖ < ‖x‖ + ε.

theorem norm_mk_lt' {M : Type u_1} (S : add_subgroup M) (m : M) {ε : } (hε : 0 < ε) :
(s : M) (H : s S), m + s < + ε

For any m : M and any 0 < ε, there is s ∈ S such that ‖m + s‖ < ‖mk' S m‖ + ε.

theorem quotient_norm_add_le {M : Type u_1} (S : add_subgroup M) (x y : M S) :

The quotient norm satisfies the triangle inequality.

theorem norm_mk_zero {M : Type u_1} (S : add_subgroup M) :

The quotient norm of 0 is 0.

theorem norm_zero_eq_zero {M : Type u_1} (S : add_subgroup M) (hS : is_closed S) (m : M) (h : = 0) :
m S

If (m : M) has norm equal to 0 in M ⧸ S for a closed subgroup S of M, then m ∈ S.

theorem quotient_nhd_basis {M : Type u_1} (S : add_subgroup M) :
(nhds 0).has_basis (λ (ε : ), 0 < ε) (λ (ε : ), {x : M S | x < ε})
@[protected, instance]

The seminormed group structure on the quotient by an additive subgroup.

Equations
@[protected, instance]

The quotient in the category of normed groups.

Equations
(M S)

The morphism from a seminormed group to the quotient by a subgroup.

Equations
@[simp]
theorem add_subgroup.normed_mk.apply {M : Type u_1} (S : add_subgroup M) (m : M) :

S.normed_mk agrees with quotient_add_group.mk' S.

S.normed_mk is surjective.

The kernel of S.normed_mk is S.

The operator norm of the projection is at most 1.

The operator norm of the projection is 1 if the subspace is not dense.

The operator norm of the projection is 0 if the subspace is dense.

structure normed_add_group_hom.is_quotient {M : Type u_1} {N : Type u_2} (f : N) :
Prop

is_quotient f, for f : M ⟶ N means that N is isomorphic to the quotient of M by the kernel of f.

def normed_add_group_hom.lift {M : Type u_1} {N : Type u_2} (S : add_subgroup M) (f : N) (hf : (s : M), s S f s = 0) :

Given f : normed_add_group_hom M N such that f s = 0 for all s ∈ S, where, S : add_subgroup M is closed, the induced morphism normed_add_group_hom (M ⧸ S) N.

Equations
theorem normed_add_group_hom.lift_mk {M : Type u_1} {N : Type u_2} (S : add_subgroup M) (f : N) (hf : (s : M), s S f s = 0) (m : M) :
hf) ((S.normed_mk) m) = f m
theorem normed_add_group_hom.lift_unique {M : Type u_1} {N : Type u_2} (S : add_subgroup M) (f : N) (hf : (s : M), s S f s = 0) (g : normed_add_group_hom (M S) N) :
g.comp S.normed_mk = f g =

S.normed_mk satisfies is_quotient.

theorem normed_add_group_hom.is_quotient.norm_lift {M : Type u_1} {N : Type u_2} {f : N} (hquot : f.is_quotient) {ε : } (hε : 0 < ε) (n : N) :
(m : M), f m = n m < n + ε
theorem normed_add_group_hom.is_quotient.norm_le {M : Type u_1} {N : Type u_2} {f : N} (hquot : f.is_quotient) (m : M) :
theorem normed_add_group_hom.lift_norm_le {M : Type u_1} {N : Type u_2} (S : add_subgroup M) (f : N) (hf : (s : M), s S f s = 0) {c : nnreal} (fb : f c) :
theorem normed_add_group_hom.lift_norm_noninc {M : Type u_1} {N : Type u_2} (S : add_subgroup M) (f : N) (hf : (s : M), s S f s = 0) (fb : f.norm_noninc) :

Submodules and ideals #

In what follows, the norm structures created above for quotients of (semi)normed_add_comm_groups by add_subgroups are transferred via definitional equality to quotients of modules by submodules, and of rings by ideals, thereby preserving the definitional equality for the topological group and uniform structures worked for above. Completeness is also transferred via this definitional equality.

In addition, instances are constructed for normed_space, semi_normed_comm_ring, normed_comm_ring and normed_algebra under the appropriate hypotheses. Currently, we do not have quotients of rings by two-sided ideals, hence the commutativity hypotheses are required.

@[protected, instance]
noncomputable def submodule.quotient.seminormed_add_comm_group {M : Type u_1} {R : Type u_3} [ring R] [ M] (S : M) :
Equations
@[protected, instance]
noncomputable def submodule.quotient.normed_add_comm_group {M : Type u_1} {R : Type u_3} [ring R] [ M] (S : M) [hS : is_closed S] :
Equations
@[protected, instance]
def submodule.quotient.complete_space {M : Type u_1} {R : Type u_3} [ring R] [ M] (S : M)  :
theorem submodule.quotient.norm_mk_lt {M : Type u_1} {R : Type u_3} [ring R] [ M] {S : M} (x : M S) {ε : } (hε : 0 < ε) :
(m : M), m < x + ε

For any x : M ⧸ S and any 0 < ε, there is m : M such that submodule.quotient.mk m = x and ‖m‖ < ‖x‖ + ε.

theorem submodule.quotient.norm_mk_le {M : Type u_1} {R : Type u_3} [ring R] [ M] (S : M) (m : M) :
@[protected, instance]
def submodule.quotient.normed_space {M : Type u_1} {R : Type u_3} [ring R] [ M] (S : M) (𝕜 : Type u_2) [normed_field 𝕜] [ M] [ R] [ M] :
(M S)
Equations
theorem ideal.quotient.norm_mk_lt {R : Type u_3} {I : ideal R} (x : R I) {ε : } (hε : 0 < ε) :
(r : R), r = x r < x + ε
theorem ideal.quotient.norm_mk_le {R : Type u_3} (I : ideal R) (r : R) :
@[protected, instance]
noncomputable def ideal.quotient.semi_normed_comm_ring {R : Type u_3} (I : ideal R) :
Equations
@[protected, instance]
noncomputable def ideal.quotient.normed_comm_ring {R : Type u_3} (I : ideal R) [is_closed I] :
Equations
@[protected, instance]
noncomputable def ideal.quotient.normed_algebra {R : Type u_3} (I : ideal R) (𝕜 : Type u_4) [normed_field 𝕜] [ R] :
(R I)
Equations