English
The range of kerParam g equals the image under the centralizer map of the toPermHom ker.
Русский
Образ kerParam g совпадает с образом центральизатора через toPermHom ker.
LaTeX
$$kerParam g).range = (toPermHom g).ker.map (Subgroup.subtype _)$$
Lean4
theorem kerParam_apply {u : Perm (Function.fixedPoints g)} {v : (c : g.cycleFactorsFinset) → Subgroup.zpowers c.val}
{x : α} :
kerParam g (u, v) x =
if hx : g.cycleOf x ∈ g.cycleFactorsFinset then (v ⟨g.cycleOf x, hx⟩ : Perm α) x else ofSubtype u x :=
by
split_ifs with hx
· have hx' := hx
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, Ne, ← Function.mem_fixedPoints_iff] at hx'
rw [kerParam, MonoidHom.noncommCoprod_apply', mul_apply, ofSubtype_apply_of_not_mem u hx', noncommPiCoprod_apply, ←
Finset.noncommProd_erase_mul _ (Finset.mem_univ ⟨g.cycleOf x, hx⟩), mul_apply, ← notMem_support]
contrapose! hx'
obtain ⟨a, ha1, ha2⟩ := mem_support_of_mem_noncommProd_support hx'
simp only [Finset.mem_erase, Finset.mem_univ, and_true, Ne, Subtype.ext_iff] at ha1
have key := cycleFactorsFinset_pairwise_disjoint g a.2 hx ha1
rw [disjoint_iff_disjoint_support, Finset.disjoint_left] at key
obtain ⟨k, hk⟩ := mem_zpowers_iff.mp (v a).2
replace ha2 := key (support_zpow_le a.1 k (hk ▸ ha2))
obtain ⟨k, hk⟩ := mem_zpowers_iff.mp (v ⟨g.cycleOf x, hx⟩).2
rwa [← hk, zpow_apply_mem_support, notMem_support, cycleOf_apply_self] at ha2
· rw [cycleOf_mem_cycleFactorsFinset_iff] at hx
rw [kerParam, MonoidHom.noncommCoprod_apply, mul_apply, Equiv.apply_eq_iff_eq, ← notMem_support]
contrapose! hx
obtain ⟨a, -, ha⟩ :=
mem_support_of_mem_noncommProd_support (comm := fun a ha b hb h ↦
g.pairwise_commute_of_mem_zpowers h (v a) (v b) (v a).2 (v b).2) hx
exact support_zpowers_of_mem_cycleFactorsFinset_le (v a) ha
