Quotients of seminormed and ultrametric groups

For a subgroup S of a seminormed commutative group M, an element s ∈ S minimises ‖m / s'‖ over s' ∈ S if and only if ‖m / s‖ attains the quotient seminorm ‖(m : M ⧸ S)‖ (QuotientGroup.norm_div_eq_norm_mk_iff), so every coset has a least-norm element precisely when every class in M ⧸ S has a representative of the same norm (QuotientGroup.exists_mk_eq_and_norm_eq_iff). The additive, submodule and ideal counterparts give the corresponding characterisations of strict closedness for submodules and ideals.

If every nontrivial element of S has seminorm at least twice that of m, then m attains the quotient seminorm of its class (QuotientGroup.norm_mk_eq_norm). So the projection M → M ⧸ S preserves the distance between two points whose distance is at most half the least seminorm of a nontrivial element of S (QuotientGroup.dist_mk_eq_dist); for a lattice in a normed space this says that the projection to the torus is an isometry on small sets.

When M is ultrametric, the quotient seminorm on M ⧸ S is again ultrametric: each class has representatives whose norms approximate its quotient norm, and the ultrametric inequality for a product of such representatives descends to the quotient. The additive form covers quotients of modules by submodules and of commutative seminormed rings by ideals, so residue norms of nonarchimedean Banach algebras are again nonarchimedean.

