Membership in a subgroup of a cyclic group, by index, and indices of intersections

In a group generated by g, a power g ^ n lies in a subgroup K exactly when the index of K divides n: the exponents landing in K are the multiples of K.index. When K has finite index that makes K.index the least positive such exponent; when it does not, no positive exponent lands in K at all, and both readings agree through the convention index = 0.

Consequently the index of an intersection of two subgroups of a cyclic group is the least common multiple of their indices. The same holds modulo a normal subgroup N with cyclic quotient, as long as the order of N is prime to its index and to the index of one of the two subgroups.

Main results

• Subgroup.zpow_mem_iff_index_dvd: g ^ n ∈ K ↔ (K.index : ℤ) ∣ n for n : ℤ, with g a generator.
• Subgroup.pow_mem_iff_index_dvd: the same for a natural exponent.
• Subgroup.isLeast_pow_mem_index: when K has finite index, K.index is the least positive exponent with g ^ n ∈ K, with AddSubgroup.isLeast_nsmul_mem_index its additive form.
• Subgroup.isLeast_pow_mem_relIndex_zpowers: when H has finite relative index in ⟨g⟩, that relative index is the least positive exponent with g ^ n ∈ H. No generator hypothesis is needed here, g generating ⟨g⟩; AddSubgroup.isLeast_nsmul_mem_relIndex_zmultiples is the additive form.
• IsCyclic.index_inf_eq_lcm: in a cyclic group the index of H ⊓ K is the least common multiple of the indices of H and K.
• Subgroup.index_inf_eq_lcm_of_isCyclic_quotient: the same holds in a group with a normal subgroup N whose quotient is cyclic and whose order is prime to its index, provided the order of N is prime to the index of one of the two subgroups. This is the group theory behind Abhyankar's lemma, where N is the wild inertia group inside the inertia group.

@[simp]

theorem Subgroup.zpow_mem_iff_index_dvd {G : Type u_1} [Group G] {g : G} (K : Subgroup G) (hg : zpowers g = ⊤) (n : ℤ) : g ^ n ∈ K ↔ ↑K.index ∣ n

Membership in a subgroup of a cyclic group is divisibility of the index. If g generates G, then g ^ n lies in K exactly when K.index divides n.

This is the criterion a fibre-selection argument wants: it turns a membership test on powers of a generator into arithmetic in ℤ, and identifies K.index as the least positive exponent landing in K.

No finiteness is assumed. If K has infinite index its index is 0 by convention, and the statement reads g ^ n ∈ K ↔ n = 0.

@[simp]

theorem AddSubgroup.zsmul_mem_iff_index_dvd {G : Type u_1} [AddGroup G] {g : G} (K : AddSubgroup G) (hg : zmultiples g = ⊤) (n : ℤ) : n • g ∈ K ↔ ↑K.index ∣ n

Membership in a subgroup of an additive cyclic group is divisibility of the index. If g generates G, then n • g lies in K exactly when K.index divides n.

@[simp]

theorem Subgroup.pow_mem_iff_index_dvd {G : Type u_1} [Group G] {g : G} (K : Subgroup G) (hg : zpowers g = ⊤) (n : ℕ) : g ^ n ∈ K ↔ K.index ∣ n

The natural-exponent form. g ^ n ∈ K ↔ K.index ∣ n, the case n : ℕ of zpow_mem_iff_index_dvd.

@[simp]

theorem AddSubgroup.nsmul_mem_iff_index_dvd {G : Type u_1} [AddGroup G] {g : G} (K : AddSubgroup G) (hg : zmultiples g = ⊤) (n : ℕ) : n • g ∈ K ↔ K.index ∣ n

The natural-exponent form. n • g ∈ K ↔ K.index ∣ n.

theorem Subgroup.isLeast_pow_mem_index {G : Type u_1} [Group G] {g : G} (K : Subgroup G) (hg : zpowers g = ⊤) [K.FiniteIndex] : IsLeast {n : ℕ | 0 < n ∧ g ^ n ∈ K} K.index

