Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Kernel.Basic

The kernel Hopf ideal of a morphism of commutative Hopf algebras #

For a morphism f : H ⟶ K of commutative Hopf algebras, the kernel Hopf ideal is the extension of the augmentation ideal of H along f — the ideal K·f(H⁺) of the codomain, which is the coordinate ring of the source of the induced morphism of affine group schemes. Quotienting by it cuts out the kernel closed subgroup scheme (TauCeti.CommHopfAlgCat.kernelSpec, in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Scheme.Kernel).

The kernel semantics live at this coordinate level: the trivialization criterion says a map out of K kills the kernel Hopf ideal exactly when its composite with f is the trivial (counit-unit) morphism, for an arbitrary ring-valued algebra target, for Hopf-algebra morphisms, and for Hopf-ideal quotients; the coordinate-ring triangle is the mkQuotient special case. The coordinate-level factorization and its uniqueness are TauCeti.CommHopfAlgCat.liftQuotient and TauCeti.CommHopfAlgCat.liftQuotient_unique.

Main declarations #

References #

Milne, Algebraic Groups, Proposition 4.1: the kernel of a homomorphism of affine algebraic groups is represented by the quotient by this ideal.

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

The kernel Hopf ideal of a morphism of commutative Hopf algebras: the image of the augmentation ideal of the source. It is an ideal of the codomain K, the coordinate ring of the source of the induced group-scheme morphism Spec K ⟶ Spec H; its quotient represents the kernel of that morphism.

Equations
Instances For
    source
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_def {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    kernelHopfIdeal f = (HopfIdeal.augmentation R ↑H).map (CommHopfAlgCat.Hom.hom f)

    kernelHopfIdeal is the extension of the augmentation ideal along the morphism.

    source
    theorem TauCeti.CommHopfAlgCat.isNormal_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    (kernelHopfIdeal f).IsNormal

    The scheme-theoretic kernel of a morphism of affine groups is normal.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_toIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    (kernelHopfIdeal f).toIdeal = Ideal.map (↑(CommHopfAlgCat.Hom.hom f)) (HopfIdeal.augmentation R ↑H).toIdeal

    The underlying ideal of the kernel Hopf ideal is the extension of the augmentation ideal.

    source
    theorem TauCeti.CommHopfAlgCat.mem_kernelHopfIdeal_of_mem_augmentation {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {x : ↑H} (hx : CoalgebraStruct.counit x = 0) :
    (CommHopfAlgCat.Hom.hom f) x ∈ kernelHopfIdeal f

    The kernel Hopf ideal contains the image of every counit-vanishing element.

    source
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_eq_augmentation_of_surjective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) :
    kernelHopfIdeal f = HopfIdeal.augmentation R ↑K

    The kernel Hopf ideal of a surjective coordinate morphism is the augmentation ideal. This applies in particular to isomorphisms and identifies their group-scheme kernel with the trivial subgroup.

    source
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_comp {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {L : CommHopfAlgCat R} (g : K ⟶ L) :
    kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g) = (kernelHopfIdeal f).map (CommHopfAlgCat.Hom.hom g)

    The kernel Hopf ideal of a composite is the extension of the first morphism's kernel Hopf ideal along the second morphism.

    source
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_comp_le {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {L : CommHopfAlgCat R} (g : K ⟶ L) :
    kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g) ≤ kernelHopfIdeal g

    The kernel of Spec L → Spec K is contained in the kernel of Spec L → Spec H. Hopf ideals reverse the inclusion of closed subgroups.

    source
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_comp_of_surjective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {L : CommHopfAlgCat R} (g : K ⟶ L) :
    kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g) = kernelHopfIdeal g

    Precomposing a coordinate morphism with a surjective morphism does not change its kernel closed subgroup scheme.

    source
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_toIdeal_le_ker_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {A : Type w} [Ring A] [Algebra R A] (φ : ↑K →ₐ[R] A) :
    (kernelHopfIdeal f).toIdeal ≤ RingHom.ker φ.toRingHom ↔ φ.comp ↑(CommHopfAlgCat.Hom.hom f) = (Algebra.ofId R A).comp (Bialgebra.counitAlgHom R ↑H)

    Algebra-level trivialization criterion: an algebra map out of the coordinate ring of the source group scheme kills the kernel Hopf ideal exactly when its composite with f is the counit-unit composite. This is the kernel property tested against an arbitrary commutative R-algebra; TauCeti.CommHopfAlgCat.mapPointsFunctor_app_eq_one_iff (in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Points.Kernel) packages it on the functors of points.

    source
    theorem TauCeti.CommHopfAlgCat.comp_eq_unit_comp_counit_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {L : CommHopfAlgCat R} (g : K ⟶ L) :
    CategoryTheory.CategoryStruct.comp f g = CommHopfAlgCat.ofHom ((Bialgebra.unitBialgHom R ↑L).comp (Bialgebra.counitBialgHom R ↑H)) ↔ (kernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom g)).toRingHom

    The trivialization criterion for Hopf-algebra morphisms: a morphism out of K kills the kernel Hopf ideal of f exactly when its composite with f is the trivial (counit-unit) morphism.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.comp_mkQuotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    CategoryTheory.CategoryStruct.comp f (mkQuotient K (kernelHopfIdeal f)) = CommHopfAlgCat.ofHom ((Bialgebra.unitBialgHom R ↑(quotient K (kernelHopfIdeal f))).comp (Bialgebra.counitBialgHom R ↑H))

    The coordinate-ring triangle: composing f with the quotient by its kernel Hopf ideal is the counit-unit composite, i.e. the coordinate map of the trivial group-scheme morphism.

    source
    theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_le_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) {J : HopfIdeal R ↑K} :
    kernelHopfIdeal f ≤ J ↔ CategoryTheory.CategoryStruct.comp f (mkQuotient K J) = CommHopfAlgCat.ofHom ((Bialgebra.unitBialgHom R ↑(quotient K J)).comp (Bialgebra.counitBialgHom R ↑H))

    The Hopf-ideal-quotient form of the trivialization criterion: f trivializes on the closed subgroup scheme cut out by J exactly when J contains the kernel Hopf ideal. Combined with TauCeti.CommHopfAlgCat.quotientSpecMapOfLe and TauCeti.CommHopfAlgCat.quotientSpecMapOfLe_comp_quotientSpecι, such a quotient closed subgroup scheme includes into the kernel compatibly with the inclusions.