Finite-type commutative Hopf algebras

This file packages finite-type commutative Hopf algebras over a commutative ring R. These are the coordinate Hopf algebras for affine group schemes of finite type in the reductive-groups roadmap: the Hopf algebra structure carries the group law, while Algebra.FiniteType R H records the finite-type coordinate-ring hypothesis separately.

Main declarations

• TauCeti.finiteTypeCommHopfAlgProperty: the object property on CommHopfAlgCat R selecting objects whose underlying R-algebra is of finite type.
• TauCeti.FiniteTypeCommHopfAlgCat: the full subcategory of finite-type commutative Hopf algebras.
• TauCeti.FiniteTypeCommHopfAlgCat.of: construct a bundled finite-type commutative Hopf algebra from unbundled typeclasses.
• TauCeti.FiniteTypeCommHopfAlgCat.isNoetherianRing: the coordinate ring underlying a finite-type commutative Hopf algebra over a Noetherian ring is Noetherian.
• forget₂ (FiniteTypeCommHopfAlgCat R) (FGAlgCat R): the forgetful functor to Mathlib's finitely generated commutative R-algebras.
• TauCeti.FiniteTypeCommHopfAlgCat.pointsFunctor: the inherited contravariant functor of points.

References

This is the finite-type coordinate-Hopf-algebra wrapper requested by ReductiveGroups/README.md in TauCetiRoadmap, in the standing hypotheses and Layer 0 three-way dictionary: an affine group scheme of finite type over k is modeled by a commutative Hopf k-algebra finitely generated as a k-algebra. The finite-type algebra infrastructure is Mathlib's FGAlgCat and Algebra.FiniteType; the Hopf algebra category is Mathlib's bundled CommHopfAlgCat, on top of which Tau Ceti adds the points functor.

def TauCeti.finiteTypeCommHopfAlgProperty (R : Type u) [CommRing R] : CategoryTheory.ObjectProperty (CommHopfAlgCat R)

The object property on commutative Hopf algebras selecting finite-type coordinate algebras.

Equations

• TauCeti.finiteTypeCommHopfAlgProperty R H = Algebra.FiniteType R ↑H

@[simp]

theorem TauCeti.finiteTypeCommHopfAlgProperty_iff {R : Type u} [CommRing R] (H : CommHopfAlgCat R) : finiteTypeCommHopfAlgProperty R H ↔ Algebra.FiniteType R ↑H

Membership in the finite-type commutative Hopf algebra object property.

@[reducible, inline]

abbrev TauCeti.FiniteTypeCommHopfAlgCat (R : Type u) [CommRing R] : Type (max u (u_1 + 1))

The category of finite-type commutative Hopf algebras over a commutative ring R.

This is the full subcategory of CommHopfAlgCat R on objects whose underlying commutative R-algebra is finitely generated. The finite-type hypothesis is deliberately a separate object property, not part of the Hopf algebra typeclass.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat R = (TauCeti.finiteTypeCommHopfAlgProperty R).FullSubcategory

@[instance_reducible]

instance TauCeti.FiniteTypeCommHopfAlgCat.instCoeSortType {R : Type u} [CommRing R] : CoeSort (FiniteTypeCommHopfAlgCat R) (Type v)

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.instCoeSortType = { coe := fun (H : TauCeti.FiniteTypeCommHopfAlgCat R) => ↑H.obj }

@[instance_reducible]

