Documentation

TauCeti.GroupTheory.DerivedCentralQuotient

The derived subgroup modulo its centre #

Let G be a group. This file studies the group

[G, G] / Z([G, G]),

the derived subgroup of G modulo the centre of that derived subgroup.

The construction is the last step of the standard recipe producing a finite group of Lie type: one takes the fixed points H of a Steinberg endomorphism of a pinned algebraic group, passes to [H, H], and quotients by the centre of [H, H]. Taking the derived subgroup handles the parameters at which H fails to be perfect, and the central quotient is what turns a quasisimple group into a simple one. Everything in this file is carrier-independent: it needs only a group, so it is available before any particular ambient group has been constructed.

Nothing here proves that the resulting group is finite or simple. What is proved is that the recipe does nothing once it has succeeded: on a perfect group with trivial centre — in particular on any nonabelian simple group — it returns the group itself, and by Grün's lemma its output is centreless as soon as [G, G] is perfect, so a second application changes nothing.

Transport says that isomorphic groups have isomorphic derived central quotients, so the output depends only on the isomorphism class of G.

Main definitions #

Main results #

References #

This is the derived-subgroup-modulo-centre half of milestone L3 of TauCetiRoadmap/CFSGStatement/README.md, which fixes the recipe H = fixedSubgroup F and Group = [H, H] / Z([H, H]) and the reading of the centre as the centre of the derived subgroup rather than of H. 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
theorem TauCeti.IsSimpleGroup.center_eq_bot_of_not_isMulCommutative {G : Type u_1} [Group G] [IsSimpleGroup G] (h : ¬IsMulCommutative G) :
Subgroup.center G = ⊥

A nonabelian simple group has trivial centre.

source
theorem TauCeti.IsSimpleGroup.isPerfect_of_not_isMulCommutative {G : Type u_1} [Group G] [IsSimpleGroup G] (h : ¬IsMulCommutative G) :
Group.IsPerfect G

A nonabelian simple group is perfect.

The derived subgroup modulo its centre #

source
@[reducible, inline]
abbrev TauCeti.DerivedCentralQuotient (G : Type u_1) [Group G] :
Type u_1

The derived subgroup of G modulo the centre of that derived subgroup, [G, G] / Z([G, G]).

This is the group-theoretic step turning the fixed points of a Steinberg endomorphism into a candidate simple group. No finiteness or simplicity is asserted: the construction is available for every group, and returns the trivial group whenever [G, G] is commutative.

