# 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 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 `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 out-of-the-box 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 from `M` to `M ⧸ S`.

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

- `IsQuotient`: given `f : NormedAddGroupHom M N`, `IsQuotient 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_normedMk` : the operator norm of the projection is `1` if the subspace is not dense.

- `IsQuotient.norm_lift`: Provided `f : normed_hom M N` satisfies `IsQuotient f`, for every `n : N` and positive `ε`, there exists `m` such that `f 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_nhds_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 `IsTopologicalAddGroup.rightUniformSpace` 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.

source
noncomputable def QuotientGroup.groupSeminorm {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} :
GroupSeminorm (M ⧸ S)

The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on `x * M`.

Equations

- QuotientGroup.groupSeminorm = { toFun := fun (x : M ⧸ S) => Metric.infDist 1 {m : M | ↑m = x}, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }

Instances For

source
noncomputable def QuotientAddGroup.addGroupSeminorm {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} :
AddGroupSeminorm (M ⧸ S)

The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on `x + S`.

Equations

- QuotientAddGroup.addGroupSeminorm = { toFun := fun (x : M ⧸ S) => Metric.infDist 0 {m : M | ↑m = x}, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }

Instances For

source
noncomputable instance QuotientGroup.instNorm {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} :
Norm (M ⧸ S)

The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on `x * S`.

Equations

- QuotientGroup.instNorm = { norm := ⇑QuotientGroup.groupSeminorm }

source
noncomputable instance QuotientAddGroup.instNorm {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} :
Norm (M ⧸ S)

The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on `x + S`.

Equations

- QuotientAddGroup.instNorm = { norm := ⇑QuotientAddGroup.addGroupSeminorm }

source
theorem QuotientGroup.norm_eq_groupSeminorm {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} (x : M ⧸ S) :
‖x‖ = groupSeminorm x
source
theorem QuotientAddGroup.norm_eq_addGroupSeminorm {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M ⧸ S) :
‖x‖ = addGroupSeminorm x
source
theorem QuotientGroup.norm_eq_infDist {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} (x : M ⧸ S) :
‖x‖ = Metric.infDist 1 {m : M | ↑m = x}
source
theorem QuotientAddGroup.norm_eq_infDist {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M ⧸ S) :
‖x‖ = Metric.infDist 0 {m : M | ↑m = x}
source
theorem QuotientGroup.le_norm_iff {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {x : M ⧸ S} {r : ℝ} :
r ≤ ‖x‖ ↔ ∀ (m : M), ↑m = x → r ≤ ‖m‖
source
theorem QuotientAddGroup.le_norm_iff {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {x : M ⧸ S} {r : ℝ} :
r ≤ ‖x‖ ↔ ∀ (m : M), ↑m = x → r ≤ ‖m‖
source
theorem QuotientGroup.norm_lt_iff {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {x : M ⧸ S} {r : ℝ} :
‖x‖ < r ↔ ∃ (m : M), ↑m = x ∧ ‖m‖ < r
source
theorem QuotientAddGroup.norm_lt_iff {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {x : M ⧸ S} {r : ℝ} :
‖x‖ < r ↔ ∃ (m : M), ↑m = x ∧ ‖m‖ < r
source
theorem QuotientGroup.nhds_one_hasBasis {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} :
(nhds 1).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {x : M ⧸ S | ‖x‖ < ε}
source
theorem QuotientAddGroup.nhds_zero_hasBasis {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} :
(nhds 0).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {x : M ⧸ S | ‖x‖ < ε}
source
theorem QuotientGroup.norm_mk {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} (x : M) :
‖↑x‖ = Metric.infDist x ↑S

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`.

