Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Coinvariants.HopfBaseChange

Scalar extension of normal affine quotients #

For a normal closed subgroup N of an affine group G over a field, the algebra of coinvariants is a Hopf algebra. Its scalar extension is canonically isomorphic, as a Hopf algebra, to the coinvariants of the scalar-extended subgroup. The comparison commutes with the coordinate inclusions defining the quotient projections.

Consequently, the assertion that the quotient projection has kernel exactly N is preserved and reflected by every field extension. This allows the exact-kernel theorem for a normal quotient to be proved over an algebraic closure and then descended, without assuming smoothness, reducedness, or finite type.

The construction upgrades coinvariantsBaseChangeEquiv using the corestriction of the scalar-extended Hopf inclusion; it does not construct a second coinvariant algebra.

References #

source
noncomputable def TauCeti.CommHopfAlgCat.coinvariantsBaseChangeIso {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) :
baseChange (coinvariants hI) ≅ coinvariants ⋯

Scalar extension of the normal affine quotient, as an isomorphism of coordinate Hopf algebras. Contravariantly, this identifies (G/N)_K with the quotient by N_K.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.coinvariantsBaseChangeIso_hom_apply {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) (z : TensorProduct k K ↥I.coinvariants) :
    (CommHopfAlgCat.Hom.hom (coinvariantsBaseChangeIso hI).hom) z = (coinvariantsBaseChangeEquiv I) z

    The Hopf comparison is the canonical flat-base-change comparison of invariant algebras.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.coinvariantsBaseChangeIso_inv_apply {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) (z : ↥(baseChangeHopfIdeal I).coinvariants) :
    (CommHopfAlgCat.Hom.hom (coinvariantsBaseChangeIso hI).inv) z = (coinvariantsBaseChangeEquiv I).symm z

    The inverse Hopf comparison is the inverse comparison of invariant algebras.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.coinvariantsBaseChangeIso_hom_comp_coinvariantsι {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) :
    CategoryTheory.CategoryStruct.comp (coinvariantsBaseChangeIso hI).hom (coinvariantsι ⋯) = baseChangeMap (coinvariantsι hI)

    The quotient projection after scalar extension agrees with the projection for the scalar-extended subgroup under the canonical comparison.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.coinvariantsBaseChangeIso_hom_comp_coinvariantsι_assoc {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) {Z : CommHopfAlgCat K} (h : baseChange H ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (coinvariantsBaseChangeIso hI).hom (CategoryTheory.CategoryStruct.comp (coinvariantsι ⋯) h) = CategoryTheory.CategoryStruct.comp (baseChangeMap (coinvariantsι hI)) h

    The quotient projection after scalar extension agrees with the projection for the scalar-extended subgroup under the canonical comparison.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.coinvariantsBaseChangeIso_inv_comp_baseChangeMap {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) :
    CategoryTheory.CategoryStruct.comp (coinvariantsBaseChangeIso hI).inv (baseChangeMap (coinvariantsι hI)) = coinvariantsι ⋯

    The inverse comparison also commutes with the quotient coordinate inclusion.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.coinvariantsBaseChangeIso_inv_comp_baseChangeMap_assoc {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) {Z : CommHopfAlgCat K} (h : baseChange H ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (coinvariantsBaseChangeIso hI).inv (CategoryTheory.CategoryStruct.comp (baseChangeMap (coinvariantsι hI)) h) = CategoryTheory.CategoryStruct.comp (coinvariantsι ⋯) h

    The inverse comparison also commutes with the quotient coordinate inclusion.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_baseChangeMap_coinvariantsι {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) :
    kernelHopfIdeal (baseChangeMap (coinvariantsι hI)) = kernelHopfIdeal (coinvariantsι ⋯)

    The scheme-theoretic kernel of the normal quotient projection commutes with every field extension. This equality retains the full Hopf ideal, including infinitesimal structure.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_coinvariantsι_baseChange_eq_iff {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) :
    kernelHopfIdeal (coinvariantsι ⋯) = baseChangeHopfIdeal I ↔ kernelHopfIdeal (coinvariantsι hI) = I

    Exactness of the kernel of a normal quotient can be checked after any field extension. In particular, an exact-kernel theorem over an algebraic closure descends to the base field.