English
The KerParam construction parametrizes the kernel of the centralizer-to-permutation map by a product of subgroups indexed by cycle-factors and fixed points.
Русский
Построение KerParam параметризует ядро отображения к центральизатору в перестановки как произведение подгрупп, индексируемых по циклофакторам и фиксированным точкам.
LaTeX
$$kerParam g : (Perm (Function.fixedPoints g)) × ((c : g.cycleFactorsFinset) → Subgroup.zpowers c.val) →* Perm α$$
Lean4
theorem nat_card_range_toPermHom : Nat.card (toPermHom g).range = ∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)! :=
by
classical
set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
suffices Fintype.card (toPermHom g).range = Fintype.card {k : Perm g.cycleFactorsFinset | sc ∘ k = sc}
by
simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc, Finset.univ_eq_attach]
simp_rw [← CycleType.count_def]
apply Finset.prod_congr _ (fun _ _ => rfl)
ext n
simp only [Finset.mem_image, Finset.mem_attach, true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
simp only [← SetLike.coe_sort_coe, Fintype.card_eq_nat_card]
congr
ext
rw [SetLike.mem_coe, mem_range_toPermHom_iff', Set.mem_setOf_eq]
