The pointwise quotient presheaf of an affine group

A normal Hopf ideal I in a commutative Hopf algebra H cuts out a normal closed subgroup V(I)(A) ≤ G(A) over every commutative value algebra A. This file forms the pointwise quotient

G(A) / V(I)(A)

and packages it as a group-valued functor on commutative algebras. The quotient projections are natural in A. At every value algebra the resulting group satisfies the quotient universal property: a homomorphism out of G(A) descends uniquely when it kills V(I)(A).

This is the presheaf quotient that precedes fppf sheafification in Layer 3 of the reductive-groups roadmap. It is not asserted to be an fppf sheaf or representable; those are separate downstream steps with additional hypotheses.

Main declarations

• TauCeti.CommHopfAlgCat.pointwiseQuotientGroup: the group G(A) / V(I)(A).
• TauCeti.CommHopfAlgCat.pointwiseQuotientFunctor: the pointwise quotient presheaf.
• TauCeti.CommHopfAlgCat.pointwiseQuotientProjection: the natural quotient projection.
• TauCeti.CommHopfAlgCat.pointwiseQuotientLift: the quotient universal property at each value algebra, with its factorization and uniqueness properties.

References

See J. S. Milne, Algebraic Groups (2017), Section 5, for quotient sheaves. The group quotient and its universal property use Mathlib's QuotientGroup.map and QuotientGroup.lift.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.pointwiseQuotientGroup {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) : GrpCat

The pointwise quotient G(A) / V(I)(A) associated to a normal Hopf ideal I.

The denominator is the subgroup of A-points which vanish on I. Normality follows from the coordinate conjugation criterion HopfIdeal.IsNormal.

Equations

• TauCeti.CommHopfAlgCat.pointwiseQuotientGroup H I hI A = ↧(↑(TauCeti.HopfAlgebra.points A) ⧸ TauCeti.CommHopfAlgCat.quotientPointsSubgroup H I A)

noncomputable def TauCeti.CommHopfAlgCat.pointwiseQuotientMk {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) : HopfAlgebra.points A ⟶ pointwiseQuotientGroup H I hI A

The quotient projection from ambient points to the pointwise quotient.

Equations

• TauCeti.CommHopfAlgCat.pointwiseQuotientMk H I hI A = GrpCat.ofHom (QuotientGroup.mk' (TauCeti.CommHopfAlgCat.quotientPointsSubgroup H I A))

@[simp]

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientMk_apply {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : have x := ⋯; (CategoryTheory.ConcreteCategory.hom (pointwiseQuotientMk H I hI A)) g = (QuotientGroup.mk' (quotientPointsSubgroup H I A)) g

The pointwise quotient projection sends a point to its ordinary quotient class.

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientMk_ker {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) : have x := ⋯; (GrpCat.Hom.hom (pointwiseQuotientMk H I hI A)).ker = quotientPointsSubgroup H I A

The kernel of the pointwise quotient projection is exactly the subgroup cut out by I.

@[simp]

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientMk_eq_one_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) (g : ↑(HopfAlgebra.points A)) : have x := ⋯; (CategoryTheory.ConcreteCategory.hom (pointwiseQuotientMk H I hI A)) g = 1 ↔ g ∈ quotientPointsSubgroup H I A

An ambient point maps to the identity exactly when it belongs to the subgroup cut out by I.

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientMk_surjective {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (pointwiseQuotientMk H I hI A))

The pointwise quotient projection is surjective.

noncomputable def TauCeti.CommHopfAlgCat.mapPointwiseQuotient {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) {A B : CommAlgCat R} (χ : A ⟶ B) : pointwiseQuotientGroup H I hI A ⟶ pointwiseQuotientGroup H I hI B

The map on pointwise quotients induced by a morphism of value algebras.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CommHopfAlgCat.mapPointwiseQuotient_mk {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) {A B : CommAlgCat R} (χ : A ⟶ B) (g : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (mapPointwiseQuotient H I hI χ)) ((CategoryTheory.ConcreteCategory.hom (pointwiseQuotientMk H I hI A)) g) = (CategoryTheory.ConcreteCategory.hom (pointwiseQuotientMk H I hI B)) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints χ)) g)

Mapping a quotient class is represented by mapping any ambient representative.

noncomputable def TauCeti.CommHopfAlgCat.pointwiseQuotientFunctor {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : CategoryTheory.Functor (CommAlgCat R) GrpCat

The pointwise quotient presheaf A ↦ G(A) / V(I)(A).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientFunctor_obj {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) : (pointwiseQuotientFunctor H I hI).obj A = pointwiseQuotientGroup H I hI A

The object part of the pointwise quotient functor is the quotient group of ambient points by the subgroup cut out by I.

@[simp]

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientFunctor_map {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) {A B : CommAlgCat R} (χ : A ⟶ B) : (pointwiseQuotientFunctor H I hI).map χ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (mapPointwiseQuotient H I hI χ) (CategoryTheory.eqToHom ⋯))

The map part of the pointwise quotient functor is the map induced on quotient groups.

noncomputable def TauCeti.CommHopfAlgCat.pointwiseQuotientProjection {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) : HopfAlgebra.pointsFunctor ⟶ pointwiseQuotientFunctor H I hI

The natural projection from the ambient functor of points to its pointwise quotient.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientProjection_app {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) : (pointwiseQuotientProjection H I hI).app A = CategoryTheory.CategoryStruct.comp (pointwiseQuotientMk H I hI A) (CategoryTheory.eqToHom ⋯)

Each component of the natural quotient projection is the ordinary quotient-group map.

noncomputable def TauCeti.CommHopfAlgCat.pointwiseQuotientLift {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) (K : GrpCat) (f : HopfAlgebra.points A ⟶ K) (hf : quotientPointsSubgroup H I A ≤ (GrpCat.Hom.hom f).ker) : pointwiseQuotientGroup H I hI A ⟶ K

A homomorphism from ambient points which kills the normal subgroup descends to the pointwise quotient group.

Equations

• TauCeti.CommHopfAlgCat.pointwiseQuotientLift H I hI A K f hf = GrpCat.ofHom (QuotientGroup.lift (TauCeti.CommHopfAlgCat.quotientPointsSubgroup H I A) (GrpCat.Hom.hom f) hf)

@[simp]

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientLift_mk {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) (K : GrpCat) (f : HopfAlgebra.points A ⟶ K) (hf : quotientPointsSubgroup H I A ≤ (GrpCat.Hom.hom f).ker) (g : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (pointwiseQuotientLift H I hI A K f hf)) ((CategoryTheory.ConcreteCategory.hom (pointwiseQuotientMk H I hI A)) g) = (CategoryTheory.ConcreteCategory.hom f) g

The lift from a pointwise quotient agrees with the original homomorphism on every ambient representative.

theorem TauCeti.CommHopfAlgCat.pointwiseQuotientLift_unique {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (I : HopfIdeal R ↑H) (hI : I.IsNormal) (A : CommAlgCat R) (K : GrpCat) (f : HopfAlgebra.points A ⟶ K) (hf : quotientPointsSubgroup H I A ≤ (GrpCat.Hom.hom f).ker) (g : pointwiseQuotientGroup H I hI A ⟶ K) (hg : CategoryTheory.CategoryStruct.comp (pointwiseQuotientMk H I hI A) g = f) : g = pointwiseQuotientLift H I hI A K f hf

A homomorphism out of the pointwise quotient is uniquely determined by its composite with the quotient projection.