The index is the least exponent that lands in K. For a generator g of G and a subgroup K of finite index, K.index is the smallest n ≥ 1 with g ^ n ∈ K.

This is the finite-index reading of pow_mem_iff_index_dvd: the exponents landing in K are the multiples of K.index, so the least positive one is the index itself.

theorem AddSubgroup.isLeast_nsmul_mem_index {G : Type u_1} [AddGroup G] {g : G} (K : AddSubgroup G) (hg : zmultiples g = ⊤) [K.FiniteIndex] : IsLeast {n : ℕ | 0 < n ∧ n • g ∈ K} K.index

The index is the least multiple that lands in K. For a generator g of G and a subgroup K of finite index, K.index is the smallest n ≥ 1 with n • g ∈ K.

theorem Subgroup.isLeast_pow_mem_relIndex_zpowers {G : Type u_1} [Group G] (g : G) (H : Subgroup G) [H.IsFiniteRelIndex (zpowers g)] : IsLeast {n : ℕ | 0 < n ∧ g ^ n ∈ H} (H.relIndex (zpowers g))

The relative index in a cyclic subgroup is the least exponent that lands in H. When H has finite relative index in ⟨g⟩, that index is the smallest n ≥ 1 with g ^ n ∈ H.

Unlike isLeast_pow_mem_index, no hypothesis on g is needed: g generates ⟨g⟩, so this applies to an arbitrary element of an arbitrary group, asking only that H ⊓ ⟨g⟩ have finite index in ⟨g⟩. Use it when the quantity wanted is the least power of a given element that lies in a given subgroup.

theorem AddSubgroup.isLeast_nsmul_mem_relIndex_zmultiples {G : Type u_1} [AddGroup G] (g : G) (H : AddSubgroup G) [H.IsFiniteRelIndex (zmultiples g)] : IsLeast {n : ℕ | 0 < n ∧ n • g ∈ H} (H.relIndex (zmultiples g))

The relative index in a cyclic subgroup is the least multiple that lands in H. When H has finite relative index in ⟨g⟩, that index is the smallest n ≥ 1 with n • g ∈ H.

theorem IsCyclic.index_inf_eq_lcm {G : Type u_1} [Group G] [IsCyclic G] (H K : Subgroup G) : (H ⊓ K).index = H.index.lcm K.index

Indices of intersections in a cyclic group. In a cyclic group, the index of H ⊓ K is the least common multiple of the indices of H and K.

No finiteness is assumed: with the convention index = 0 for infinite index, both sides vanish exactly when one of H and K has infinite index.

theorem IsAddCyclic.index_inf_eq_lcm {G : Type u_1} [AddGroup G] [IsAddCyclic G] (H K : AddSubgroup G) : (H ⊓ K).index = H.index.lcm K.index

Indices of intersections in an additive cyclic group. The index of H ⊓ K is the least common multiple of the indices of H and K.

theorem Subgroup.index_inf_eq_lcm_of_isCyclic_quotient {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [IsCyclic (G ⧸ N)] (hN : (Nat.card ↥N).Coprime N.index) {A : Subgroup G} (hA : (Nat.card ↥N).Coprime A.index) (B : Subgroup G) : (A ⊓ B).index = A.index.lcm B.index

Indices of intersections modulo a normal subgroup with cyclic quotient. Let N be a normal subgroup of G with G ⧸ N cyclic and with the order of N prime to its index. If the order of N is also prime to the index of A, then for every subgroup B the index of A ⊓ B is the least common multiple of the indices of A and B.

When N is a p-group, the hypotheses say that p divides neither [G : N] nor [G : A]. This is the shape of an inertia group, with N its wild part, and it is what Abhyankar's lemma on the ramification index in a compositum reduces to. Without the hypothesis on A the conclusion fails: in (ℤ / p) × (ℤ / p) with N the whole group, two distinct subgroups A and B of order p have index p each while A ⊓ B = ⊥ has index p ^ 2.