Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Scheme.Kernel

The kernel of a morphism of affine group schemes #

A morphism f : H ⟶ K of commutative Hopf algebras induces contravariantly a morphism of affine group schemes Spec K ⟶ Spec H over Spec R. This file packages its kernel: the closed subgroup scheme of Spec K cut out by the kernel Hopf ideal (TauCeti.CommHopfAlgCat.kernelHopfIdeal, the extension K·f(H⁺) of the augmentation ideal, whose kernel semantics — the trivialization criterion — live in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Kernel). The inclusion is a closed immersion by TauCeti.CommHopfAlgCat.isClosedImmersion_quotientSpecι, and the scheme-level triangle here is the image of the coordinate-ring triangle under hopfSpec. The quotient--tensor identification presents this kernel as the scheme-theoretic fibre over the identity section, and the resulting pullback square lifts from schemes to group objects. The points-level kernel property is TauCeti.CommHopfAlgCat.mapPointsFunctor_app_eq_one_iff in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Points.Kernel.

Main declarations #

References #

Milne, Algebraic Groups, Proposition 4.1. The same-universe restriction on the Hopf algebras is imposed by Mathlib's current hopfSpec construction, as in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Scheme.Basic.

source
@[reducible, inline]
noncomputable abbrev TauCeti.CommHopfAlgCat.kernelSpec {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The kernel of the induced morphism of affine group schemes, as an affine group scheme: the closed subgroup scheme of the source cut out by the kernel Hopf ideal.

Equations
Instances For
    source
    noncomputable def TauCeti.CommHopfAlgCat.kernelSpecι {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    kernelSpec f ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op K)

    The inclusion of the kernel into the source group scheme. Its underlying scheme morphism is a closed immersion by TauCeti.CommHopfAlgCat.isClosedImmersion_quotientSpecι.

    Equations
    Instances For
      source
      theorem TauCeti.CommHopfAlgCat.kernelSpecι_def {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
      kernelSpecι f = quotientSpecι K (kernelHopfIdeal f)

      kernelSpecι is the quotient inclusion at the kernel Hopf ideal.

      source
      theorem TauCeti.CommHopfAlgCat.kernelSpecι_comp {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
      CategoryTheory.CategoryStruct.comp (kernelSpecι f) ((AlgebraicGeometry.hopfSpec ↧R).map f.op) = (AlgebraicGeometry.hopfSpec ↧R).map (CommHopfAlgCat.ofHom ((Bialgebra.unitBialgHom R ↑(quotient K (kernelHopfIdeal f))).comp (Bialgebra.counitBialgHom R ↑H))).op

      The scheme-level triangle: the composite of the kernel inclusion with the induced group-scheme morphism is the trivial morphism, the image under hopfSpec of the counit-unit composite. Not a simp lemma: Mathlib's simp set unfolds hopfSpec.map itself, so this left-hand side is not in simp-normal form.

      source
      theorem TauCeti.CommHopfAlgCat.isPullback_kernelSpec {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
      CategoryTheory.IsPullback (kernelSpecι f) 0 ((AlgebraicGeometry.hopfSpec ↧R).map f.op) 0

      The Hopf spectrum of the kernel quotient is the scheme-theoretic fibre over the identity. The horizontal maps are the kernel inclusion and the identity section; the vertical maps are the unique map to the trivial group scheme and the morphism induced by f, respectively.