English
For a finite p-group action, |α| ≡ |Fix| (mod p).
Русский
При действии p-группы на конечном множестве сохранение: |α| ≡ |Fix| (mod p).
LaTeX
$$$\IsPGroup(p,G) \rightarrow [hp : Fact (Nat.Prime p)] (\alpha) [MulAction G \alpha] [Finite\ \alpha], Nat.card\alpha \equiv Nat.card( fixedPoints G \alpha).Elem [MOD p]$$$
Lean4
/-- If `G` is a `p`-group acting on a finite set `α`, then the number of fixed points
of the action is congruent mod `p` to the cardinality of `α` -/
theorem card_modEq_card_fixedPoints : Nat.card α ≡ Nat.card (fixedPoints G α) [MOD p] :=
by
have := Fintype.ofFinite α
have := Fintype.ofFinite (fixedPoints G α)
rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
classical
calc
card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
_ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
_ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
_ = _ := by simp
rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
have key : ∀ x, card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } = card (orbit G x) :=
fun x => by simp only [Quotient.eq'']; congr
refine
Eq.symm
(Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
(fun a₁ _ _ a₂ _ _ h => Subtype.eq (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
(fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
obtain ⟨k, hk⟩ := hG.card_orbit b
rw [Nat.card_eq_fintype_card] at hk
have : k = 0 := by
contrapose! hb
simp [-Quotient.eq, key, hk, hb]
exact
⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩, Finset.mem_univ _,
ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩
