Documentation

TauCeti.Algebra.AlgebraicGroup.Hopf.KernelPoints

Points of kernel quotients #

For a surjective morphism of Hopf algebras f : H →ₐc[R] K, the quotient by the Hopf-ideal kernel is bialgebra-equivalent to K. This file transports that first isomorphism theorem to functors of points: for every commutative R-algebra A, the convolution group of A-points of H ⧸ kerOfSurjective f is multiplicatively equivalent to the convolution group of A-points of K.

The characteristic compatibility says that including an A-point of H ⧸ kerOfSurjective f back into the ambient H-points is the same as first identifying it with a K-point and then pre-composing along f. This compatibility with the closed-subgroup inclusion assumes the source Hopf algebra H is commutative.

Main declarations #

References #

This is a Layer 3 prerequisite for TauCetiRoadmap/ReductiveGroups/README.md, "Hopf ideals ↔ closed subgroup schemes", specifically the kernels part of the Hopf-ideal dictionary. It uses the first isomorphism theorem TauCeti.HopfIdeal.kerLiftBialgEquiv and the contravariant points functoriality TauCeti.AlgHom.mapDomainMulEquiv.

source
noncomputable def TauCeti.HopfIdeal.quotientKerPointsMulEquiv {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) :
WithConv (H ⧸ (kerOfSurjective f hf).toIdeal →ₐ[R] ↑A) ≃* WithConv (K →ₐ[R] ↑A)

The points of the quotient by the Hopf-ideal kernel of a surjective Hopf algebra morphism are the points of its codomain.

Contravariantly, this is induced by the bialgebra equivalence H ⧸ kerOfSurjective f ≃ₐc[R] K from the Hopf-algebra first isomorphism theorem.

Equations
Instances For
    source
    theorem TauCeti.HopfIdeal.quotientKerPointsMulEquiv_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (g : WithConv (H ⧸ (kerOfSurjective f hf).toIdeal →ₐ[R] ↑A)) :
    (quotientKerPointsMulEquiv f hf A) g = (AlgHom.mapDomain ↑(kerLiftBialgEquiv f hf).symm) g

    The quotient-kernel point equivalence acts by pre-composition with the inverse bialgebra equivalence K ≃ₐc[R] H ⧸ kerOfSurjective f.

    source
    theorem TauCeti.HopfIdeal.quotientKerPointsMulEquiv_symm_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (g : WithConv (K →ₐ[R] ↑A)) :
    (quotientKerPointsMulEquiv f hf A).symm g = (AlgHom.mapDomain ↑(kerLiftBialgEquiv f hf)) g

    The inverse quotient-kernel point equivalence acts by pre-composition with the bialgebra equivalence H ⧸ kerOfSurjective f ≃ₐc[R] K.

    source
    theorem TauCeti.HopfIdeal.quotientKerPointsMulEquiv_mapValue {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] {B : Type u_1} [CommRing B] [Algebra R B] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (χ : ↑A →ₐ[R] B) (g : WithConv (H ⧸ (kerOfSurjective f hf).toIdeal →ₐ[R] ↑A)) :
    (quotientKerPointsMulEquiv f hf ↧B) ((AlgHom.mapValue χ) g) = (AlgHom.mapValue χ) ((quotientKerPointsMulEquiv f hf A) g)

    The quotient-kernel point equivalence is natural in the value algebra.

    source
    theorem TauCeti.HopfIdeal.mapValue_quotientKerPointsMulEquiv_symm_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] {B : Type u_1} [CommRing B] [Algebra R B] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (χ : ↑A →ₐ[R] B) (g : WithConv (K →ₐ[R] ↑A)) :
    (AlgHom.mapValue χ) ((quotientKerPointsMulEquiv f hf A).symm g) = (quotientKerPointsMulEquiv f hf ↧B).symm ((AlgHom.mapValue χ) g)

    The inverse quotient-kernel point equivalence is natural in the value algebra.

    source
    theorem TauCeti.HopfIdeal.quotientPointsHom_quotientKerPointsMulEquiv_symm_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [CommRing H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
    (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (kerOfSurjective f hf) A)) ((quotientKerPointsMulEquiv f hf A).symm g) = (AlgHom.mapDomain f) g

    Including the quotient point attached to a K-point back into ambient H-points is pre-composition along the original surjective Hopf algebra morphism.

    source
    theorem TauCeti.HopfIdeal.quotientPointsHom_quotientKerPointsMulEquiv_symm_apply_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [CommRing H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) (h : H) :
    ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (kerOfSurjective f hf) A)) ((quotientKerPointsMulEquiv f hf A).symm g)).ofConv h = g.ofConv (f h)

    Pointwise form of quotientPointsHom_quotientKerPointsMulEquiv_symm_apply.

    source
    theorem TauCeti.HopfIdeal.quotientPointsHom_quotientKerPointsMulEquiv_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [CommRing H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) :
    (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (kerOfSurjective f hf) A)) g = (AlgHom.mapDomain f) ((quotientKerPointsMulEquiv f hf A) g)

    For an arbitrary point of H ⧸ kerOfSurjective f, the quotient-points inclusion agrees with first identifying it as a K-point and then pre-composing along f.

    source
    theorem TauCeti.HopfIdeal.quotientPointsHom_quotientKerPointsMulEquiv_apply_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [CommRing H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) (h : H) :
    ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (↧H) (kerOfSurjective f hf) A)) g).ofConv h = ((quotientKerPointsMulEquiv f hf A) g).ofConv (f h)

    Pointwise form of quotientPointsHom_quotientKerPointsMulEquiv_apply.

    source
    theorem TauCeti.HopfIdeal.quotientPointsSubgroup_kerOfSurjective_eq_range {R : Type u} [CommRing R] {H : Type v} {K : Type w} [CommRing H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) (A : CommAlgCat R) :
    CommHopfAlgCat.quotientPointsSubgroup (↧H) (kerOfSurjective f hf) A = (AlgHom.mapDomain f).range

    The closed subgroup cut out by the kernel of a surjective Hopf-algebra morphism has, on every value algebra, exactly the points obtained by pre-composition with that morphism.

    source
    theorem TauCeti.HopfIdeal.quotientPointsSubgroup_kerOfSurjective_eq_range_mapPointsFunctor {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) (A : CommAlgCat R) :
    CommHopfAlgCat.quotientPointsSubgroup H (kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf) A = (GrpCat.Hom.hom ((CommHopfAlgCat.mapPointsFunctor f).app A)).range

    The bundled form of quotientPointsSubgroup_kerOfSurjective_eq_range: the points cut out by the kernel of a surjective morphism are the range of its point map.