English
There is a long composition of equivalences that yields a bijection between the sigma-fixed-by product and orbits; the proof is by a chain of equivalences.
Русский
Существует цепочка эквив, приводящая к биекции между суммой фиксированных по группе и орбитами.
LaTeX
$$(Σ a : α, fixedBy β a) ≃ Ω × α$$
Lean4
theorem normalCore_eq_ker : H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker :=
by
apply le_antisymm
· intro g hg
apply Equiv.Perm.ext
refine fun q ↦ QuotientGroup.induction_on q ?_
refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)
rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
exact H.normalCore.inv_mem hg g'⁻¹
· refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)
rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))
