Archimedean groups are either discrete or densely ordered

This file proves a few additional facts about linearly ordered additive groups which satisfy the Archimedean property -- they are either order-isomorphic and additvely isomorphic to the integers, or they are densely ordered.

They are placed here in a separate file (rather than incorporated as a continuation of GroupTheory.Archimedean) because they rely on some imports from pointwise lemmas.

theorem Subgroup.mem_closure_singleton_iff_existsUnique_zpow {G : Type u_1} [LinearOrderedCommGroup G] {a b : G} (ha : a ≠ 1) : b ∈ Subgroup.closure {a} ↔ ∃! k : ℤ, a ^ k = b

The subgroup generated by an element of a group equals the set of integer powers of the element, such that each power is a unique element. This is the stronger version of Subgroup.mem_closure_singleton.

theorem AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul {G : Type u_1} [LinearOrderedAddCommGroup G] {a b : G} (ha : a ≠ 0) : b ∈ AddSubgroup.closure {a} ↔ ∃! k : ℤ, k • a = b

The additive subgroup generated by an element of an additive group equals the set of integer multiples of the element, such that each multiple is a unique element. This is the stronger version of AddSubgroup.mem_closure_singleton.

noncomputable def LinearOrderedCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [LinearOrderedCommGroup G] [LinearOrderedCommGroup G'] (x : G) (y : G') (hxy : x = 1 ↔ y = 1) : ↥(Subgroup.closure {x}) ≃*o ↥(Subgroup.closure {y})

In two linearly ordered groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

Equations

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

noncomputable def LinearOrderedAddCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) : ↥(AddSubgroup.closure {x}) ≃+o ↥(AddSubgroup.closure {y})

In two linearly ordered additive groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

Equations

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

theorem Subgroup.isLeast_of_closure_iff_eq_mabs {G : Type u_1} [LinearOrderedCommGroup G] [MulArchimedean G] {a b : G} : IsLeast {y : G | y ∈ Subgroup.closure {a} ∧ 1 < y} b ↔ b = mabs a ∧ 1 < b

theorem AddSubgroup.isLeast_of_closure_iff_eq_abs {G : Type u_1} [LinearOrderedAddCommGroup G] [Archimedean G] {a b : G} : IsLeast {y : G | y ∈ AddSubgroup.closure {a} ∧ 0 < y} b ↔ b = |a| ∧ 0 < b

noncomputable def LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos {G : Type u_2} [LinearOrderedAddCommGroup G] [Archimedean G] {x : G} (h : IsLeast {y : G | 0 < y} x) : G ≃+o ℤ

If an element of a linearly ordered archimedean additive group is the least positive element, then the whole group is isomorphic (and order-isomorphic) to the integers.

Equations

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

noncomputable def LinearOrderedCommGroup.multiplicative_int_orderMonoidIso_of_isLeast_one_lt {G : Type u_1} [LinearOrderedCommGroup G] [MulArchimedean G] {x : G} (h : IsLeast {y : G | 1 < y} x) : G ≃*o Multiplicative ℤ

If an element of a linearly ordered mul-archimedean group is the least element greater than 1, then the whole group is isomorphic (and order-isomorphic) to the multiplicative integers.

Equations

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

theorem LinearOrderedAddCommGroup.discrete_or_denselyOrdered (G : Type u_2) [LinearOrderedAddCommGroup G] [Archimedean G] : Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic) to the integers, or is densely ordered.

theorem LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered (G : Type u_2) [LinearOrderedAddCommGroup G] [Archimedean G] : Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic) to the integers, or is densely ordered, exclusively.

theorem LinearOrderedCommGroup.discrete_or_denselyOrdered (G : Type u_1) [LinearOrderedCommGroup G] [MulArchimedean G] : Nonempty (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G

Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic) to the multiplicative integers, or is densely ordered.

theorem LinearOrderedCommGroup.discrete_iff_not_denselyOrdered (G : Type u_1) [LinearOrderedCommGroup G] [MulArchimedean G] : Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic) to the multiplicative integers, or is densely ordered, exclusively.

theorem denselyOrdered_units_iff {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] : DenselyOrdered G₀ˣ ↔ DenselyOrdered G₀

theorem LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered (G : Type u_2) [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] : Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered G

Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is either isomorphic (and order-isomorphic) to ℤₘ₀, or is densely ordered.

theorem LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered (G : Type u_2) [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] : Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬DenselyOrdered G

Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is either isomorphic (and order-isomorphic) to ℤₘ₀, or is densely ordered, exclusively

theorem LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete {G : Type u_2} [LinearOrderedAddCommGroup G] [Nontrivial G] {g : G} : ({x : G | g ≤ x}.WellFoundedOn fun (x1 x2 : G) => x1 < x2) ↔ Nonempty (G ≃+o ℤ)

theorem LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete {G : Type u_2} [LinearOrderedAddCommGroup G] [Nontrivial G] (g : G) : ({x : G | x ≤ g}.WellFoundedOn fun (x1 x2 : G) => x1 > x2) ↔ Nonempty (G ≃+o ℤ)

theorem LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete {G : Type u_2} [LinearOrderedCommGroup G] [Nontrivial G] {g : G} : ({x : G | g ≤ x}.WellFoundedOn fun (x1 x2 : G) => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

theorem LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete {G : Type u_2} [LinearOrderedCommGroup G] [Nontrivial G] (g : G) : ({x : G | x ≤ g}.WellFoundedOn fun (x1 x2 : G) => x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) : ({x : G₀ | g ≤ x}.WellFoundedOn fun (x1 x2 : G₀) => x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) : ({x : G₀ | x ≤ g}.WellFoundedOn fun (x1 x2 : G₀) => x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))