Fixed points through a finite kernel #
A surjective homomorphism intertwining two group endomorphisms induces an isomorphism of their
fixed subgroups when its kernel is finite and has no nonidentity fixed point. Neither endomorphism
needs to be invertible. The lifting argument corrects an arbitrary lift by an element of the kernel,
using MonoidHom.FixedPointFree.commutatorMap_surjective.
theorem
MonoidHom.existsUnique_fixed_lift_of_finite_ker
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
(ψ : G →* H)
{F : G →* G}
{F' : H →* H}
[Finite ↥ψ.ker]
(hψ : ψ.comp F = F'.comp ψ)
(hsurj : Function.Surjective ⇑ψ)
(hker : Disjoint ψ.ker (TauCeti.fixedSubgroup F))
{y : H}
(hy : F' y = y)
:
A fixed point has a unique fixed lift through an equivariant surjection with finite kernel whose only fixed point is the identity.
noncomputable def
MonoidHom.fixedSubgroupCongrOfFiniteKer
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
(ψ : G →* H)
{F : G →* G}
{F' : H →* H}
[Finite ↥ψ.ker]
(hψ : ψ.comp F = F'.comp ψ)
(hsurj : Function.Surjective ⇑ψ)
(hker : Disjoint ψ.ker (TauCeti.fixedSubgroup F))
:
Restriction of an equivariant surjection to fixed subgroups, when its finite kernel has no nonidentity fixed point. Its inverse sends a point to its unique fixed lift.
Instances For
@[simp]
theorem
MonoidHom.coe_fixedSubgroupCongrOfFiniteKer_apply
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
(ψ : G →* H)
{F : G →* G}
{F' : H →* H}
[Finite ↥ψ.ker]
(hψ : ψ.comp F = F'.comp ψ)
(hsurj : Function.Surjective ⇑ψ)
(hker : Disjoint ψ.ker (TauCeti.fixedSubgroup F))
(x : ↥(TauCeti.fixedSubgroup F))
:
@[simp]
theorem
MonoidHom.map_fixedSubgroupCongrOfFiniteKer_symm_apply
{G : Type u_1}
{H : Type u_2}
[Group G]
[Group H]
(ψ : G →* H)
{F : G →* G}
{F' : H →* H}
[Finite ↥ψ.ker]
(hψ : ψ.comp F = F'.comp ψ)
(hsurj : Function.Surjective ⇑ψ)
(hker : Disjoint ψ.ker (TauCeti.fixedSubgroup F))
(y : ↥(TauCeti.fixedSubgroup F'))
: