English
Let α be a finite set and f: α → α a map with f^{p^n} = id, where p is prime. Then the size of α is congruent to the number of fixed points of f modulo p.
Русский
Пусть α — конечное множество и f: α → α такая, что f^{p^n} = id, где p — простое число. Тогда |α| ≡ |Fix(f)| (mod p).
LaTeX
$$$(f^{p^n} = \\mathrm{id}_X) \\land (\\text{p is prime}) \\implies |X| \\equiv |\\mathrm{Fix}(f)| \\pmod{p}$$$
Lean4
/-- The number of fixed points of a `p ^ n`-th root of the identity function over a finite set
and the set's cardinality have the same residue modulo `p`, where `p` is a prime. -/
theorem card_fixedPoints_modEq [DecidableEq α] {f : Function.End α} {p n : ℕ} [hp : Fact p.Prime] (hf : f ^ p ^ n = 1) :
Fintype.card α ≡ Fintype.card f.fixedPoints [MOD p] :=
by
let σ : α ≃ α :=
⟨f, f ^ (p ^ n - 1), leftInverse_iff_comp.mpr ((pow_sub_mul_pow f (Nat.one_le_pow n p hp.out.pos)).trans hf),
leftInverse_iff_comp.mpr ((pow_mul_pow_sub f (Nat.one_le_pow n p hp.out.pos)).trans hf)⟩
have hσ : σ ^ p ^ n = 1 := by
rw [DFunLike.ext'_iff, coe_pow]
exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf
suffices Fintype.card f.fixedPoints = (support σ)ᶜ.card from this ▸ (card_compl_support_modEq hσ).symm
suffices f.fixedPoints = (support σ)ᶜ by simp only [this]; apply Fintype.card_coe
simp [σ, Set.ext_iff, IsFixedPt]
