Products of finite-type commutative Hopf algebras

This file packages the tensor product of two finite-type commutative Hopf algebras as another object of FiniteTypeCommHopfAlgCat. On affine group schemes this is the coordinate algebra of the direct product. The Hopf-algebra structure is Mathlib's tensor-product Hopf algebra; the finite-type input is Mathlib's stability of finite type under base change, followed by transitivity of finite type along R → H₁ → H₁ ⊗[R] H₂.

The coordinate inclusions H₁ → H₁ ⊗[R] H₂ and H₂ → H₁ ⊗[R] H₂ are also bundled as morphisms in FiniteTypeCommHopfAlgCat. The points of the finite-type product are identified with pairs of points by the existing product-points equivalence from TauCeti.Algebra.AlgebraicGroup.Product.

This is a finite-type wrapper for the ReductiveGroups roadmap Layer 0 product/functor-of-points infrastructure: affine group schemes of finite type should remain finite type under products.

theorem TauCeti.FiniteTypeCommHopfAlgCat.tensorProduct_finiteType {R : Type u} [CommRing R] (A B : Type v) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra.FiniteType R A] [Algebra.FiniteType R B] : Algebra.FiniteType R (TensorProduct R A B)

The tensor product of two finite-type commutative algebras is finite type over the base.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.tensorProduct {R : Type u} [CommRing R] (H K : FiniteTypeCommHopfAlgCat R) : FiniteTypeCommHopfAlgCat R

The tensor product of two finite-type commutative Hopf algebras, bundled as a finite-type commutative Hopf algebra.

Contravariantly, this is the coordinate-Hopf-algebra model for the product of the represented affine group schemes.

Equations

• H.tensorProduct K = TauCeti.FiniteTypeCommHopfAlgCat.of R (TensorProduct R ↑H.obj ↑K.obj)

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.includeLeft {R : Type u} [CommRing R] (H K : FiniteTypeCommHopfAlgCat R) : H ⟶ H.tensorProduct K

The left coordinate inclusion H → H ⊗[R] K, bundled in the finite-type commutative Hopf-algebra category. On points this is the first projection from product points.

Equations

• H.includeLeft K = TauCeti.FiniteTypeCommHopfAlgCat.ofHom TauCeti.Bialgebra.TensorProduct.includeLeft

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.includeRight {R : Type u} [CommRing R] (H K : FiniteTypeCommHopfAlgCat R) : K ⟶ H.tensorProduct K

The right coordinate inclusion K → H ⊗[R] K, bundled in the finite-type commutative Hopf-algebra category. On points this is the second projection from product points.

Equations

• H.includeRight K = TauCeti.FiniteTypeCommHopfAlgCat.ofHom TauCeti.Bialgebra.TensorProduct.includeRight

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.includeLeft_apply {R : Type u} [CommRing R] (H K : FiniteTypeCommHopfAlgCat R) (h : ↑H.obj) : (toBialgHom (H.includeLeft K)) h = h ⊗ₜ[R] 1

The left coordinate inclusion sends h to h ⊗ 1.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.includeRight_apply {R : Type u} [CommRing R] (H K : FiniteTypeCommHopfAlgCat R) (k : ↑K.obj) : (toBialgHom (H.includeRight K)) k = 1 ⊗ₜ[R] k

The right coordinate inclusion sends k to 1 ⊗ k.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv {R : Type u} [CommRing R] (A : CommAlgCat R) (H K : FiniteTypeCommHopfAlgCat R) : ↑(HopfAlgebra.points A) ≃* ↑(HopfAlgebra.points A) × ↑(HopfAlgebra.points A)

The product-points equivalence for the finite-type tensor-product object.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv A H K = TauCeti.AffineGroup.Product.pointsMulEquiv

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv_fst {R : Type u} [CommRing R] (A : CommAlgCat R) (H K : FiniteTypeCommHopfAlgCat R) (f : ↑(HopfAlgebra.points A)) : ((pointsMulEquiv A H K) f).1 = (CategoryTheory.ConcreteCategory.hom ((pointsFunctor.map (H.includeLeft K).op).app A)) f

The first component of pointsMulEquiv is induced by the left coordinate inclusion.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv_snd {R : Type u} [CommRing R] (A : CommAlgCat R) (H K : FiniteTypeCommHopfAlgCat R) (f : ↑(HopfAlgebra.points A)) : ((pointsMulEquiv A H K) f).2 = (CategoryTheory.ConcreteCategory.hom ((pointsFunctor.map (H.includeRight K).op).app A)) f

