feat(GroupTheory/SpecificGroups/Cyclic): comparison and index of subgroups generated by powers

Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

@@ -137,8 +137,18 @@ theorem zpowers_one_eq_bot : Subgroup.zpowers (1 : G) = ⊥ :=
 theorem zpowers_inv : zpowers g⁻¹ = zpowers g :=
   eq_of_forall_ge_iff fun _ ↦ by simp only [zpowers_le, inv_mem_iff]
 
+/-- The subgroup generated by `g * h` is contained in the one generated by `g` and `h`. -/
+@[to_additive /-- The subgroup generated by `g + h` is contained in the one generated by `g`
+and `h`. -/]
+theorem zpowers_mul_le_sup (g h : G) : zpowers (g * h) ≤ zpowers g ⊔ zpowers h :=
+  zpowers_le.mpr (mul_mem_sup (mem_zpowers g) (mem_zpowers h))
+
 end Subgroup
 
+theorem Int.zmultiples_le_zmultiples_iff {a b : ℤ} :
+    AddSubgroup.zmultiples a ≤ AddSubgroup.zmultiples b ↔ b ∣ a := by
+  rw [AddSubgroup.zmultiples_le, Int.mem_zmultiples_iff]
+
 theorem Int.zmultiples_natAbs (a : ℤ) :
     AddSubgroup.zmultiples (a.natAbs : ℤ) = AddSubgroup.zmultiples a := by
   simp [le_antisymm_iff, Int.mem_zmultiples_iff, Int.dvd_natAbs, Int.natAbs_dvd]

Mathlib/Data/Nat/Basic.lean

@@ -119,6 +119,10 @@ lemma set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ k : ℕ, k ∈ S 
 
 /-! ### `mod`, `dvd` -/
 
+/-- Two natural numbers dividing each other are equal. -/
+protected lemma dvd_antisymm_iff : m = n ↔ m ∣ n ∧ n ∣ m :=
+  ⟨by simp +contextual, fun ⟨h₁, h₂⟩ ↦ Nat.dvd_antisymm h₁ h₂⟩
+
 /-- `dvd` is injective in the left argument -/
 lemma dvd_left_injective : Function.Injective ((· ∣ ·) : ℕ → ℕ → Prop) := fun _ _ h =>
   dvd_right_iff_eq.mp fun a => iff_of_eq (congr_fun h a)

Mathlib/GroupTheory/OrderOfElement.lean

