# Archimedean groups #

This file proves a few facts about ordered groups which satisfy the `Archimedean` property, that is: `class Archimedean (α) [OrderedAddCommMonoid α] : Prop :=` `(arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)`

They are placed here in a separate file (rather than incorporated as a continuation of `Algebra.Order.Archimedean`) because they rely on some imports from `GroupTheory` -- bundled subgroups in particular.

The main result is `AddSubgroup.cyclic_of_min`: a subgroup of a decidable archimedean abelian group is cyclic, if its set of positive elements has a minimal element.

This result is used in this file to deduce `Int.subgroup_cyclic`, proving that every subgroup of `ℤ` is cyclic. (There are several other methods one could use to prove this fact, including more purely algebraic methods, but none seem to exist in mathlib as of writing. The closest is `Subgroup.is_cyclic`, but that has not been transferred to `AddSubgroup`.)

The file also supports multiplicative groups via `MulArchimedean`.

The result is also used in `Topology.Instances.Real` as an ingredient in the classification of subgroups of `ℝ`.

source
theorem Subgroup.cyclic_of_min {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a) :
H = closure {a}

Given a subgroup `H` of a decidable linearly ordered mul-archimedean abelian group `G`, if there exists a minimal element `a` of `H ∩ G_{>1}` then `H` is generated by `a`.

source
theorem AddSubgroup.cyclic_of_min {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 0 < g} a) :
H = closure {a}

Given a subgroup `H` of a decidable linearly ordered archimedean abelian group `G`, if there exists a minimal element `a` of `H ∩ G_{>0}` then `H` is generated by `a`.

source
theorem Subgroup.exists_isLeast_one_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 1 < a) (hd : Disjoint (↑H) (Set.Ioo 1 a)) :
∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b

If a nontrivial subgroup of a linear ordered commutative group is disjoint with the interval `Set.Ioo 1 a` for some `1 < a`, then the set of elements greater than 1 of this group admits the least element.

source
theorem AddSubgroup.exists_isLeast_pos {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 0 < a) (hd : Disjoint (↑H) (Set.Ioo 0 a)) :
∃ (b : G), IsLeast {g : G | g ∈ H ∧ 0 < g} b

If a nontrivial additive subgroup of a linear ordered additive commutative group is disjoint with the interval `Set.Ioo 0 a` for some positive `a`, then the set of positive elements of this group admits the least element.

source
theorem Subgroup.cyclic_of_isolated_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (h₀ : 1 < a) (hd : Disjoint (↑H) (Set.Ioo 1 a)) :
∃ (b : G), H = closure {b}

If a subgroup of a linear ordered commutative group is disjoint with the interval `Set.Ioo 1 a` for some `1 < a`, then this is a cyclic subgroup.

source
theorem AddSubgroup.cyclic_of_isolated_zero {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} {a : G} (h₀ : 0 < a) (hd : Disjoint (↑H) (Set.Ioo 0 a)) :
∃ (b : G), H = closure {b}

If an additive subgroup of a linear ordered additive commutative group is disjoint with the interval `Set.Ioo 0 a` for some positive `a`, then this is a cyclic subgroup.

source
theorem Int.subgroup_cyclic (H : AddSubgroup ℤ) :
∃ (a : ℤ), H = AddSubgroup.closure {a}

Every subgroup of `ℤ` is cyclic.