Documentation

TauCeti.Algebra.AlgebraicGroup.Derived.Functoriality

Functoriality of the derived subgroup #

A homomorphism of affine group schemes carries commutators to commutators, and therefore restricts to a homomorphism of their derived closed subgroup schemes. In coordinate Hopf algebras, a morphism f : H ⟶ K sends the ideal defining the derived subgroup of Spec H into the ideal defining the derived subgroup of Spec K. It consequently induces a morphism

H / derivedDefiningIdeal H ⟶ K / derivedDefiningIdeal K.

Using the naturality of the commutator coordinate morphism, this file constructs the induced quotient morphism and packages its identity and composition laws as an endofunctor on commutative Hopf algebras. Applying Spec reverses this map to the expected restriction between derived subgroup schemes.

Main declarations #

References #

This supplies the functoriality part of the derived-group target G_der in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

source
theorem TauCeti.CommHopfAlgCat.derivedDefiningIdeal_map_le {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [CommSemiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) :
(derivedDefiningIdeal H).map f ≤ derivedDefiningIdeal K

A morphism of commutative Hopf algebras sends the derived defining ideal into the derived defining ideal of its target. Contravariantly, a group-scheme homomorphism sends the source derived subgroup into the target derived subgroup.

source
@[simp]
theorem TauCeti.CommHopfAlgCat.comapOfSurjective_derivedDefiningIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (e : H ≅ K) :
(derivedDefiningIdeal ↑K).comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯ = derivedDefiningIdeal ↑H

An isomorphism of commutative Hopf algebras preserves the derived defining ideal.

source
noncomputable def TauCeti.CommHopfAlgCat.derivedMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
quotient H (derivedDefiningIdeal ↑H) ⟶ quotient K (derivedDefiningIdeal ↑K)

The coordinate morphism induced by a homomorphism on the coordinate algebras of the derived subgroups. After applying Spec, this is the restriction of the original group-scheme homomorphism to the derived subgroup schemes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.derivedMap_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (x : ↑H) :
    (CommHopfAlgCat.Hom.hom (derivedMap f)) ((Ideal.Quotient.mk (derivedDefiningIdeal ↑H).toIdeal) x) = (Ideal.Quotient.mkₐ R (derivedDefiningIdeal ↑K).toIdeal) ((CommHopfAlgCat.Hom.hom f) x)

    On quotient classes, the induced derived-coordinate map applies the ambient morphism before taking the target quotient class.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_derivedMap {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    CategoryTheory.CategoryStruct.comp (mkQuotient H (derivedDefiningIdeal ↑H)) (derivedMap f) = CategoryTheory.CategoryStruct.comp f (mkQuotient K (derivedDefiningIdeal ↑K))

    The induced map on derived coordinate algebras commutes with the ambient quotient maps. This is the coordinate square expressing that the derived-subgroup map restricts the original map.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.derivedMap_id {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
    derivedMap (CategoryTheory.CategoryStruct.id H) = CategoryTheory.CategoryStruct.id (quotient H (derivedDefiningIdeal ↑H))

    The map induced on derived coordinate algebras by the identity is the identity.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.derivedMap_comp {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) :
    derivedMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (derivedMap f) (derivedMap g)

    Maps induced on derived coordinate algebras respect composition.

    source
    noncomputable def TauCeti.CommHopfAlgCat.derivedFunctor {R : Type u} [CommRing R] :
    CategoryTheory.Functor (CommHopfAlgCat R) (CommHopfAlgCat R)

    Taking the coordinate algebra of the derived subgroup is an endofunctor on commutative Hopf algebras. On affine group schemes, composition with the contravariant spectrum functor gives the covariant derived-subgroup construction.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.derivedFunctor_obj {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
      derivedFunctor.obj H = quotient H (derivedDefiningIdeal ↑H)

      The derived-coordinate functor acts on objects by quotienting by the derived defining ideal.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.derivedFunctor_map {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
      derivedFunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (derivedMap f) (CategoryTheory.eqToHom ⋯))

      The derived-coordinate functor acts on morphisms by the induced quotient morphism.

      source
      noncomputable def TauCeti.CommHopfAlgCat.derivedQuotientNatTrans {R : Type u} [CommRing R] :
      CategoryTheory.Functor.id (CommHopfAlgCat R) ⟶ derivedFunctor

      The quotient morphisms from an ambient coordinate Hopf algebra to its derived-subgroup coordinate algebra form a natural transformation. After applying the contravariant spectrum functor, this is the natural closed immersion of the derived subgroup into the ambient group.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.CommHopfAlgCat.derivedQuotientNatTrans_app {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
        derivedQuotientNatTrans.app H = CategoryTheory.CategoryStruct.comp (mkQuotient H (derivedDefiningIdeal ↑H)) (CategoryTheory.eqToHom ⋯)

        The component of the derived quotient natural transformation is the coordinate quotient morphism defining the derived closed subgroup.