instance TauCeti.FiniteTypeCommHopfAlgCat.commRing {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : CommRing ↑H.obj

Equations

• H.commRing = CommHopfAlgCat.instCommRingObjForgetBialgHomX

@[instance_reducible]

instance TauCeti.FiniteTypeCommHopfAlgCat.hopfAlgebra {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : HopfAlgebra R ↑H.obj

Equations

• H.hopfAlgebra = CommHopfAlgCat.instHopfAlgebraObjForgetBialgHomX

instance TauCeti.FiniteTypeCommHopfAlgCat.finiteType {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : Algebra.FiniteType R ↑H.obj

instance TauCeti.FiniteTypeCommHopfAlgCat.isNoetherianRing {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) [IsNoetherianRing R] : IsNoetherianRing ↑H.obj

A finite-type commutative Hopf algebra over a Noetherian ring has a Noetherian underlying coordinate ring.

@[reducible, inline]

abbrev TauCeti.FiniteTypeCommHopfAlgCat.of (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] [Algebra.FiniteType R H] : FiniteTypeCommHopfAlgCat R

Construct a bundled finite-type commutative Hopf algebra from the usual unbundled typeclasses.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.of R H = { obj := ↧H, property := inst✝ }

@[reducible, inline]

abbrev TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (φ : H ⟶ K) : ↑H.obj →ₐc[R] ↑K.obj

Turn a morphism in FiniteTypeCommHopfAlgCat back into a bialgebra morphism.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom φ = CommHopfAlgCat.Hom.hom φ.hom

@[reducible, inline]

abbrev TauCeti.FiniteTypeCommHopfAlgCat.ofHom {R : Type u} [CommRing R] {H K : Type v} [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] [Algebra.FiniteType R H] [Algebra.FiniteType R K] (φ : H →ₐc[R] K) : of R H ⟶ of R K

Typecheck a bialgebra morphism between finite-type commutative Hopf algebras as a morphism in FiniteTypeCommHopfAlgCat.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.ofHom φ = CategoryTheory.ObjectProperty.homMk (CommHopfAlgCat.ofHom φ)

theorem TauCeti.FiniteTypeCommHopfAlgCat.hom_ext {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} {φ ψ : H ⟶ K} (h : toBialgHom φ = toBialgHom ψ) : φ = ψ

Two morphisms of finite-type commutative Hopf algebras are equal when their underlying bialgebra morphisms are equal.

theorem TauCeti.FiniteTypeCommHopfAlgCat.hom_ext_iff {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} {φ ψ : H ⟶ K} : φ = ψ ↔ toBialgHom φ = toBialgHom ψ

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom_id {R : Type u} [CommRing R] {H : FiniteTypeCommHopfAlgCat R} : toBialgHom (CategoryTheory.CategoryStruct.id H) = BialgHom.id R ↑H.obj

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom_comp {R : Type u} [CommRing R] {H K L : FiniteTypeCommHopfAlgCat R} (φ : H ⟶ K) (ψ : K ⟶ L) : toBialgHom (CategoryTheory.CategoryStruct.comp φ ψ) = (toBialgHom ψ).comp (toBialgHom φ)

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.ofHom_toBialgHom {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (φ : H ⟶ K) : ofHom (toBialgHom φ) = φ

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom_ofHom {R : Type u} [CommRing R] {H K : Type v} [CommRing H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] [Algebra.FiniteType R H] [Algebra.FiniteType R K] (φ : H →ₐc[R] K) : toBialgHom (ofHom φ) = φ

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.forget₂_commHopfAlgCat_obj {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : (CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat R) (CommHopfAlgCat R)).obj H = H.obj

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.forget₂_commHopfAlgCat_map {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (φ : H ⟶ K) : (CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat R) (CommHopfAlgCat R)).map φ = φ.hom

@[instance_reducible]

instance TauCeti.FiniteTypeCommHopfAlgCat.hasForgetToFGAlgCat {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (FiniteTypeCommHopfAlgCat R) (FGAlgCat R)

The forgetful functor from finite-type commutative Hopf algebras to finitely generated commutative algebras.

Equations

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

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.forget₂_fgAlgCat_obj {R : Type u} [CommRing R] (H : FiniteTypeCommHopfAlgCat R) : (CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat R) (FGAlgCat R)).obj H = { obj := ↧↑H.obj, property := ⋯ }

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.forget₂_fgAlgCat_map {R : Type u} [CommRing R] {H K : FiniteTypeCommHopfAlgCat R} (φ : H ⟶ K) : (CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat R) (FGAlgCat R)).map φ = CategoryTheory.ObjectProperty.homMk (CommAlgCat.ofHom ↑(toBialgHom φ))

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.pointsFunctor {R : Type u} [CommRing R] : CategoryTheory.Functor (FiniteTypeCommHopfAlgCat R)ᵒᵖ (CategoryTheory.Functor (CommAlgCat R) GrpCat)

The contravariant group-valued functor of points of a finite-type commutative Hopf algebra.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.pointsFunctor = (CategoryTheory.forget₂ (TauCeti.FiniteTypeCommHopfAlgCat R) (CommHopfAlgCat R)).op.comp TauCeti.CommHopfAlgCat.pointsFunctor

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsFunctor_obj {R : Type u} [CommRing R] (H : (FiniteTypeCommHopfAlgCat R)ᵒᵖ) : pointsFunctor.obj H = HopfAlgebra.pointsFunctor

The object part of pointsFunctor is the points functor of the underlying commutative Hopf algebra.

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsFunctor_map {R : Type u} [CommRing R] {H K : (FiniteTypeCommHopfAlgCat R)ᵒᵖ} (φ : H ⟶ K) : pointsFunctor.map φ = CommHopfAlgCat.mapPointsFunctor φ.unop.hom

The morphism part of pointsFunctor is pre-composition in the coordinate commutative Hopf algebra.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsFunctor_map_app_apply_apply {R : Type u} [CommRing R] {H K : (FiniteTypeCommHopfAlgCat R)ᵒᵖ} (φ : H ⟶ K) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) (h : ↑(Opposite.unop K).obj) : (have this := ((CategoryTheory.ConcreteCategory.hom ((pointsFunctor.map φ).app A)) f).ofConv; this) h = f.ofConv ((toBialgHom φ.unop) h)

Pointwise form of the morphism part of pointsFunctor: the image of a point f under φ sends h to the value of f at the image of h under φ.