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 additively 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 exists_pow_lt₀ {G : Type u_1} [LinearOrderedCommGroupWithZero G] [MulArchimedean G] {a : G} (ha : a < 1) (b : Gˣ) : ∃ (n : ℕ), a ^ n < ↑b

theorem Subgroup.mem_closure_singleton_iff_existsUnique_zpow {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (ha : a ≠ 1) : b ∈ 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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (ha : a ≠ 0) : b ∈ 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.

theorem Int.addEquiv_eq_refl_or_neg (e : ℤ ≃+ ℤ) : e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

@[implicit_reducible]

instance instFintypeAddEquivInt : Fintype (ℤ ≃+ ℤ)

@[simp]

theorem Int.univ_addEquiv : Finset.univ = Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

@[simp]

theorem Int.card_fintype_addEquiv : Fintype.card (ℤ ≃+ ℤ) = 2

@[implicit_reducible]

instance instUniqueOrderAddMonoidIsoInt : Unique (ℤ ≃+o ℤ)

@[implicit_reducible]

instance instUniqueOrderAddMonoidIsoIntOrderDual : Unique (ℤ ≃+o ℤᵒᵈ)

noncomputable def LinearOrderedCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [CommGroup G'] [LinearOrder G'] [IsOrderedMonoid 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.

noncomputable def LinearOrderedAddCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup G'] [LinearOrder G'] [IsOrderedAddMonoid 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.

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

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

noncomputable def LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid 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.

noncomputable def LinearOrderedCommGroup.multiplicative_int_orderMonoidIso_of_isLeast_one_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid 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.

theorem Archimedean.of_locallyFiniteOrder {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : Archimedean G

Any locally finite linear additive group is archimedean.

theorem MulArchimedean.of_locallyFiniteOrder {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G] : MulArchimedean G

Any locally finite linear group is mul-archimedean.

theorem LinearOrderedAddCommGroup.discrete_or_denselyOrdered (G : Type u_2) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid 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) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid 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.

(See also LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered.)

theorem LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered {A : Type u_2} [AddCommGroup A] [LinearOrder A] [IsOrderedAddMonoid A] [Archimedean A] [Nontrivial A] : IsAddCyclic A ↔ ¬DenselyOrdered A

Any non-trivial linearly ordered archimedean additive group is either cyclic, or densely ordered, exclusively.

theorem LinearOrderedCommGroup.discrete_or_denselyOrdered (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid 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) [CommGroup G] [LinearOrder G] [IsOrderedMonoid 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.

(See also LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered.)

theorem LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] [Nontrivial G] : IsCyclic G ↔ ¬DenselyOrdered G

Any non-trivial linearly ordered mul-archimedean group is either cyclic, or densely ordered, exclusively.

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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid 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} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid 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} [CommGroup G] [LinearOrder G] [IsOrderedMonoid 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} [CommGroup G] [LinearOrder G] [IsOrderedMonoid 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 ℤ))

instance instWellFoundedGTWithZeroMultiplicativeIntLeOne : WellFoundedGT { v : WithZero (Multiplicative ℤ) // v ≤ 1 }

theorem OrderMonoidIso.mulArchimedean {α : Type u_2} {β : Type u_3} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] (e : α ≃*o β) [MulArchimedean α] : MulArchimedean β

theorem OrderAddMonoidIso.addArchimedean {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] (e : α ≃+o β) [Archimedean α] : Archimedean β

theorem WithZero.mulArchimedean_iff {α : Type u_2} [CommGroup α] [PartialOrder α] : MulArchimedean (WithZero α) ↔ MulArchimedean α

theorem Units.mulArchimedean_iff {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] : MulArchimedean G₀ˣ ↔ MulArchimedean G₀

@[implicit_reducible]

instance instLocallyFiniteOrderMultiplicative {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] : LocallyFiniteOrder (Multiplicative X)

@[implicit_reducible]

instance instLocallyFiniteOrderAdditive {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] : LocallyFiniteOrder (Additive X)

@[implicit_reducible]

noncomputable instance instLocallyFiniteOrderUnits {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] [Monoid X] : LocallyFiniteOrder Xˣ

@[implicit_reducible]

instance instLocallyFiniteOrderUnitsWithZero {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] [Group X] : LocallyFiniteOrder (WithZero X)ˣ

theorem denselyOrdered_additive_iff {X : Type u_2} [LT X] : DenselyOrdered (Additive X) ↔ DenselyOrdered X

theorem denselyOrdered_multiplicative_iff {X : Type u_2} [LT X] : DenselyOrdered (Multiplicative X) ↔ DenselyOrdered X

instance instDenselyOrderedMultiplicative {X : Type u_2} [LT X] [DenselyOrdered X] : DenselyOrdered (Multiplicative X)

instance instDenselyOrderedAdditive {X : Type u_2} [LT X] [DenselyOrdered X] : DenselyOrdered (Additive X)

theorem WithZero.denselyOrdered_iff {M : Type u_3} [Preorder M] [NoMinOrder M] : DenselyOrdered (WithZero M) ↔ DenselyOrdered M

instance instDenselyOrderedWithZeroOfNoMinOrder {X : Type u_3} [Preorder X] [NoMinOrder X] [DenselyOrdered X] : DenselyOrdered (WithZero X)

theorem Int.not_denselyOrdered : ¬DenselyOrdered ℤ

theorem not_denselyOrdered_withZero_int : ¬DenselyOrdered (WithZero (Multiplicative ℤ))

theorem WithZero.denselyOrdered_set_iff_subsingleton {X : Type u_3} [LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithZero X)} : DenselyOrdered ↑s ↔ s.Subsingleton