The cyclic subgroup generated by an element

Facts about Subgroup.zpowers g that Mathlib does not name: when it meets a factor of a product trivially, that g generates it from inside, and what it is when g has order two.

For σ : G and τ : H, the cyclic subgroup generated by (σ, τ) meets the first factor G × 1 trivially as soon as orderOf σ ∣ orderOf τ.

The two factors behave differently: the meet with 1 × H is trivial under the reverse divisibility, so the two statements are not interchangeable and the direction matters at every call site.

No finiteness is assumed. orderOf x = 0 for an element of infinite order, so the hypothesis is also meaningful there, and covers the case of σ of infinite order.

References

The proof skeleton is adapted from cyclic_subgroup_meets_G_times_one_trivially in CebotarevDensity/Abelian.lean of CBirkbeck/chebotarev-density (Apache-2.0, Birkbeck--Brasca) at commit 8575c9df1ae0a61120ab5c964c7911414254bec7. That version assumes Nat.card G ∣ orderOf τ with both groups finite; the hypothesis here is weaker.

It also records that g, viewed inside the subgroup it generates, generates that subgroup: the canonical generator of zpowers g is ⟨g, mem_zpowers g⟩. Mathlib knows zpowers g is cyclic but does not name a generator, which is what a transport along an isomorphism out of zpowers g needs.

For an element of order two the subgroup is as small as it can be while being nontrivial: an integer power of g is determined by its exponent modulo orderOf g, so zpowers g is {1, g}. That membership normal form is what a two-element complement in a semidirect decomposition is used through, for instance the subgroup generated by a reflection in a dihedral group. In a commutative group with distributive negation the squares of {1, -1} are trivial, so {±1} has index 2 over its subgroup of squares when -1 ≠ 1.

Main results

• Subgroup.zpowers_inf_top_prod_bot_eq_bot_of_orderOf_dvd
• Subgroup.zpowers_mk_self_eq_top, with its additive form
• Subgroup.exists_coprime_zpow_of_generators, and its additive form AddSubgroup.exists_coprime_zsmul_of_generators: two generators differ by an integer power or multiple coprime to the group's cardinality.
• Subgroup.mem_zpowers_iff_of_orderOf_eq_two: the subgroup generated by an element of order two is {1, g}; Subgroup.mem_zpowers_neg_one_iff: the subgroup generated by -1 is {1, -1}
• Subgroup.map_powMonoidHom_two_zpowers_neg_one: {±1}² = 1; Subgroup.relIndex_map_powMonoidHom_two_zpowers_neg_one: ({±1} : {±1}²) = 2 when -1 ≠ 1

theorem Subgroup.zpowers_inf_top_prod_bot_eq_bot_of_orderOf_dvd {G : Type u_1} {H : Type u_2} [Group G] [Group H] (σ : G) (τ : H) (hστ : orderOf σ ∣ orderOf τ) : zpowers (σ, τ) ⊓ ⊤.prod ⊥ = ⊥

A cyclic subgroup of a product meets the first factor trivially, whenever the order of the first coordinate divides that of the second: ⟨(σ, τ)⟩ ⊓ (G × 1) = 1.

For the meet with the second factor 1 × H, the divisibility runs the other way.

@[simp]

theorem Subgroup.zpowers_mk_self_eq_top {G : Type u_1} [Group G] (g : G) : zpowers ⟨g, ⋯⟩ = ⊤

An element generates the subgroup it generates. Inside zpowers g, the canonical element ⟨g, mem_zpowers g⟩ has all of zpowers g for its own zpowers.

Mathlib supplies IsCyclic ↥(zpowers g) as an instance but names no generator, so this is what a transport along an isomorphism out of zpowers g consumes.

@[simp]

theorem AddSubgroup.zmultiples_mk_self_eq_top {G : Type u_1} [AddGroup G] (g : G) : zmultiples ⟨g, ⋯⟩ = ⊤

An element generates the subgroup it generates. Inside zmultiples g, the canonical element ⟨g, mem_zmultiples g⟩ has all of zmultiples g for its own zmultiples.

theorem Subgroup.exists_coprime_zpow_of_generators {G : Type u_1} [Group G] (q r : G) (hq : zpowers q = ⊤) (hr : zpowers r = ⊤) : ∃ (k : ℤ), k.gcd ↑(Nat.card G) = 1 ∧ r = q ^ k

If q and r both generate a group, then r is an integer power of q with exponent coprime to the cardinality of the group. This includes infinite cyclic groups, whose Nat.card is zero.

theorem AddSubgroup.exists_coprime_zsmul_of_generators {G : Type u_1} [AddGroup G] (q r : G) (hq : zmultiples q = ⊤) (hr : zmultiples r = ⊤) : ∃ (k : ℤ), k.gcd ↑(Nat.card G) = 1 ∧ r = k • q

If q and r both generate an additive group, then r = k • q for an integer k coprime to the group's cardinality. This includes infinite cyclic groups.

theorem Subgroup.mem_zpowers_iff_of_orderOf_eq_two {G : Type u_1} [Group G] {g x : G} (hg : orderOf g = 2) : x ∈ zpowers g ↔ x = 1 ∨ x = g

The subgroup generated by an element of order two is {1, g}. An integer power of g is determined by its exponent modulo orderOf g = 2, and only the residues 0 and 1 occur.

Not a simp lemma: the hypothesis orderOf g = 2 is not one simp can discharge on its own, so the specializations at concrete elements of order two are what carry the simp attribute.

theorem Subgroup.mem_zpowers_neg_one_iff {G : Type u_1} [Group G] [HasDistribNeg G] (h : -1 ≠ 1) {x : G} : x ∈ zpowers (-1) ↔ x = 1 ∨ x = -1

The subgroup generated by -1 is {1, -1}, as soon as -1 ≠ 1.

theorem Subgroup.map_powMonoidHom_two_zpowers_neg_one {G : Type u_1} [CommGroup G] [HasDistribNeg G] : map (powMonoidHom 2) (zpowers (-1)) = ⊥

Squaring kills the subgroup generated by -1: {±1}² = 1.

theorem Subgroup.relIndex_map_powMonoidHom_two_zpowers_neg_one {G : Type u_1} [CommGroup G] [HasDistribNeg G] (h : -1 ≠ 1) : (map (powMonoidHom 2) (zpowers (-1))).relIndex (zpowers (-1)) = 2

The subgroup generated by -1 has index 2 over its squares, as soon as -1 ≠ 1.