English
If a group K acts on a cyclic p-group G of coprime order, then the map (k,g) ↦ k•g g^{-1} is either trivial or surjective.
Русский
Если группа K действует на циклическую p-группу G порядка, взаимно простого по отношению к |K|, то отображение (k,g) ↦ k•g g^{-1} либо тривиально, либо сюръективно.
LaTeX
$$$(\\forall g\\in G)(\\forall k\\in K)(k\\cdot g\\,g^{-1}=1) \\lor (\\forall g\\in G)(\\exists k\\in K)(\\exists q\\in G,\, k\\cdot q\\,q^{-1}=g)$$$
Lean4
/-- If a group `K` acts on a cyclic `p`-group `G` of coprime order, then the map `K × G → G`
defined by `(k, g) ↦ k • g * g⁻¹` is either trivial or surjective. -/
theorem smul_mul_inv_trivial_or_surjective [IsCyclic G] (hG : IsPGroup p G) {K : Type*} [Group K]
[MulDistribMulAction K G] (hGK : (Nat.card G).Coprime (Nat.card K)) :
(∀ g : G, ∀ k : K, k • g * g⁻¹ = 1) ∨ (∀ g : G, ∃ k : K, ∃ q : G, k • q * q⁻¹ = g) :=
by
by_cases hc : Nat.card G = 0
· rw [hc, Nat.coprime_zero_left, Nat.card_eq_one_iff_unique] at hGK
simp [← hGK.1.elim 1]
have := Nat.finite_of_card_ne_zero hc
let ϕ := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K rfl
have h (g : G) (k : K) (n : ℤ) (h : ϕ k - 1 = n) : k • g * g⁻¹ = g ^ n :=
by
rw [sub_eq_iff_eq_add, ← Int.cast_one, ← Int.cast_add] at h
rw [MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply rfl k g (n + 1) h, zpow_add_one, mul_inv_cancel_right]
replace hG k : ϕ k = 1 ∨ IsUnit (ϕ k - 1) :=
by
obtain ⟨n, hn⟩ := hG.exists_card_eq
exact
ZMod.eq_one_or_isUnit_sub_one hn (ϕ k)
(hGK.symm.coprime_dvd_left ((orderOf_map_dvd ϕ k).trans (orderOf_dvd_natCard k)))
rcases forall_or_exists_not (fun k : K ↦ ϕ k = 1) with hϕ | ⟨k, hk⟩
· exact Or.inl fun p k ↦ by rw [h p k 0 (by rw [hϕ, sub_self, Int.cast_zero]), zpow_zero]
· obtain ⟨⟨u, v, -, hvu⟩, hu : u = ϕ k - 1⟩ := (hG k).resolve_left hk
rw [← u.intCast_zmod_cast] at hu hvu
rw [← v.intCast_zmod_cast, ← Int.cast_mul, ← Int.cast_one, ZMod.intCast_eq_intCast_iff] at hvu
refine Or.inr fun p ↦ zpow_one p ▸ ⟨k, p ^ (v.cast : ℤ), ?_⟩
rw [h (p ^ v.cast) k u.cast hu.symm, ← zpow_mul, zpow_eq_zpow_iff_modEq]
exact hvu.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard p))