@@ -1046,6 +1046,15 @@ lemma orderOf_eq_zero_iff_eq_zero {G₀ : Type*} [GroupWithZero G₀] [Finite G
 section FiniteGroup
 variable [Group G] {x y : G}
 
+@[to_additive]
+theorem orderOf_pow_natAbs (x : G) (n : ℤ) : orderOf (x ^ n.natAbs) = orderOf (x ^ n) := by
+  cases n <;> simp
+
+@[to_additive]
+theorem orderOf_zpow' (x : G) {n : ℤ} (h : n ≠ 0) :
+    orderOf (x ^ n) = orderOf x / (orderOf x).gcd n.natAbs := by
+  rw [← orderOf_pow' _ (Int.natAbs_ne_zero.mpr h), orderOf_pow_natAbs]
+
 @[to_additive]
 theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by
   rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]
@@ -1091,6 +1100,11 @@ theorem mem_zpowers_pow_iff {g : G} {k : ℕ} :
 section Finite
 variable [Finite G]
 
+@[to_additive]
+theorem orderOf_zpow (x : G) (n : ℤ) :
+    orderOf (x ^ n) = orderOf x / (orderOf x).gcd n.natAbs := by
+  rw [← orderOf_pow, orderOf_pow_natAbs]
+
 @[to_additive]
 theorem exists_zpow_eq_one (x : G) : ∃ (i : ℤ) (_ : i ≠ 0), x ^ (i : ℤ) = 1 := by
   obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 module
 
+public import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
 public import Mathlib.Algebra.Group.TypeTags.Finite
 public import Mathlib.Algebra.Order.Hom.TypeTags
 public import Mathlib.Data.Nat.Totient
@@ -395,6 +396,79 @@ theorem zpowersHom_ker_eq [Group G] (g : G) :
     (zpowersHom G g).ker = zpowers (Multiplicative.ofAdd ↑(orderOf g)) :=
   congr_arg AddSubgroup.toSubgroup <| zmultiplesHom_ker_eq (Additive.ofMul g)
 
+/-- `zmultiples (i • g) ≤ zmultiples (j • g)` iff `j.gcd (addOrderOf g) ∣ i.gcd (addOrderOf g)`.
+This characterizes inclusion of cyclic subgroups of an additive group generated by integer
+multiples of a single element. -/
+theorem AddSubgroup.zmultiples_le_zmultiples_iff [AddGroup G] (g : G) (i j : ℤ) :
+    zmultiples (i • g) ≤ zmultiples (j • g) ↔
+      j.gcd (addOrderOf g) ∣ i.gcd (addOrderOf g) := by
+  simp_rw [← zmultiplesHom_apply, ← AddMonoidHom.map_zmultiples,
+    AddSubgroup.map_le_map_iff', zmultiplesHom_ker_eq, Int.zmultiples_sup,
+    Int.zmultiples_le_zmultiples_iff, Int.natCast_dvd_natCast]
+
+/-- `zpowers (g ^ i) ≤ zpowers (g ^ j)` iff `j.gcd (orderOf g) ∣ i.gcd (orderOf g)`.
+This characterizes inclusion of cyclic subgroups of a group generated by integer powers of a
+single element. -/
+@[to_additive existing]
+theorem Subgroup.zpowers_le_zpowers_iff [Group G] (g : G) (i j : ℤ) :
+    zpowers (g ^ i) ≤ zpowers (g ^ j) ↔ j.gcd (orderOf g) ∣ i.gcd (orderOf g) :=
+  AddSubgroup.zmultiples_le_zmultiples_iff (Additive.ofMul g) i j
+
+/-- In any additive group, the index of `zmultiples (i • g)` relative to `zmultiples g` is the
+gcd of `i` and the order of `g`. -/
+theorem AddSubgroup.relIndex_zmultiples_zsmul [AddGroup G] (g : G) (i : ℤ) :
+    (zmultiples (i • g)).relIndex (zmultiples g) = i.gcd (addOrderOf g) := by
+  rw [← zmultiplesHom_apply, ← AddMonoidHom.map_zmultiples, ← range_zmultiplesHom g,
+    AddMonoidHom.range_eq_map, AddSubgroup.relIndex_map_map, top_sup_eq,
+    AddSubgroup.relIndex_top_right, zmultiplesHom_ker_eq, Int.zmultiples_sup,
+    Int.index_zmultiples, Int.natAbs_natCast]
+
+/-- In any group, the index of `zpowers (g ^ i)` relative to `zpowers g` is the gcd of `i` and
+the order of `g`. -/
+@[to_additive existing]
+theorem Subgroup.relIndex_zpowers_zpow [Group G] (g : G) (i : ℤ) :
+    (zpowers (g ^ i)).relIndex (zpowers g) = i.gcd (orderOf g) :=
+  AddSubgroup.relIndex_zmultiples_zsmul (Additive.ofMul g) i
+
+/-- In an additive group generated by `g`, the index of `zmultiples (i • g)` is the gcd of `i`
+and the order of `g`. -/
+theorem AddSubgroup.index_zmultiples_zsmul [AddGroup G] {g : G} (hg : zmultiples g = ⊤) (i : ℤ) :
+    (zmultiples (i • g)).index = i.gcd (addOrderOf g) := by
+  rw [← AddSubgroup.relIndex_top_right, ← hg, AddSubgroup.relIndex_zmultiples_zsmul]
+
+/-- In a group generated by `g`, the index of `zpowers (g ^ i)` is the gcd of `i` and the order
+of `g`. -/
+@[to_additive existing]
+theorem Subgroup.index_zpowers_zpow [Group G] {g : G} (hg : zpowers g = ⊤) (i : ℤ) :
+    (zpowers (g ^ i)).index = i.gcd (orderOf g) := by
+  rw [← Subgroup.relIndex_top_right, ← hg, Subgroup.relIndex_zpowers_zpow]
+
+/-- The subgroups generated by `g ^ i` and `g ^ j` are equal iff
+`i.gcd (orderOf g) = j.gcd (orderOf g)`. Compare `Subgroup.zpowers_eq_zpowers_iff`, which
+characterizes equality of `zpowers x` and `zpowers y` when `x` has infinite order. -/
+@[to_additive /-- The subgroups generated by `i • g` and `j • g` are equal iff
+`i.gcd (addOrderOf g) = j.gcd (addOrderOf g)`. Compare `AddSubgroup.zmultiples_eq_zmultiples_iff`,
+which characterizes equality of `zmultiples x` and `zmultiples y` when `x` has infinite order. -/]
+theorem Subgroup.zpowers_eq_zpowers_iff' [Group G] (g : G) (i j : ℤ) :
+    zpowers (g ^ i) = zpowers (g ^ j) ↔ i.gcd (orderOf g) = j.gcd (orderOf g) := by
+  rw [le_antisymm_iff, zpowers_le_zpowers_iff, zpowers_le_zpowers_iff,
+    ← Nat.dvd_antisymm_iff, eq_comm]
+
+@[to_additive]
+theorem Subgroup.zpowers_le_zpowers_of_dvd [Group G] (g : G) {m n : ℤ} (h : n ∣ m) :
+    zpowers (g ^ m) ≤ zpowers (g ^ n) :=
+  (zpowers_le_zpowers_iff g m n).mpr (Int.gcd_dvd_gcd_of_dvd_left _ h)
+
+/-- The subgroup generated by `g ^ i` and `g ^ j` is generated by `g ^ gcd i j`. -/
+@[to_additive /-- The subgroup generated by `i • g` and `j • g` is generated by `gcd i j • g`. -/]
+theorem Subgroup.zpowers_zpow_sup [Group G] (g : G) (i j : ℤ) :
+    zpowers (g ^ i) ⊔ zpowers (g ^ j) = zpowers (g ^ (i.gcd j : ℤ)) := by
+  apply le_antisymm
+  · exact sup_le (zpowers_le_zpowers_of_dvd g (gcd_dvd_left i j))
+      (zpowers_le_zpowers_of_dvd g (gcd_dvd_right i j))
+  · grw [Int.gcd_eq_gcd_ab, zpow_add, zpowers_mul_le_sup]
+    exact sup_le_sup (zpowers_le_zpowers_of_dvd g (dvd_mul_right i (i.gcdA j)))
+      (zpowers_le_zpowers_of_dvd g (dvd_mul_right j (i.gcdB j)))
 section addGenerator
 variable [AddGroup G] {g : G} (hg : ∀ x, x ∈ zmultiples g) {n : ℕ} (hn : Nat.card G = n)