Equations
Instances For
    source
    theorem TauCeti.DerivedCentralQuotient.subsingleton_iff {G : Type u_1} [Group G] :
    Subsingleton (DerivedCentralQuotient G) ↔ IsMulCommutative ↥(commutator G)

    The derived central quotient is trivial exactly when the derived subgroup is commutative. In particular it is trivial for every commutative G, whose derived subgroup is itself trivial.

    source
    instance TauCeti.DerivedCentralQuotient.instSubsingletonOfIsMulCommutativeSubtypeMemSubgroupCommutator {G : Type u_1} [Group G] [IsMulCommutative ↥(commutator G)] :
    Subsingleton (DerivedCentralQuotient G)
    source
    theorem TauCeti.DerivedCentralQuotient.card_dvd_card {G : Type u_1} [Group G] :
    Nat.card (DerivedCentralQuotient G) ∣ Nat.card G

    The order of the derived central quotient divides the order of the group.

    The universal property #

    source
    def TauCeti.DerivedCentralQuotient.lift {G : Type u_1} [Group G] {K : Type u_2} [Group K] (f : ↥(commutator G) →* K) (hf : Function.Surjective ⇑f) (hK : Subgroup.center K = ⊥) :
    DerivedCentralQuotient G →* K

    A surjection from [G, G] onto a group with trivial centre factors through the derived central quotient.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.DerivedCentralQuotient.lift_mk {G : Type u_1} [Group G] {K : Type u_2} [Group K] (f : ↥(commutator G) →* K) (hf : Function.Surjective ⇑f) (hK : Subgroup.center K = ⊥) (x : ↥(commutator G)) :
      (lift f hf hK) ↑x = f x
      source
      theorem TauCeti.DerivedCentralQuotient.lift_unique {G : Type u_1} [Group G] {K : Type u_2} [Group K] (f : ↥(commutator G) →* K) (hf : Function.Surjective ⇑f) (hK : Subgroup.center K = ⊥) (g : DerivedCentralQuotient G →* K) (hg : ∀ (x : ↥(commutator G)), g ↑x = f x) :
      g = lift f hf hK

      The factorisation through the derived central quotient is unique.

      source
      theorem TauCeti.DerivedCentralQuotient.lift_surjective {G : Type u_1} [Group G] {K : Type u_2} [Group K] (f : ↥(commutator G) →* K) (hf : Function.Surjective ⇑f) (hK : Subgroup.center K = ⊥) :
      Function.Surjective ⇑(lift f hf hK)

      The factorisation of a surjection through the derived central quotient is again surjective, so the quotient sits between [G, G] and the centreless group it was mapped onto.

      The recipe on groups it has already succeeded on #

      source
      def TauCeti.DerivedCentralQuotient.mulEquivOfCenterEqBot {G : Type u_1} [Group G] [Group.IsPerfect G] (h : Subgroup.center G = ⊥) :
      DerivedCentralQuotient G ≃* G

      A perfect group with trivial centre is its own derived central quotient.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.DerivedCentralQuotient.mulEquivOfCenterEqBot_mk {G : Type u_1} [Group G] [Group.IsPerfect G] (h : Subgroup.center G = ⊥) (x : ↥(commutator G)) :
        (mulEquivOfCenterEqBot h) ↑x = ↑x
        source
        def TauCeti.DerivedCentralQuotient.mulEquivOfIsSimpleGroup {G : Type u_1} [Group G] [IsSimpleGroup G] (h : ¬IsMulCommutative G) :
        DerivedCentralQuotient G ≃* G

        The recipe returns a nonabelian simple group unchanged.

        So the construction is the identity on every nonabelian entry of the classification list. The abelian cyclic entries instead collapse to the trivial group by subsingleton_iff.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.DerivedCentralQuotient.mulEquivOfIsSimpleGroup_mk {G : Type u_1} [Group G] [IsSimpleGroup G] (h : ¬IsMulCommutative G) (x : ↥(commutator G)) :
          (mulEquivOfIsSimpleGroup h) ↑x = ↑x
          source
          theorem TauCeti.DerivedCentralQuotient.center_eq_bot {G : Type u_1} [Group G] [Group.IsPerfect ↥(commutator G)] :
          Subgroup.center (DerivedCentralQuotient G) = ⊥

          Grün's lemma for the recipe: when the derived subgroup is perfect, the derived central quotient has trivial centre.

          This is the reason the two steps compose in the stated order: the centre is removed once and for all, and does not reappear.

          source
          def TauCeti.DerivedCentralQuotient.mulEquivSelf {G : Type u_1} [Group G] [Group.IsPerfect ↥(commutator G)] :
          DerivedCentralQuotient (DerivedCentralQuotient G) ≃* DerivedCentralQuotient G

          The construction is idempotent on a group with perfect derived subgroup.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.DerivedCentralQuotient.mulEquivSelf_mk {G : Type u_1} [Group G] [Group.IsPerfect ↥(commutator G)] (x : ↥(commutator (DerivedCentralQuotient G))) :
            mulEquivSelf ↑x = ↑x

            Transport along an isomorphism #

            source
            def TauCeti.DerivedCentralQuotient.congr {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (ψ : G ≃* G') :
            DerivedCentralQuotient G ≃* DerivedCentralQuotient G'

            The derived central quotient transported along an isomorphism of groups.

            Both steps of the recipe are transported: the isomorphism restricts to the derived subgroups, and that restriction carries the centre of the one onto the centre of the other. So the recipe depends only on the isomorphism class of G.

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