The second component of pointsMulEquiv is induced by the right coordinate inclusion.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv_symm_apply {R : Type u} [CommRing R] (A : CommAlgCat R) (H K : FiniteTypeCommHopfAlgCat R) (p : ↑(HopfAlgebra.points A) × ↑(HopfAlgebra.points A)) : (pointsMulEquiv A H K).symm p = WithConv.toConv (Algebra.TensorProduct.productMap p.1.ofConv p.2.ofConv)

The inverse of pointsMulEquiv is Mathlib's tensor-product product map.

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv_mapValue {R : Type u} [CommRing R] (A : CommAlgCat R) {B : CommAlgCat R} (H K : FiniteTypeCommHopfAlgCat R) (φ : ↑A →ₐ[R] ↑B) (f : ↑(HopfAlgebra.points A)) : (pointsMulEquiv B H K) ((AlgHom.mapValue φ) f) = ((AlgHom.mapValue φ) ((pointsMulEquiv A H K) f).1, (AlgHom.mapValue φ) ((pointsMulEquiv A H K) f).2)

The product-points equivalence is natural in the value algebra: post-composing a point of the product by φ, then splitting it into its two factor points, agrees with splitting first and then post-composing each factor point by φ.

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv_mapValue_fst {R : Type u} [CommRing R] (A : CommAlgCat R) {B : CommAlgCat R} (H K : FiniteTypeCommHopfAlgCat R) (φ : ↑A →ₐ[R] ↑B) (f : ↑(HopfAlgebra.points A)) : ((pointsMulEquiv B H K) ((AlgHom.mapValue φ) f)).1 = (AlgHom.mapValue φ) ((pointsMulEquiv A H K) f).1

First-component form of pointsMulEquiv_mapValue.

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv_mapValue_snd {R : Type u} [CommRing R] (A : CommAlgCat R) {B : CommAlgCat R} (H K : FiniteTypeCommHopfAlgCat R) (φ : ↑A →ₐ[R] ↑B) (f : ↑(HopfAlgebra.points A)) : ((pointsMulEquiv B H K) ((AlgHom.mapValue φ) f)).2 = (AlgHom.mapValue φ) ((pointsMulEquiv A H K) f).2

Second-component form of pointsMulEquiv_mapValue.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mapValue_pointsMulEquiv_symm_apply {R : Type u} [CommRing R] (A : CommAlgCat R) {B : CommAlgCat R} (H K : FiniteTypeCommHopfAlgCat R) (φ : ↑A →ₐ[R] ↑B) (p : ↑(HopfAlgebra.points A) × ↑(HopfAlgebra.points A)) : (AlgHom.mapValue φ) ((pointsMulEquiv A H K).symm p) = (pointsMulEquiv B H K).symm ((AlgHom.mapValue φ) p.1, (AlgHom.mapValue φ) p.2)

The inverse product-points map is natural in the value algebra: assembling an A-valued product point from a pair of factor points and post-composing by φ is the same as post-composing both factor points by φ and then assembling the resulting B-valued point.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mapValue_pointsMulEquiv_symm_apply_tmul {R : Type u} [CommRing R] (A : CommAlgCat R) {B : CommAlgCat R} (H K : FiniteTypeCommHopfAlgCat R) (φ : ↑A →ₐ[R] ↑B) (p : ↑(HopfAlgebra.points A) × ↑(HopfAlgebra.points A)) (x : ↑H.obj) (y : ↑K.obj) : ((AlgHom.mapValue φ) ((pointsMulEquiv A H K).symm p)).ofConv (x ⊗ₜ[R] y) = φ (p.1.ofConv x * p.2.ofConv y)

On pure tensors, naturality of the inverse product-points map evaluates post-composition by φ as applying φ to the product of the two factor values.

theorem TauCeti.FiniteTypeCommHopfAlgCat.pointsMulEquiv_symm_mapValue_apply_tmul {R : Type u} [CommRing R] (A : CommAlgCat R) {B : CommAlgCat R} (H K : FiniteTypeCommHopfAlgCat R) (φ : ↑A →ₐ[R] ↑B) (p : ↑(HopfAlgebra.points A) × ↑(HopfAlgebra.points A)) (x : ↑H.obj) (y : ↑K.obj) : ((pointsMulEquiv B H K).symm ((AlgHom.mapValue φ) p.1, (AlgHom.mapValue φ) p.2)).ofConv (x ⊗ₜ[R] y) = φ (p.1.ofConv x) * φ (p.2.ofConv y)

On pure tensors, assembling after post-composing both factor points by φ multiplies the two post-composed factor values.