source
theorem QuotientAddGroup.norm_mk {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M) :
‖↑x‖ = Metric.infDist x ↑S

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`.

source
theorem QuotientGroup.norm_mk_le_norm {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {m : M} :
‖↑m‖ ≤ ‖m‖

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

source
theorem QuotientAddGroup.norm_mk_le_norm {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {m : M} :
‖↑m‖ ≤ ‖m‖

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

source
theorem QuotientGroup.norm_mk_eq_zero_iff_mem_closure {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {m : M} :
‖↑m‖ = 0 ↔ m ∈ closure ↑S

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`.

source
theorem QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {m : M} :
‖↑m‖ = 0 ↔ m ∈ closure ↑S

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`.

source
theorem QuotientGroup.norm_mk_eq_zero {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {m : M} [hS : IsClosed ↑S] :
‖↑m‖ = 0 ↔ m ∈ S

The norm of the image of `m : M` in the quotient by a closed subgroup `S` is zero if and only if `m ∈ S`.

source
theorem QuotientAddGroup.norm_mk_eq_zero {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {m : M} [hS : IsClosed ↑S] :
‖↑m‖ = 0 ↔ m ∈ S

The norm of the image of `m : M` in the quotient by a closed subgroup `S` is zero if and only if `m ∈ S`.

source
theorem QuotientGroup.exists_norm_mk_lt {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {ε : ℝ} (x : M ⧸ S) (hε : 0 < ε) :
∃ (m : 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‖ + ε`.

