Documentation

TauCeti.AlgebraicGeometry.AffineGroupScheme.Semisimple.Basic

Semisimple affine group schemes #

This file transports semisimplicity from finite-type commutative Hopf algebras to affine group schemes of finite type over a field. The coordinate-ring predicate says that the group is smooth and geometrically connected and that every connected normal smooth solvable closed subgroup of its geometric fibre is trivial. The resulting full subcategory is anti-equivalent to semisimple finite-type commutative Hopf algebras.

The formulation uses the universal property of a trivial geometric radical. It does not assume that a maximal solvable normal subgroup has already been constructed. Its triviality requirement ranges over connected normal smooth solvable subgroup schemes; nonsmooth subgroup schemes are not constrained, while the ambient finite-type affine-group-scheme category still includes nonsmooth objects. Bundled semisimple objects carry smooth and geometrically connected structural-morphism instances.

Main declarations #

References #

The formal organization follows TauCeti.AlgebraicGeometry.AffineGroupScheme.Unipotent. This advances Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap by keeping the coordinate-Hopf and affine-group-scheme models synchronized. Construction of the geometric radical and identification of this predicate with its triviality remain downstream.

source
def TauCeti.semisimpleAffineGroupSchemeProperty (k : Type u) [Field k] :
CategoryTheory.ObjectProperty (FiniteTypeAffineGroupSchemeCat ↧k)

The object property selecting semisimple affine group schemes of finite type over a field.

The property is transported through the finite-type affine Hopf/group-scheme anti-equivalence. Thus its normal-subgroup condition is the coordinate-Hopf universal property used by semisimpleCommHopfAlgProperty, presented on the scheme side.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.semisimpleAffineGroupSchemeProperty_iff (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) :
    semisimpleAffineGroupSchemeProperty k G ↔ semisimpleCommHopfAlgProperty k (Opposite.unop ((finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).inverse.obj G))

    A finite-type affine group scheme is semisimple exactly when its coordinate Hopf algebra satisfies semisimpleCommHopfAlgProperty.

    source
    instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeAffineGroupSchemeCatOfSemisimpleAffineGroupSchemeProperty (k : Type u) [Field k] :
    (semisimpleAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

    Semisimplicity of finite-type affine group schemes is invariant under isomorphism.

    source
    @[reducible, inline]
    abbrev TauCeti.SemisimpleAffineGroupSchemeCat (k : Type u) [Field k] :
    Type (u + 1)

    The category of semisimple affine group schemes of finite type over a field.

    Equations
    Instances For
      source
      theorem TauCeti.smooth_of_semisimpleAffineGroupSchemeProperty (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hG : semisimpleAffineGroupSchemeProperty k G) :
      AlgebraicGeometry.Smooth G.obj.obj.X.hom

      A finite-type affine group scheme satisfying the semisimplicity property has smooth structural morphism.

      source
      instance TauCeti.instSmoothHomSchemeXOverSpecOfObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteTypeAffineGroupSchemePropertyFiniteTypeAffineGroupSchemeCatSemisimpleAffineGroupSchemeProperty (k : Type u) [Field k] (G : SemisimpleAffineGroupSchemeCat k) :
      AlgebraicGeometry.Smooth G.obj.obj.obj.X.hom

      Objects of SemisimpleAffineGroupSchemeCat k have smooth structural morphism.

      source
      theorem TauCeti.geometricallyConnected_of_semisimpleAffineGroupSchemeProperty (k : Type u) [Field k] (G : FiniteTypeAffineGroupSchemeCat ↧k) (hG : semisimpleAffineGroupSchemeProperty k G) :
      AlgebraicGeometry.GeometricallyConnected G.obj.obj.X.hom

      A finite-type affine group scheme satisfying the semisimplicity property has geometrically connected structural morphism.

      source
      instance TauCeti.instGeometricallyConnectedHomSchemeXOverSpecOfObjGrpAffineGroupSchemePropertyAffineGroupSchemeCatFiniteTypeAffineGroupSchemePropertyFiniteTypeAffineGroupSchemeCatSemisimpleAffineGroupSchemeProperty (k : Type u) [Field k] (G : SemisimpleAffineGroupSchemeCat k) :
      AlgebraicGeometry.GeometricallyConnected G.obj.obj.obj.X.hom

      Objects of SemisimpleAffineGroupSchemeCat k have geometrically connected structural morphism.

      source
      theorem TauCeti.semisimpleAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] :
      (semisimpleAffineGroupSchemeProperty k).inverseImage (finiteTypeCommHopfAlgCatOpEquivFiniteTypeAffineGroupSchemeCat k).functor = (semisimpleCommHopfAlgProperty k).op

      Under the finite-type affine Hopf/group-scheme anti-equivalence, the inverse image of semisimplicity on group schemes is semisimplicity of coordinate Hopf algebras.

      source
      noncomputable def TauCeti.semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat (k : Type u) [Field k] :
      (SemisimpleCommHopfAlgCat k)ᵒᵖ ≌ SemisimpleAffineGroupSchemeCat k

      Spec restricts to an anti-equivalence from semisimple finite-type commutative Hopf algebras to semisimple affine group schemes.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def TauCeti.semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat.functorCompιIso (k : Type u) [Field k] :
        (semisimpleCommHopfAlgCatOpEquivSemisimpleAffineGroupSchemeCat k).functor.comp ((semisimpleAffineGroupSchemeProperty k).ι.comp ((finiteTypeAffineGroupSchemeProperty ↧k).ι.comp (affineGroupSchemeProperty ↧k).ι)) ≅ (CategoryTheory.forget₂ (SemisimpleCommHopfAlgCat k) (FiniteTypeCommHopfAlgCat k)).op.comp ((CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat k) (CommHopfAlgCat k)).op.comp (AlgebraicGeometry.hopfSpec ↧k))

        The forward semisimple anti-equivalence, followed by the inclusions into finite-type affine group schemes and affine group schemes, is Mathlib's hopfSpec after forgetting semisimplicity and finite type. This is the computation interface for the restricted equivalence.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For