Base change of commutative Hopf algebras

This file packages the scalar extension K ⊗[k] H of a commutative Hopf k-algebra as a commutative Hopf K-algebra, functorially in the bundled commutative Hopf algebra. It also records the corresponding base-change equivalence on functors of points.

It is the bundled Hopf-algebra base-change layer 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

• CommHopfAlgCat.baseChange: the bundled Hopf K-algebra K ⊗[k] H.
• CommHopfAlgCat.baseChangeMap: scalar extension of a coordinate morphism.
• CommHopfAlgCat.baseChangeFunctor: functorial base change on commutative Hopf algebras.
• CommHopfAlgCat.baseChangePointsMulEquiv: the inherited point equivalence (K ⊗[k] H →ₐ[K] A) ≃* (H →ₐ[k] A).

References

This builds on Tau Ceti's unbundled base-change equivalence AlgHom.baseChangePointsMulEquiv and its naturality lemmas, plus Mathlib's Bialgebra.TensorProduct.map.

@[reducible, inline]

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

Base change of a 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

• TauCeti.CommHopfAlgCat.baseChange H = { X := TensorProduct k K ↑H, commRing := Algebra.TensorProduct.instCommRing, hopfAlgebra := TensorProduct.instHopfAlgebra }

@[reducible, inline]

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

Scalar extension of a morphism of commutative Hopf algebras.

Equations

• TauCeti.CommHopfAlgCat.baseChangeMap φ = CommHopfAlgCat.ofHom (Bialgebra.TensorProduct.map (BialgHom.id K K) (CommHopfAlgCat.Hom.hom φ))

@[simp]

theorem TauCeti.CommHopfAlgCat.hom_baseChangeMap {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : _root_.CommHopfAlgCat k} (φ : H ⟶ L) : CommHopfAlgCat.Hom.hom (baseChangeMap φ) = Bialgebra.TensorProduct.map (BialgHom.id K K) (CommHopfAlgCat.Hom.hom φ)

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

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

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

@[reducible, inline]

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

Base change is functorial on commutative Hopf algebras.

Equations

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

@[simp]

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

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

@[simp]

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

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

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

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

Equations

• TauCeti.CommHopfAlgCat.baseChangePointsMulEquiv A H = TauCeti.AlgHom.baseChangePointsMulEquiv.symm

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangePointsMulEquiv_apply_apply {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (A : CommAlgCat K) (H : _root_.CommHopfAlgCat k) (f : ↑(HopfAlgebra.points A)) (h : ↑H) : ((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.CommHopfAlgCat.baseChangePointsMulEquiv_symm_apply_tmul {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (A : CommAlgCat K) (H : _root_.CommHopfAlgCat k) (f : ↑(HopfAlgebra.points (CommAlgCat.restrictScalarsObj (algebraMap k K) A))) (s : K) (h : ↑H) : ((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.CommHopfAlgCat.baseChangePointsMulEquiv_mapValue {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {A B : CommAlgCat K} (H : _root_.CommHopfAlgCat 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.CommHopfAlgCat.baseChangePointsMulEquiv_mapDomain {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {A : CommAlgCat K} {H L : _root_.CommHopfAlgCat k} (φ : H ⟶ L) (f : ↑(HopfAlgebra.points A)) : (baseChangePointsMulEquiv A H) ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom (baseChangeMap φ))) f) = (AlgHom.mapDomain (CommHopfAlgCat.Hom.hom φ)) ((baseChangePointsMulEquiv A L) f)

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