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 ℝ.

theorem AddSubgroup.cyclic_of_min {G : Type u_1} [LinearOrderedAddCommGroup G] [Archimedean G] {H : AddSubgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 0 < g} a) : H = AddSubgroup.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.

theorem Subgroup.cyclic_of_min {G : Type u_1} [LinearOrderedCommGroup G] [MulArchimedean G] {H : Subgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a) : H = Subgroup.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.

theorem AddSubgroup.exists_isLeast_pos {G : Type u_1} [LinearOrderedAddCommGroup 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.

theorem Subgroup.exists_isLeast_one_lt {G : Type u_1} [LinearOrderedCommGroup 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.

theorem AddSubgroup.cyclic_of_isolated_zero {G : Type u_1} [LinearOrderedAddCommGroup G] [Archimedean G] {H : AddSubgroup G} {a : G} (h₀ : 0 < a) (hd : Disjoint (↑H) (Set.Ioo 0 a)) : ∃ (b : G), H = AddSubgroup.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.

theorem Subgroup.cyclic_of_isolated_one {G : Type u_1} [LinearOrderedCommGroup G] [MulArchimedean G] {H : Subgroup G} {a : G} (h₀ : 1 < a) (hd : Disjoint (↑H) (Set.Ioo 1 a)) : ∃ (b : G), H = Subgroup.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.

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

Every subgroup of ℤ is cyclic.