Fixed-point candidates through a finite kernel #
The fixed-subgroup isomorphism induced by an equivariant surjection with finite, fixed-point-free
kernel transports the derived subgroup modulo its own centre. This extends the existing
TauCeti.FixedPointCandidate.congr to homomorphisms that need not be injective. It asserts neither
finiteness nor simplicity of the candidates.
noncomputable def
TauCeti.FixedPointCandidate.congrOfFiniteKer
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
{F : G →* G}
{F' : H →* H}
(ψ : G →* H)
[Finite ↥ψ.ker]
(hψ : ψ.comp F = F'.comp ψ)
(hsurj : Function.Surjective ⇑ψ)
(hker : Disjoint ψ.ker (fixedSubgroup F))
:
Transport the candidate through an equivariant surjection with finite kernel whose only fixed point is the identity.
Instances For
@[simp]
theorem
TauCeti.FixedPointCandidate.congrOfFiniteKer_mk
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
{F : G →* G}
{F' : H →* H}
(ψ : G →* H)
[Finite ↥ψ.ker]
(hψ : ψ.comp F = F'.comp ψ)
(hsurj : Function.Surjective ⇑ψ)
(hker : Disjoint ψ.ker (fixedSubgroup F))
(x : ↥(commutator ↥(fixedSubgroup F)))
:
(congrOfFiniteKer ψ hψ hsurj hker) ↑x = ↑((ψ.fixedSubgroupCongrOfFiniteKer hψ hsurj hker).commutatorCongr x)