Documentation

TauCeti.GroupTheory.FixedSubgroup

The fixed points of an endomorphism #

Let F be an endomorphism of a group G. This file studies the subgroup

fixedSubgroup F = F.eqLocus (MonoidHom.id G)

of points of G fixed by F: when it is everything, how it grows along the powers of F, and how it transports along an isomorphism of the ambient group.

An isomorphism ψ : G ≃* G' intertwines F with an endomorphism F' of G' when ψ ∘ F = F' ∘ ψ. Such a ψ carries fixedSubgroup F onto fixedSubgroup F', so the pair (G, F) determines its fixed subgroup up to isomorphism and not merely up to inclusion. The one-sided statement for a homomorphism is TauCeti.map_fixedSubgroup_le; the two-sided statements are TauCeti.map_fixedSubgroup_eq and TauCeti.fixedSubgroupCongr.

Main definitions and results #

References #

The fixed subgroup of a Steinberg endomorphism of a connected reductive group is a finite group of Lie type; see R. W. Carter, Simple Groups of Lie Type.

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

The subgroup of points fixed by an endomorphism of a group, F.eqLocus (MonoidHom.id G).

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.mem_fixedSubgroup {G : Type u_1} [Group G] {F : G →* G} {x : G} :
    x ∈ fixedSubgroup F ↔ F x = x

    A point lies in the fixed subgroup of F exactly when F fixes it.

    source
    theorem TauCeti.fixedSubgroup_eq_top_iff {G : Type u_1} [Group G] {F : G →* G} :
    fixedSubgroup F = ⊤ ↔ F = MonoidHom.id G

    Only the identity fixes every point.

    source
    theorem TauCeti.fixedSubgroup_le_fixedSubgroup_pow {G : Type u_1} [Group G] (F : Monoid.End G) (n : ℕ) :
    fixedSubgroup F ≤ fixedSubgroup (F ^ n)

    A point fixed by an endomorphism is fixed by each of its powers.

    In particular, when some power of a Steinberg endomorphism is a Frobenius map (its square, for the Suzuki and Ree groups), the fixed group of the Steinberg endomorphism lies inside the fixed group of that Frobenius map.

    source
    theorem TauCeti.fixedSubgroup_inf_fixedSubgroup_le_fixedSubgroup_comp {G : Type u_1} [Group G] (F F' : G →* G) :
    fixedSubgroup F ⊓ fixedSubgroup F' ≤ fixedSubgroup (F'.comp F)

    A point fixed by each of two endomorphisms is fixed by their composite.

    The converse fails in general: a Steinberg endomorphism is a composite of a Frobenius with a diagram automorphism, and its fixed points are not in general fixed by either factor.

    This is the subgroup-packaged form of Function.inter_subset_fixedPoints_comp.

    source
    theorem TauCeti.map_fixedSubgroup_le {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 ψ) :
    Subgroup.map ψ (fixedSubgroup F) ≤ fixedSubgroup F'

    A homomorphism intertwining two endomorphisms carries the points fixed by the one to the points fixed by the other.

    source
    theorem TauCeti.map_subtype_fixedSubgroup_of_coe_eq {G : Type u_1} [Group G] {S : Subgroup G} (F : ↥S →* ↥S) (f : G →* G) (hF : ∀ (g : ↥S), ↑(F g) = f ↑g) :
    Subgroup.map S.subtype (fixedSubgroup F) = S ⊓ fixedSubgroup f

    Fixed points of an endomorphism of a subgroup, read in the ambient group. If an endomorphism F of S ≤ G is the restriction of an endomorphism f of G, then the image of its fixed subgroup in G is S ⊓ fixedSubgroup f.

    Transport along an isomorphism of the ambient group #

    source
    theorem TauCeti.map_fixedSubgroup_eq {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 ↑ψ) :
    Subgroup.map (↑ψ) (fixedSubgroup F) = fixedSubgroup F'

    An isomorphism intertwining two endomorphisms carries the points fixed by the one onto the points fixed by the other.

    source
    def TauCeti.fixedSubgroupCongr {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 ↑ψ) :
    ↥(fixedSubgroup F) ≃* ↥(fixedSubgroup F')

    The isomorphism of fixed subgroups induced by an isomorphism intertwining the two endomorphisms.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.coe_fixedSubgroupCongr_apply {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 : ↥(fixedSubgroup F)) :
      ↑((fixedSubgroupCongr ψ hψ) x) = ψ ↑x
      source
      @[simp]
      theorem TauCeti.coe_fixedSubgroupCongr_symm_apply {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 ↑ψ) (y : ↥(fixedSubgroup F')) :
      ↑((fixedSubgroupCongr ψ hψ).symm y) = ψ.symm ↑y
      source
      @[simp]
      theorem TauCeti.fixedSubgroupCongr_refl {G : Type u_1} [Group G] {F : G →* G} (hψ : (↑(MulEquiv.refl G)).comp F = F.comp ↑(MulEquiv.refl G)) :
      fixedSubgroupCongr (MulEquiv.refl G) hψ = MulEquiv.refl ↥(fixedSubgroup F)
      source
      @[simp]
      theorem TauCeti.fixedSubgroupCongr_trans {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] {F : G →* G} {F' : G' →* G'} {G'' : Type u_3} [Group G''] {F'' : G'' →* G''} (ψ : G ≃* G') (hψ : (↑ψ).comp F = F'.comp ↑ψ) (χ : G' ≃* G'') (hχ : (↑χ).comp F' = F''.comp ↑χ) :
      (fixedSubgroupCongr ψ hψ).trans (fixedSubgroupCongr χ hχ) = fixedSubgroupCongr (ψ.trans χ) ⋯
      source
      theorem TauCeti.fixedSubgroupCongr_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 ↑ψ) :
      (fixedSubgroupCongr ψ hψ).symm = fixedSubgroupCongr ψ.symm ⋯