The null subgroup in a seminormed commutative group

For any SeminormedAddCommGroup M, the quotient SeparationQuotient M by the null subgroup is defined as a NormedAddCommGroup instance in Mathlib/Analysis/Normed/Group/Uniform.lean. Here we define the null space as a subgroup.

Main definitions

We use M to denote seminormed groups.

• nullAddSubgroup : the subgroup of elements x with ‖x‖ = 0.

If E is a vector space over 𝕜 with an appropriate continuous action, we also define the null subspace as a submodule of E.

• nullSubmodule : the subspace of elements x with ‖x‖ = 0.

def nullSubgroup (M : Type u_1) [SeminormedCommGroup M] : Subgroup M

The null subgroup with respect to the norm.

Equations

• nullSubgroup M = { carrier := {x : M | ‖x‖ = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def nullAddSubgroup (M : Type u_1) [SeminormedAddCommGroup M] : AddSubgroup M

The additive null subgroup with respect to the norm.

Equations

• nullAddSubgroup M = { carrier := {x : M | ‖x‖ = 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem isClosed_nullSubgroup {M : Type u_1} [SeminormedCommGroup M] : IsClosed ↑(nullSubgroup M)

theorem isClosed_nullAddSubgroup {M : Type u_1} [SeminormedAddCommGroup M] : IsClosed ↑(nullAddSubgroup M)

@[simp]

theorem mem_nullSubgroup_iff {M : Type u_1} [SeminormedCommGroup M] {x : M} : x ∈ nullSubgroup M ↔ ‖x‖ = 0

@[simp]

theorem mem_nullAddSubgroup_iff {M : Type u_1} [SeminormedAddCommGroup M] {x : M} : x ∈ nullAddSubgroup M ↔ ‖x‖ = 0

def nullSubmodule (𝕜 : Type u_2) (E : Type u_3) [SeminormedAddCommGroup E] [SeminormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : Submodule 𝕜 E

The null space with respect to the norm.

Equations

• nullSubmodule 𝕜 E = { toAddSubmonoid := (nullAddSubgroup E).toAddSubmonoid, smul_mem' := ⋯ }

theorem isClosed_nullSubmodule {𝕜 : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] [SeminormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : IsClosed ↑(nullSubmodule 𝕜 E)

@[simp]

theorem mem_nullSubmodule_iff {𝕜 : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] [SeminormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] {x : E} : x ∈ nullSubmodule 𝕜 E ↔ ‖x‖ = 0