Quotients of seminormed groups #
For any semi_normed_group M
and any S : add_subgroup M
, we provide a semi_normed_group
the group quotient M ⧸ S
.
If S
is closed, we provide normed_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.
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 fromM
toM ⧸ S
. -
lift S f hf
: implements the universal property ofM ⧸ S
. Here(f : normed_group_hom M N)
,(hf : ∀ s ∈ S, f s = 0)
andlift S f hf : normed_group_hom (M ⧸ S) N
. -
is_quotient
: givenf : normed_group_hom M N
,is_quotient f
meansN
is isomorphic to a quotient ofM
by a subgroup, with projectionf
. Technically it assertsf
is surjective and the norm off x
is the infimum of the norms ofx + m
form
inf.ker
.
Main results #
-
norm_normed_mk
: the operator norm of the projection is1
if the subspace is not dense. -
is_quotient.norm_lift
: Providedf : normed_hom M N
satisfiesis_quotient f
, for everyn : N
and positiveε
, there existsm
such thatf m = n ∧ ∥m∥ < ∥n∥ + ε
.
Implementation details #
For any semi_normed_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 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.
The definition of the norm on the quotient by an additive subgroup.
Equations
- norm_on_quotient S = {norm := λ (x : M ⧸ S), has_Inf.Inf (has_norm.norm '' {m : M | ⇑(quotient_add_group.mk' S) m = x})}
The norm on the quotient satisfies ∥-x∥ = ∥x∥
.
The norm of the projection is smaller or equal to the norm of the original element.
The norm of the projection is smaller or equal to the norm of the original element.
The norm of the image under the natural morphism to the quotient.
The quotient norm is nonnegative.
The quotient norm is nonnegative.
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
.
For any x : M ⧸ S
and any 0 < ε
, there is m : M
such that mk' S m = x
and ∥m∥ < ∥x∥ + ε
.
For any m : M
and any 0 < ε
, there is s ∈ S
such that ∥m + s∥ < ∥mk' S m∥ + ε
.
The quotient norm satisfies the triangle inequality.
The quotient norm of 0
is 0
.
If (m : M)
has norm equal to 0
in M ⧸ S
for a closed subgroup S
of M
, then
m ∈ S
.
The seminormed group structure on the quotient by an additive subgroup.
Equations
- S.semi_normed_group_quotient = {to_has_norm := norm_on_quotient S, to_add_comm_group := quotient_add_group.add_comm_group S, to_pseudo_metric_space := {to_has_dist := {dist := λ (x y : M ⧸ S), ∥x - y∥}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : M ⧸ S), ↑⟨(λ (x y : M ⧸ S), ∥x - y∥) x y, _⟩, edist_dist := _, to_uniform_space := topological_add_group.to_uniform_space (M ⧸ S) _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : M ⧸ S), ∥x - y∥) _ quotient_norm_sub_rev _, cobounded_sets := _}, dist_eq := _}
The quotient in the category of normed groups.
Equations
- S.normed_group_quotient = {to_has_norm := semi_normed_group.to_has_norm S.semi_normed_group_quotient, to_add_comm_group := semi_normed_group.to_add_comm_group S.semi_normed_group_quotient, to_metric_space := {to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space S.semi_normed_group_quotient, eq_of_dist_eq_zero := _}, dist_eq := _}
The morphism from a seminormed group to the quotient by a subgroup.
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.
- surjective : function.surjective ⇑f
- norm : ∀ (x : M), ∥⇑f x∥ = has_Inf.Inf ((λ (m : M), ∥x + m∥) '' ↑(f.ker))
is_quotient f
, for f : M ⟶ N
means that N
is isomorphic to the quotient of M
by the kernel of f
.
Given f : normed_group_hom M N
such that f s = 0
for all s ∈ S
, where,
S : add_subgroup M
is closed, the induced morphism normed_group_hom (M ⧸ S) N
.
Equations
- normed_group_hom.lift S f hf = {to_fun := (quotient_add_group.lift S f.to_add_monoid_hom hf).to_fun, map_add' := _, bound' := _}
S.normed_mk
satisfies is_quotient
.