Base change of finite-type commutative Hopf algebras

This file packages the scalar extension K ⊗[k] H of a finite-type commutative Hopf k-algebra as a finite-type commutative Hopf K-algebra. The generic bundled commutative Hopf-algebra base-change API is in CommHopfAlgCatBaseChange; this file restricts it to the finite-type full subcategory, using Mathlib's finite-type base-change instance.

It is the finite-type coordinate-Hopf-algebra wrapper for the ReductiveGroups roadmap Layer 0 base-change item: geometric notions are studied after replacing the coordinate Hopf algebra H by K ⊗[k] H, and the functor of points of this base-changed object is identified with the original points evaluated on K-algebras.

Main declarations

• FiniteTypeCommHopfAlgCat.baseChange: the bundled finite-type Hopf K-algebra K ⊗[k] H.
• FiniteTypeCommHopfAlgCat.baseChangeMap: scalar extension of a coordinate morphism.
• FiniteTypeCommHopfAlgCat.baseChangeFunctor: functorial base change.
• FiniteTypeCommHopfAlgCat.baseChangeTensorProductIso: the canonical comparison between the base change of a tensor product and the tensor product of the base changes.
• FiniteTypeCommHopfAlgCat.baseChangeMap_includeLeft_injective and FiniteTypeCommHopfAlgCat.baseChangeMap_includeRight_injective: the base-changed coordinate inclusions into a product are injective.
• FiniteTypeCommHopfAlgCat.baseChangeIsoOfObjIso: lift an isomorphism between specified underlying base-changed objects to the finite-type full subcategory.
• FiniteTypeCommHopfAlgCat.baseChangePointsMulEquiv: the inherited point equivalence (K ⊗[k] H →ₐ[K] A) ≃* (H →ₐ[k] A).

References

This builds on CommHopfAlgCat.baseChange and CommHopfAlgCat.baseChangeFunctor, whose point equivalence ultimately comes from Tau Ceti's unbundled AlgHom.baseChangePointsMulEquiv, plus Mathlib's Algebra.FiniteType.baseChange.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.baseChange {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (H : FiniteTypeCommHopfAlgCat k) : FiniteTypeCommHopfAlgCat K

Base change of a finite-type commutative Hopf algebra along k → K.

The underlying coordinate Hopf algebra is K ⊗[k] H, with the tensor-product Hopf algebra structure over K.

Equations

• H.baseChange = { obj := TauCeti.CommHopfAlgCat.baseChange H.obj, property := ⋯ }

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : FiniteTypeCommHopfAlgCat k} (φ : H ⟶ L) : H.baseChange ⟶ L.baseChange

Scalar extension of a morphism of finite-type commutative Hopf algebras.

Equations

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

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom_baseChangeMap {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : FiniteTypeCommHopfAlgCat k} (φ : H ⟶ L) : toBialgHom (baseChangeMap φ) = Bialgebra.TensorProduct.map (BialgHom.id K K) (toBialgHom φ)

The underlying bialgebra hom of baseChangeMap is tensoring the morphism with the identity on the new base.

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap_apply_tmul {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : FiniteTypeCommHopfAlgCat k} (φ : H ⟶ L) (s : K) (h : ↑H.obj) : (toBialgHom (baseChangeMap φ)) (s ⊗ₜ[k] h) = s ⊗ₜ[k] (toBialgHom φ) h

On pure tensors, baseChangeMap applies the original morphism to the second factor.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.baseChangeFunctor {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] : CategoryTheory.Functor (FiniteTypeCommHopfAlgCat k) (FiniteTypeCommHopfAlgCat K)

Base change is functorial on finite-type commutative Hopf algebras.