theorem QuotientGroup.norm_div_eq_norm_mk_iff {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {m s : M} (hs : s ∈ S) : ‖m / s‖ = ‖↑m‖ ↔ ∀ s' ∈ S, ‖m / s‖ ≤ ‖m / s'‖

For s ∈ S, the element m / s attains the quotient seminorm of m modulo S if and only if s minimises ‖m / s'‖ over S.

theorem QuotientAddGroup.norm_sub_eq_norm_mk_iff {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {m s : M} (hs : s ∈ S) : ‖m - s‖ = ‖↑m‖ ↔ ∀ s' ∈ S, ‖m - s‖ ≤ ‖m - s'‖

For s ∈ S, the element m - s attains the quotient seminorm of m modulo S if and only if s minimises ‖m - s'‖ over S.

theorem QuotientGroup.exists_mk_eq_and_norm_eq_iff {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} : (∀ (x : M ⧸ S), ∃ (m : M), ↑m = x ∧ ‖m‖ = ‖x‖) ↔ ∀ (m : M), ∃ s ∈ S, ∀ s' ∈ S, ‖m / s‖ ≤ ‖m / s'‖

Every class in M ⧸ S has a representative attaining its quotient seminorm if and only if every coset of S has an element of least seminorm.

theorem QuotientAddGroup.exists_mk_eq_and_norm_eq_iff {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} : (∀ (x : M ⧸ S), ∃ (m : M), ↑m = x ∧ ‖m‖ = ‖x‖) ↔ ∀ (m : M), ∃ s ∈ S, ∀ s' ∈ S, ‖m - s‖ ≤ ‖m - s'‖

Every class in M ⧸ S has a representative attaining its quotient seminorm if and only if every coset of S has an element of least seminorm.

theorem QuotientGroup.norm_mk_eq_norm {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {m : M} (h : ∀ s ∈ S, s ≠ 1 → 2 * ‖m‖ ≤ ‖s‖) : ‖↑m‖ = ‖m‖

If every nontrivial element of S has at least twice the seminorm of m, then the quotient seminorm of m modulo S is the seminorm of m.

theorem QuotientAddGroup.norm_mk_eq_norm {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {m : M} (h : ∀ s ∈ S, s ≠ 0 → 2 * ‖m‖ ≤ ‖s‖) : ‖↑m‖ = ‖m‖

If every nonzero element of S has at least twice the seminorm of m, then the quotient seminorm of m modulo S is the seminorm of m.

theorem QuotientGroup.dist_mk_eq_dist {M : Type u_1} [SeminormedCommGroup M] {S : Subgroup M} {x y : M} (h : ∀ s ∈ S, s ≠ 1 → 2 * dist x y ≤ ‖s‖) : dist ↑x ↑y = dist x y

The projection to M ⧸ S preserves the distance between x and y when every nontrivial element of S has at least twice that distance as seminorm.

theorem QuotientAddGroup.dist_mk_eq_dist {M : Type u_1} [SeminormedAddCommGroup M] {S : AddSubgroup M} {x y : M} (h : ∀ s ∈ S, s ≠ 0 → 2 * dist x y ≤ ‖s‖) : dist ↑x ↑y = dist x y

The projection to M ⧸ S preserves the distance between x and y when every nonzero element of S has at least twice that distance as seminorm.

instance QuotientGroup.instIsUltrametricDist {M : Type u_1} [SeminormedCommGroup M] [IsUltrametricDist M] (S : Subgroup M) : IsUltrametricDist (M ⧸ S)

The quotient of an ultrametric seminormed commutative group by a subgroup is ultrametric.

instance QuotientAddGroup.instIsUltrametricDist {M : Type u_1} [SeminormedAddCommGroup M] [IsUltrametricDist M] (S : AddSubgroup M) : IsUltrametricDist (M ⧸ S)

The quotient of an ultrametric seminormed additive commutative group by an additive subgroup is ultrametric.

theorem Submodule.Quotient.norm_sub_eq_norm_mk_iff {R : Type u_1} {M : Type u_2} [Ring R] [SeminormedAddCommGroup M] [Module R M] {S : Submodule R M} {m s : M} (hs : s ∈ S) : ‖m - s‖ = ‖mk m‖ ↔ ∀ s' ∈ S, ‖m - s‖ ≤ ‖m - s'‖

For s ∈ S, the vector m - s attains the quotient seminorm of m modulo the submodule S if and only if s minimises ‖m - s'‖ over S.

theorem Submodule.Quotient.exists_mk_eq_and_norm_eq_iff {R : Type u_1} {M : Type u_2} [Ring R] [SeminormedAddCommGroup M] [Module R M] {S : Submodule R M} : (∀ (x : M ⧸ S), ∃ (m : M), mk m = x ∧ ‖m‖ = ‖x‖) ↔ ∀ (m : M), ∃ s ∈ S, ∀ s' ∈ S, ‖m - s‖ ≤ ‖m - s'‖

Every class in M ⧸ S has a representative attaining its quotient seminorm if and only if every coset of the submodule S has a vector of least seminorm.

instance Submodule.Quotient.instIsUltrametricDist {R : Type u_1} {M : Type u_2} [Ring R] [SeminormedAddCommGroup M] [Module R M] [IsUltrametricDist M] (S : Submodule R M) : IsUltrametricDist (M ⧸ S)

The quotient of an ultrametric seminormed module by a submodule is ultrametric.

theorem Ideal.Quotient.norm_sub_eq_norm_mk_iff {R : Type u_1} [SeminormedCommRing R] {I : Ideal R} {r s : R} (hs : s ∈ I) : ‖r - s‖ = ‖(mk I) r‖ ↔ ∀ s' ∈ I, ‖r - s‖ ≤ ‖r - s'‖

For s ∈ I, the element r - s attains the quotient seminorm of r modulo the ideal I if and only if s minimises ‖r - s'‖ over I.

theorem Ideal.Quotient.exists_mk_eq_and_norm_eq_iff {R : Type u_1} [SeminormedCommRing R] {I : Ideal R} : (∀ (x : R ⧸ I), ∃ (r : R), (mk I) r = x ∧ ‖r‖ = ‖x‖) ↔ ∀ (r : R), ∃ s ∈ I, ∀ s' ∈ I, ‖r - s‖ ≤ ‖r - s'‖

Every residue class in R ⧸ I has a representative attaining its quotient seminorm if and only if every coset of I has an element of least seminorm.