Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Coinvariants.Components

Finite étale quotients by subgroups containing the identity component #

Over an algebraically closed field, the coinvariants of a closed subgroup containing the identity component form a finite étale algebra. For normal subgroups this is the coordinate algebra of the represented quotient. Neither the ambient group nor the subgroup needs to be reduced, and finiteness of the invariant algebra does not require normality.

The identity-component coinvariants are the functions on the finite component group. For a normal subgroup containing the identity component, the quotient is therefore a finite étale quotient of the component group.

References #

source
@[simp]
theorem TauCeti.FiniteTypeCommHopfAlgCat.coinvariants_identityComponentHopfIdeal_eq_range {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
HopfAlgebra.identityComponentHopfIdeal.coinvariants = H.componentCoordinateMap.range

The functions invariant under the identity component are exactly the pullbacks of functions on the finite component group, including for nonreduced affine groups.

source
noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentCoinvariantsIso {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
↧(ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj))) ≅ CommHopfAlgCat.coinvariants ⋯

The constant component coordinate algebra is canonically isomorphic to the identity-component coinvariants, including for nonreduced affine groups.

Instances For
    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoinvariantsIso_hom_comp {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
    CategoryTheory.CategoryStruct.comp H.componentCoinvariantsIso.hom (CommHopfAlgCat.coinvariantsι ⋯) = H.componentCoordinateHom

    The comparison with coinvariants recovers the component coordinate morphism after composition with the coinvariant inclusion.

    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoinvariantsIso_hom_comp_assoc {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) {Z : CommHopfAlgCat k} (h : H.obj ⟶ Z) :
    CategoryTheory.CategoryStruct.comp H.componentCoinvariantsIso.hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.coinvariantsι ⋯) h) = CategoryTheory.CategoryStruct.comp H.componentCoordinateHom h

    The comparison with coinvariants recovers the component coordinate morphism after composition with the coinvariant inclusion.

    source
    theorem TauCeti.FiniteTypeCommHopfAlgCat.moduleFinite_coinvariants_of_le_identityComponentHopfIdeal {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) (hI : I ≤ HopfAlgebra.identityComponentHopfIdeal) :
    Module.Finite k ↥I.coinvariants

    The invariant functions of a subgroup containing the identity component are finite-dimensional. Normality and reducedness are not required.

    source
    theorem TauCeti.FiniteTypeCommHopfAlgCat.algebraEtale_coinvariants_of_le_identityComponentHopfIdeal {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (I : HopfIdeal k ↑H.obj) (hI : I ≤ HopfAlgebra.identityComponentHopfIdeal) :
    Algebra.Etale k ↥I.coinvariants

    The invariant algebra of a subgroup containing the identity component is étale, even when the ambient group or the subgroup is nonreduced.