Equations

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

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeFunctor_obj {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (H : FiniteTypeCommHopfAlgCat k) : baseChangeFunctor.obj H = H.baseChange

The object part of baseChangeFunctor is the bundled base-change object.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeFunctor_map {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : FiniteTypeCommHopfAlgCat k} (φ : H ⟶ L) : baseChangeFunctor.map φ = baseChangeMap φ

The morphism part of baseChangeFunctor is scalar extension of coordinate morphisms.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.baseChangeTensorProductIso {k : Type u} [CommRing k] (K : Type w) [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) : (H.tensorProduct L).baseChange ≅ H.baseChange.tensorProduct L.baseChange

Base change commutes with finite-type affine-group products.

This is Bialgebra.TensorProduct.baseChangeTensorBialgEquiv bundled as an isomorphism in the finite-type commutative Hopf-algebra category.

Equations

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

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom_baseChangeTensorProductIso_hom {k : Type u} [CommRing k] (K : Type w) [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) : toBialgHom (baseChangeTensorProductIso K H L).hom = ↑(Bialgebra.TensorProduct.baseChangeTensorBialgEquiv k K ↑H.obj ↑L.obj)

The underlying bialgebra equivalence of the finite-type product/base-change isomorphism is the canonical tensor-product comparison.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.toBialgHom_baseChangeTensorProductIso_inv {k : Type u} [CommRing k] (K : Type w) [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) : toBialgHom (baseChangeTensorProductIso K H L).inv = ↑(Bialgebra.TensorProduct.baseChangeTensorBialgEquiv k K ↑H.obj ↑L.obj).symm

The underlying bialgebra equivalence of the inverse finite-type product/base-change isomorphism is the inverse canonical tensor-product comparison.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap_includeLeft_comp_baseChangeTensorProductIso_hom {k : Type u} [CommRing k] (K : Type w) [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) : CategoryTheory.CategoryStruct.comp (baseChangeMap (H.includeLeft L)) (baseChangeTensorProductIso K H L).hom = H.baseChange.includeLeft L.baseChange

The product/base-change isomorphism carries the base change of the left coordinate inclusion to the left coordinate inclusion between the base-changed factors.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap_includeLeft_comp_baseChangeTensorProductIso_hom_assoc {k : Type u} [CommRing k] (K : Type w) [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) {Z : FiniteTypeCommHopfAlgCat K} (h : H.baseChange.tensorProduct L.baseChange ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeMap (H.includeLeft L)) (CategoryTheory.CategoryStruct.comp (baseChangeTensorProductIso K H L).hom h) = CategoryTheory.CategoryStruct.comp (H.baseChange.includeLeft L.baseChange) h

The product/base-change isomorphism carries the base change of the left coordinate inclusion to the left coordinate inclusion between the base-changed factors.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap_includeRight_comp_baseChangeTensorProductIso_hom {k : Type u} [CommRing k] (K : Type w) [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) : CategoryTheory.CategoryStruct.comp (baseChangeMap (H.includeRight L)) (baseChangeTensorProductIso K H L).hom = H.baseChange.includeRight L.baseChange

The product/base-change isomorphism carries the base change of the right coordinate inclusion to the right coordinate inclusion between the base-changed factors.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap_includeRight_comp_baseChangeTensorProductIso_hom_assoc {k : Type u} [CommRing k] (K : Type w) [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) {Z : FiniteTypeCommHopfAlgCat K} (h : H.baseChange.tensorProduct L.baseChange ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeMap (H.includeRight L)) (CategoryTheory.CategoryStruct.comp (baseChangeTensorProductIso K H L).hom h) = CategoryTheory.CategoryStruct.comp (H.baseChange.includeRight L.baseChange) h

The product/base-change isomorphism carries the base change of the right coordinate inclusion to the right coordinate inclusion between the base-changed factors.

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap_includeLeft_injective {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) : Function.Injective ⇑(toBialgHom (baseChangeMap (H.includeLeft L)))

The base change of the left coordinate inclusion into a product is injective.

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeMap_includeRight_injective {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (H L : FiniteTypeCommHopfAlgCat k) : Function.Injective ⇑(toBialgHom (baseChangeMap (H.includeRight L)))

The base change of the right coordinate inclusion into a product is injective.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.baseChangeIsoOfObjIso {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : FiniteTypeCommHopfAlgCat k} {H' : FiniteTypeCommHopfAlgCat K} {B : CommHopfAlgCat k} {B' : CommHopfAlgCat K} (hH : H.obj = B) (hH' : H'.obj = B') (e : CommHopfAlgCat.baseChange B ≅ B') : H.baseChange ≅ H'

Lift an isomorphism between specified underlying base-changed Hopf algebras to the finite-type full subcategory. The object equalities record the chosen presentations of the source and target coordinate Hopf algebras.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.baseChangeIsoOfObjIso hH hH' e = (TauCeti.finiteTypeCommHopfAlgProperty K).isoMk (CategoryTheory.eqToIso ⋯ ≪≫ e ≪≫ CategoryTheory.eqToIso ⋯)

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangeIsoOfObjIso_hom {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : FiniteTypeCommHopfAlgCat k} {H' : FiniteTypeCommHopfAlgCat K} {B : CommHopfAlgCat k} {B' : CommHopfAlgCat K} (hH : H.obj = B) (hH' : H'.obj = B') (e : CommHopfAlgCat.baseChange B ≅ B') : (baseChangeIsoOfObjIso hH hH' e).hom.hom = (CategoryTheory.eqToIso ⋯ ≪≫ e ≪≫ CategoryTheory.eqToIso ⋯).hom

The underlying morphism of baseChangeIsoOfObjIso is the supplied isomorphism, conjugated by the specified object equalities.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.baseChangePointsMulEquiv {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (A : CommAlgCat K) (H : FiniteTypeCommHopfAlgCat k) : ↑(HopfAlgebra.points A) ≃* ↑(HopfAlgebra.points (CommAlgCat.restrictScalarsObj (algebraMap k K) A))

The points of the base-changed finite-type Hopf algebra are the original points evaluated on the same algebra, with scalars restricted from K to k.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.baseChangePointsMulEquiv A H = TauCeti.CommHopfAlgCat.baseChangePointsMulEquiv A H.obj

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangePointsMulEquiv_apply_apply {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (A : CommAlgCat K) (H : FiniteTypeCommHopfAlgCat k) (f : ↑(HopfAlgebra.points A)) (h : ↑H.obj) : ((baseChangePointsMulEquiv A H) f).ofConv h = f.ofConv (1 ⊗ₜ[k] h)

Applying the base-change points equivalence restricts a K-point along h ↦ 1 ⊗ h.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangePointsMulEquiv_symm_apply_tmul {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (A : CommAlgCat K) (H : FiniteTypeCommHopfAlgCat k) (f : ↑(HopfAlgebra.points (CommAlgCat.restrictScalarsObj (algebraMap k K) A))) (s : K) (h : ↑H.obj) : ((baseChangePointsMulEquiv A H).symm f).ofConv (s ⊗ₜ[k] h) = s • f.ofConv h

The inverse base-change points equivalence sends a restricted point to s ⊗ h ↦ s • f h.

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangePointsMulEquiv_mapValue {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {A B : CommAlgCat K} (H : FiniteTypeCommHopfAlgCat k) (χ : A ⟶ B) (f : ↑(HopfAlgebra.points A)) : (baseChangePointsMulEquiv B H) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints χ)) f) = (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints ((CommAlgCat.restrictScalars (algebraMap k K)).map χ))) ((baseChangePointsMulEquiv A H) f)

The base-change points equivalence is natural in the value algebra.

theorem TauCeti.FiniteTypeCommHopfAlgCat.baseChangePointsMulEquiv_mapDomain {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {A : CommAlgCat K} {H L : FiniteTypeCommHopfAlgCat k} (φ : H ⟶ L) (f : ↑(HopfAlgebra.points A)) : (baseChangePointsMulEquiv A H) ((AlgHom.mapDomain (toBialgHom (baseChangeMap φ))) f) = (AlgHom.mapDomain (toBialgHom φ)) ((baseChangePointsMulEquiv A L) f)

The base-change points equivalence is natural in the coordinate Hopf algebra.