Documentation

TauCeti.GroupTheory.FixedPointCandidate

The candidate simple group attached to an endomorphism #

For an endomorphism F of a group G this file composes the two constructions of TauCeti.GroupTheory.FixedSubgroup and TauCeti.GroupTheory.DerivedCentralQuotient into

FixedPointCandidate F = [H, H] / Z([H, H]),  where  H = fixedSubgroup F,

the group the classification's Lie-type lane attaches to a Steinberg endomorphism of a pinned algebraic group. Nothing here asserts that the result is finite or simple, and no ambient group is involved: the composite is a carrier-independent prerequisite for the later family-by-family construction.

Both steps of the recipe transport along an isomorphism, so the composite does too: TauCeti.FixedPointCandidate.congr turns an isomorphism ψ : G ≃* G' intertwining F with an endomorphism F' of G' into an isomorphism of the two candidates. The candidate therefore depends only on the isomorphism class of the pair (G, F), which is what lets a construction of (G, F) be replaced by another realization of it without changing the group named.

Main definitions #

References #

This is the composite prescribed by milestone L3 of TauCetiRoadmap/CFSGStatement/README.md, which fixes H_d = fixedSubgroup d.steinberg and d.Group = [H_d, H_d] / Z([H_d, H_d]), with the centre read as the centre of the derived subgroup rather than of H_d. The construction is standard; see R. W. Carter, Simple Groups of Lie Type, and D. Gorenstein, R. Lyons and R. Solomon, The Classification of the Finite Simple Groups.

source
@[reducible, inline]
abbrev TauCeti.FixedPointCandidate {G : Type u_1} [Group G] (F : G →* G) :
Type u_1

The candidate simple group attached to an endomorphism F of a group: the derived subgroup of the fixed points of F, modulo the centre of that derived subgroup.

For the Steinberg endomorphisms constructed by the roadmap, this is the corresponding finite group of Lie type outside the small parameters excluded by LieTypeIndex.InStandardRange; at those parameters it can be trivial, nonsimple, a duplicate, or the separately indexed Tits group. None of these properties is asserted here.

Equations
Instances For
    source
    def TauCeti.FixedPointCandidate.congr {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] {F : G →* G} {F' : G' →* G'} (ψ : G ≃* G') (hψ : (↑ψ).comp F = F'.comp ↑ψ) :
    FixedPointCandidate F ≃* FixedPointCandidate F'

    The candidate simple group transported along an isomorphism intertwining the two endomorphisms.

    The isomorphism carries the fixed subgroup of the one onto the fixed subgroup of the other, and the derived central quotient of isomorphic groups are isomorphic, so the candidate depends only on the isomorphism class of the pair (G, F).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.FixedPointCandidate.congr_mk {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] {F : G →* G} {F' : G' →* G'} (ψ : G ≃* G') (hψ : (↑ψ).comp F = F'.comp ↑ψ) (x : ↥(commutator ↥(fixedSubgroup F))) :
      (congr ψ hψ) ↑x = ↑((fixedSubgroupCongr ψ hψ).commutatorCongr x)
      source
      @[simp]
      theorem TauCeti.FixedPointCandidate.congr_refl {G : Type u_1} [Group G] {F : G →* G} (hψ : (↑(MulEquiv.refl G)).comp F = F.comp ↑(MulEquiv.refl G)) :
      congr (MulEquiv.refl G) hψ = MulEquiv.refl (FixedPointCandidate F)
      source
      @[simp]
      theorem TauCeti.FixedPointCandidate.congr_trans {G : Type u_1} [Group G] {G' : Type u_2} {G'' : Type u_3} [Group G'] [Group G''] {F : G →* G} {F' : G' →* G'} {F'' : G'' →* G''} (ψ : G ≃* G') (hψ : (↑ψ).comp F = F'.comp ↑ψ) (χ : G' ≃* G'') (hχ : (↑χ).comp F' = F''.comp ↑χ) :
      (congr ψ hψ).trans (congr χ hχ) = congr (ψ.trans χ) ⋯
      source
      @[simp]
      theorem TauCeti.FixedPointCandidate.congr_symm {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] {F : G →* G} {F' : G' →* G'} (ψ : G ≃* G') (hψ : (↑ψ).comp F = F'.comp ↑ψ) :
      (congr ψ hψ).symm = congr ψ.symm ⋯