English
The stabilizer cardinality equals the product of factorials of fibre sizes, with a codomain indexed by i in the image of f.
Русский
Кардинал стабилизатора равен произведению факториалов размеров волокон, индексированных значениями изображения функции.
LaTeX
$$Fintype.card { g : Perm α // f ∘ g = f } = (\prod i ∈ image f, Fintype.card({a // f a = i}))!$$
Lean4
/-- The cardinality of the type of permutations preserving a function
(without the finiteness assumption on target) -/
theorem stabilizer_card' :
Fintype.card { g : Perm α // f ∘ g = f } = ∏ i ∈ Finset.univ.image f, (Fintype.card ({ a // f a = i }))! :=
by
set φ : α → Finset.univ.image f := Set.codRestrict f (Finset.univ.image f) (fun a => by simp)
suffices ∀ g : Perm α, f ∘ g = f ↔ φ ∘ g = φ
by
simp only [this, stabilizer_card]
apply Finset.prod_bij (fun g _ => g.val)
· exact fun g _ => Finset.coe_mem g
· exact fun g _ g' _ => SetCoe.ext
· simp
· intro i _
apply congr_arg
apply Fintype.card_congr
apply Equiv.subtypeEquiv (Equiv.refl α)
intro a
rw [refl_apply, ← Subtype.coe_inj]
simp only [φ, Set.val_codRestrict_apply]
· intro g
simp only [funext_iff]
apply forall_congr'
intro a
simp only [Function.comp_apply, φ, ← Subtype.coe_inj, Set.val_codRestrict_apply]
