Quotients of seminormed groups #

For any semi_normed_group M and any S : add_subgroup M, we provide a semi_normed_group structure on quotient_add_group.quotient S (abreviated quotient S in the following). If S is closed, we provide normed_group (quotient 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 quotient 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.

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.

• semi_normed_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_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 quotient S.

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

• is_quotient: given f : normed_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 semi_normed_group M and any S : add_subgroup M we define a norm on quotient 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 quotient S is automatically a topological space (as any quotient of a topological space), one needs to be careful while defining the semi_normed_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 semi_normed_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.