Quotients of seminormed groups #
For any SeminormedAddCommGroup M
and any S : AddSubgroup M
, we provide a
SeminormedAddCommGroup
, the group quotient M ⧸ S
.
If S
is closed, we provide NormedAddCommGroup (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 nonincreasing
(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 IsQuotient
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 SeminormedAddCommGroup
and NormedAddCommGroup
instances described above are transferred directly, but we also define instances of NormedSpace
,
SeminormedCommRing
, NormedCommRing
and NormedAlgebra
under appropriate type class
assumptions on the original space. Moreover, while QuotientAddGroup.completeSpace
works
outofthebox for quotients of NormedAddCommGroup
s by AddSubgroup
s, we need to transfer
this instance in Submodule.Quotient.completeSpace
so that it applies to these other quotients.
Main definitions #
We use M
and N
to denote seminormed groups and S : AddSubgroup M
.
All the following definitions are in the AddSubgroup
namespace. Hence we can access
AddSubgroup.normedMk S
as S.normedMk
.

seminormedAddCommGroupQuotient
: The seminormed group structure on the quotient by an additive subgroup. This is an instance so there is no need to explicitly use it. 
normedAddCommGroupQuotient
: The normed group structure on the quotient by a closed additive subgroup. This is an instance so there is no need to explicitly use it. 
normedMk S
: the normed group hom fromM
toM ⧸ S
. 
lift S f hf
: implements the universal property ofM ⧸ S
. Here(f : NormedAddGroupHom M N)
,(hf : ∀ s ∈ S, f s = 0)
andlift S f hf : NormedAddGroupHom (M ⧸ S) N
. 
IsQuotient
: givenf : NormedAddGroupHom M N
,IsQuotient 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_normedMk
: the operator norm of the projection is1
if the subspace is not dense. 
IsQuotient.norm_lift
: Providedf : normed_hom M N
satisfiesIsQuotient f
, for everyn : N
and positiveε
, there existsm
such thatf m = n ∧ ‖m‖ < ‖n‖ + ε
.
Implementation details #
For any SeminormedAddCommGroup M
and any S : AddSubgroup M
we define a norm on M ⧸ S
by
‖x‖ = sInf (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 SeminormedAddCommGroup
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 is settled, we have two topologies that are propositionally 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 SeminormedAddCommGroup
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 TopologicalAddGroup.toUniformSpace
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.
An alternative definition of the norm on the quotient group: the norm of ((x : M) : M ⧸ S)
is
equal to the distance from x
to S
.
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 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.
The quotient in the category of normed groups.
The morphism from a seminormed group to the quotient by a subgroup.
Instances For
S.normedMk
agrees with QuotientAddGroup.mk' S
.
S.normedMk
is surjective.
The kernel of S.normedMk
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
IsQuotient f
, for f : M ⟶ N
means that N
is isomorphic to the quotient of M
by the kernel of f
.
Instances For
Given f : NormedAddGroupHom M N
such that f s = 0
for all s ∈ S
, where,
S : AddSubgroup M
is closed, the induced morphism NormedAddGroupHom (M ⧸ S) N
.
Instances For
S.normedMk
satisfies IsQuotient
.
Submodules and ideals #
In what follows, the norm structures created above for quotients of (semi)NormedAddCommGroup
s
by AddSubgroup
s 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 NormedSpace
, SeminormedCommRing
,
NormedCommRing
and NormedAlgebra
under the appropriate hypotheses. Currently, we do not
have quotients of rings by twosided ideals, hence the commutativity hypotheses are required.
For any x : M ⧸ S
and any 0 < ε
, there is m : M
such that Submodule.Quotient.mk m = x
and ‖m‖ < ‖x‖ + ε
.