source
theorem QuotientAddGroup.exists_norm_mk_lt {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {ε : ℝ} (x : M ⧸ S) (hε : 0 < ε) :
∃ (m : 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‖ + ε`.

source
theorem QuotientGroup.exists_norm_mul_lt {M : Type u_1} [SeminormedCommGroup M] (S : Subgroup M) (m : M) {ε : ℝ} (hε : 0 < ε) :
∃ s ∈ S, ‖m * s‖ < ‖(mk' S) m‖ + ε

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

source
theorem QuotientAddGroup.exists_norm_add_lt {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M) {ε : ℝ} (hε : 0 < ε) :
∃ s ∈ S, ‖m + s‖ < ‖(mk' S) m‖ + ε

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

source
noncomputable instance QuotientGroup.instSeminormedCommGroup {M : Type u_1} [SeminormedCommGroup M] (S : Subgroup M) :
SeminormedCommGroup (M ⧸ S)

The seminormed group structure on the quotient by a subgroup.

Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance QuotientAddGroup.instSeminormedAddCommGroup {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) :
SeminormedAddCommGroup (M ⧸ S)

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

Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance QuotientGroup.instNormedCommGroup {M : Type u_1} [SeminormedCommGroup M] (S : Subgroup M) [hS : IsClosed ↑S] :
NormedCommGroup (M ⧸ S)

The quotient in the category of normed groups.

Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance QuotientAddGroup.instNormedAddCommGroup {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) [hS : IsClosed ↑S] :
NormedAddCommGroup (M ⧸ S)

The quotient in the category of normed groups.

Equations

- One or more equations did not get rendered due to their size.

source
def Subgroup.quotientIsometryEquivOfEq {M : Type u_1} [SeminormedCommGroup M] {S T : Subgroup M} (h : S = T) :
M ⧸ S ≃ᵢ M ⧸ T

An isometric version of `Subgroup.quotientEquivOfEq`.

Equations

- Subgroup.quotientIsometryEquivOfEq h = { toEquiv := Subgroup.quotientEquivOfEq h, isometry_toFun := ⋯ }

Instances For

source
def AddSubgroup.quotientIsometryEquivOfEq {M : Type u_1} [SeminormedAddCommGroup M] {S T : AddSubgroup M} (h : S = T) :
M ⧸ S ≃ᵢ M ⧸ T

An isometric version of `AddSubgroup.quotientEquivOfEq`.

Equations

- AddSubgroup.quotientIsometryEquivOfEq h = { toEquiv := AddSubgroup.quotientEquivOfEq h, isometry_toFun := ⋯ }

Instances For

source
def QuotientGroup.quotientBotIsometryEquiv {M : Type u_1} [SeminormedCommGroup M] :
M ⧸ ⊥ ≃ᵢ M

An isometric version of `QuotientGroup.quotientBot`.

Equations

- QuotientGroup.quotientBotIsometryEquiv = { toEquiv := QuotientGroup.quotientBot.toEquiv, isometry_toFun := ⋯ }

Instances For

source
def QuotientAddGroup.quotientBotIsometryEquiv {M : Type u_1} [SeminormedAddCommGroup M] :
M ⧸ ⊥ ≃ᵢ M

An isometric version of `QuotientAddGroup.quotientBot`.

Equations

- QuotientAddGroup.quotientBotIsometryEquiv = { toEquiv := QuotientAddGroup.quotientBot.toEquiv, isometry_toFun := ⋯ }

Instances For

source
def QuotientGroup.quotientQuotientIsometryEquivQuotient {M : Type u_1} [SeminormedCommGroup M] {S T : Subgroup M} (h : S ≤ T) :
(M ⧸ S) ⧸ Subgroup.map (mk' S) T ≃ᵢ M ⧸ T

An isometric version of `QuotientGroup.quotientQuotientEquivQuotient`.

Equations

- QuotientGroup.quotientQuotientIsometryEquivQuotient h = { toEquiv := (QuotientGroup.quotientQuotientEquivQuotient S T h).toEquiv, isometry_toFun := ⋯ }

Instances For

source
def QuotientAddGroup.quotientQuotientIsometryEquivQuotient {M : Type u_1} [SeminormedAddCommGroup M] {S T : AddSubgroup M} (h : S ≤ T) :
(M ⧸ S) ⧸ AddSubgroup.map (mk' S) T ≃ᵢ M ⧸ T

An isometric version of `QuotientAddGroup.quotientQuotientEquivQuotient`.

Equations

- QuotientAddGroup.quotientQuotientIsometryEquivQuotient h = { toEquiv := (QuotientAddGroup.quotientQuotientEquivQuotient S T h).toEquiv, isometry_toFun := ⋯ }

Instances For

source
theorem quotient_norm_mk_eq {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M) :
‖(QuotientAddGroup.mk' S) m‖ = sInf ((fun (x : M) => ‖m + x‖) '' ↑S)

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

source
theorem quotient_norm_add_le {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) (x y : M ⧸ S) :
‖x + y‖ ≤ ‖x‖ + ‖y‖

The quotient norm satisfies the triangle inequality.

source
noncomputable def AddSubgroup.normedMk {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) :
NormedAddGroupHom M (M ⧸ S)

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

Equations

- S.normedMk = { toFun := (↑(QuotientAddGroup.mk' S)).toFun, map_add' := ⋯, bound' := ⋯ }

Instances For

source
@[simp]
theorem AddSubgroup.normedMk.apply {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M) :
S.normedMk m = (QuotientAddGroup.mk' S) m

`S.normedMk` agrees with `QuotientAddGroup.mk' S`.

source
theorem AddSubgroup.surjective_normedMk {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) :
Function.Surjective ⇑S.normedMk

`S.normedMk` is surjective.

source
theorem AddSubgroup.ker_normedMk {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) :
S.normedMk.ker = S

The kernel of `S.normedMk` is `S`.

source
theorem AddSubgroup.norm_normedMk_le {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) :
‖S.normedMk‖ ≤ 1

The operator norm of the projection is at most `1`.

source
theorem QuotientAddGroup.norm_lift_apply_le {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] {S : AddSubgroup M} (f : NormedAddGroupHom M N) (hf : ∀ x ∈ S, f x = 0) (x : M ⧸ S) :
‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖
source
theorem AddSubgroup.norm_normedMk {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) (h : ↑S.topologicalClosure ≠ Set.univ) :
‖S.normedMk‖ = 1

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

source
theorem AddSubgroup.norm_trivial_quotient_mk {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) (h : ↑S.topologicalClosure = Set.univ) :
‖S.normedMk‖ = 0

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

source
structure NormedAddGroupHom.IsQuotient {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) :
Prop

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

- surjective : Function.Surjective ⇑f
- norm (x : M) : ‖f x‖ = sInf ((fun (m : M) => ‖x + m‖) '' ↑f.ker)

Instances For

source
noncomputable def NormedAddGroupHom.lift {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) :
NormedAddGroupHom (M ⧸ S) N

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`.

Equations

- NormedAddGroupHom.lift S f hf = { toFun := (↑(QuotientAddGroup.lift S f.toAddMonoidHom hf)).toFun, map_add' := ⋯, bound' := ⋯ }

Instances For

source
theorem NormedAddGroupHom.lift_mk {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) (m : M) :
(lift S f hf) (S.normedMk m) = f m
source
theorem NormedAddGroupHom.lift_unique {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) (g : NormedAddGroupHom (M ⧸ S) N) (h : g.comp S.normedMk = f) :
g = lift S f hf
source
theorem NormedAddGroupHom.isQuotientQuotient {M : Type u_1} [SeminormedAddCommGroup M] (S : AddSubgroup M) :
S.normedMk.IsQuotient

`S.normedMk` satisfies `IsQuotient`.

source
theorem NormedAddGroupHom.IsQuotient.norm_lift {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] {f : NormedAddGroupHom M N} (hquot : f.IsQuotient) {ε : ℝ} (hε : 0 < ε) (n : N) :
∃ (m : M), f m = n ∧ ‖m‖ < ‖n‖ + ε
source
theorem NormedAddGroupHom.IsQuotient.norm_le {M : Type u_1} {N : Type u_2} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] {f : NormedAddGroupHom M N} (hquot : f.IsQuotient) (m : M) :
‖f m‖ ≤ ‖m‖
source
theorem NormedAddGroupHom.norm_lift_le {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) :
‖lift S f hf‖ ≤ ‖f‖
source
theorem NormedAddGroupHom.lift_norm_le {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) {c : NNReal} (fb : ‖f‖ ≤ ↑c) :
‖lift S f hf‖ ≤ ↑c
source
theorem NormedAddGroupHom.lift_normNoninc {M : Type u_1} [SeminormedAddCommGroup M] {N : Type u_3} [SeminormedAddCommGroup N] (S : AddSubgroup M) (f : NormedAddGroupHom M N) (hf : ∀ s ∈ S, f s = 0) (fb : f.NormNoninc) :
(lift S f hf).NormNoninc

### 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 two-sided ideals, hence the commutativity hypotheses are required.

source
instance Submodule.Quotient.seminormedAddCommGroup {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S : Submodule R M) :
SeminormedAddCommGroup (M ⧸ S)
Equations

- Submodule.Quotient.seminormedAddCommGroup S = QuotientAddGroup.instSeminormedAddCommGroup S.toAddSubgroup

source
instance Submodule.Quotient.normedAddCommGroup {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S : Submodule R M) [hS : IsClosed ↑S] :
NormedAddCommGroup (M ⧸ S)
Equations

- Submodule.Quotient.normedAddCommGroup S = QuotientAddGroup.instNormedAddCommGroup S.toAddSubgroup

source
instance Submodule.Quotient.completeSpace {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S : Submodule R M) [CompleteSpace M] :
CompleteSpace (M ⧸ S)
source
theorem Submodule.Quotient.norm_mk_lt {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] {S : Submodule R M} (x : M ⧸ S) {ε : ℝ} (hε : 0 < ε) :
∃ (m : M), mk m = x ∧ ‖m‖ < ‖x‖ + ε

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

source
theorem Submodule.Quotient.norm_mk_le {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S : Submodule R M) (m : M) :
‖mk m‖ ≤ ‖m‖
source
instance Submodule.Quotient.instIsBoundedSMul {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S : Submodule R M) (𝕜 : Type u_4) [SeminormedCommRing 𝕜] [Module 𝕜 M] [IsBoundedSMul 𝕜 M] [SMul 𝕜 R] [IsScalarTower 𝕜 R M] :
IsBoundedSMul 𝕜 (M ⧸ S)
source
instance Submodule.Quotient.normedSpace {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S : Submodule R M) (𝕜 : Type u_4) [NormedField 𝕜] [NormedSpace 𝕜 M] [SMul 𝕜 R] [IsScalarTower 𝕜 R M] :
NormedSpace 𝕜 (M ⧸ S)
Equations

- Submodule.Quotient.normedSpace S 𝕜 = { toModule := Submodule.Quotient.module' S, norm_smul_le := ⋯ }

source
def Submodule.quotLIEOfEq {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S T : Submodule R M) (h : S = T) :
M ⧸ S ≃ₗᵢ[R] M ⧸ T

An isometric version of `Submodule.quotEquivOfEq`.

Equations

- S.quotLIEOfEq T h = { toLinearEquiv := S.quotEquivOfEq T h, norm_map' := ⋯ }

Instances For

source
def Submodule.quotientQuotientLIEQuotient {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S T : Submodule R M) (h : S ≤ T) :
(M ⧸ S) ⧸ map S.mkQ T ≃ₗᵢ[R] M ⧸ T

An isometric version of `Submodule.quotientQuotientEquivQuotient`.

Equations

- S.quotientQuotientLIEQuotient T h = { toLinearEquiv := S.quotientQuotientEquivQuotient T h, norm_map' := ⋯ }

Instances For

source
def Submodule.quotientQuotientLIEQuotientSup {M : Type u_1} [SeminormedAddCommGroup M] {R : Type u_3} [Ring R] [Module R M] (S T : Submodule R M) :
(M ⧸ S) ⧸ map S.mkQ T ≃ₗᵢ[R] M ⧸ S ⊔ T

An isometric version of `Submodule.quotientQuotientEquivQuotientSup`.

Equations

- S.quotientQuotientLIEQuotientSup T = ((Submodule.map S.mkQ T).quotLIEOfEq (Submodule.map S.mkQ (S ⊔ T)) ⋯).trans (S.quotientQuotientLIEQuotient (S ⊔ T) ⋯)

Instances For

source
theorem Ideal.Quotient.norm_mk_lt {R : Type u_3} [SeminormedCommRing R] {I : Ideal R} (x : R ⧸ I) {ε : ℝ} (hε : 0 < ε) :
∃ (r : R), (mk I) r = x ∧ ‖r‖ < ‖x‖ + ε
source
theorem Ideal.Quotient.norm_mk_le {R : Type u_3} [SeminormedCommRing R] (I : Ideal R) (r : R) :
‖(mk I) r‖ ≤ ‖r‖
source
instance Ideal.Quotient.semiNormedCommRing {R : Type u_3} [SeminormedCommRing R] (I : Ideal R) :
SeminormedCommRing (R ⧸ I)
Equations

- One or more equations did not get rendered due to their size.

source
instance Ideal.Quotient.normedCommRing {R : Type u_3} [SeminormedCommRing R] (I : Ideal R) [IsClosed ↑I] :
NormedCommRing (R ⧸ I)
Equations

- One or more equations did not get rendered due to their size.

source
instance Ideal.Quotient.normedAlgebra {R : Type u_3} [SeminormedCommRing R] (I : Ideal R) (𝕜 : Type u_4) [NormedField 𝕜] [NormedAlgebra 𝕜 R] :
NormedAlgebra 𝕜 (R ⧸ I)
Equations

- Ideal.Quotient.normedAlgebra I 𝕜 = { toSMul := (Submodule.Quotient.normedSpace I 𝕜).toSMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯, norm_smul_le := ⋯ }