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.

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.baseChangeMap_surjective: base change preserves surjectivity.
• CommHopfAlgCat.baseChangeMap_surjective_of_iso: surjectivity in isomorphic presentations.
• CommHopfAlgCat.baseChangeMap_injective: flat base change preserves injectivity.
• CommHopfAlgCat.baseChangeFunctor: functorial base change on commutative Hopf algebras.
• CommHopfAlgCat.baseChangePointsMulEquiv: the inherited point equivalence (K ⊗[k] H →ₐ[K] A) ≃* (H →ₐ[k] A).
• CommHopfAlgCat.baseChangeIsoPointsMulEquiv: the same equivalence for a Hopf K-algebra presented as a scalar extension by an isomorphism L ≅ K ⊗[k] H.
• CommHopfAlgCat.baseChangeIsoPointsMulEquiv_mapPointsFunctor: point transport through such a presentation commutes with a compatible square of coordinate morphisms.

See also

• AlgHom.baseChangePointsMulEquiv: unbundled base-change equivalence and naturality lemmas.
• Bialgebra.TensorProduct.map: tensor product map on bialgebras.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.baseChange {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (H : CommHopfAlgCat k) : 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 = ↧(TensorProduct k K ↑H)

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.baseChangeMap {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : 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 : 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 : 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.

theorem TauCeti.CommHopfAlgCat.baseChangeMap_surjective {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : CommHopfAlgCat k} (φ : H ⟶ L) (hφ : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom φ)) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (baseChangeMap φ))

Base change along k → K preserves surjectivity of a morphism of commutative Hopf algebras.

theorem TauCeti.CommHopfAlgCat.baseChangeMap_injective {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] [Module.Flat k K] {H L : CommHopfAlgCat k} (φ : H ⟶ L) (hφ : Function.Injective ⇑(CommHopfAlgCat.Hom.hom φ)) : Function.Injective ⇑(CommHopfAlgCat.Hom.hom (baseChangeMap φ))

Flat base change preserves injectivity of a morphism of commutative Hopf algebras.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.baseChangeFunctor {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] : CategoryTheory.Functor (CommHopfAlgCat k) (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 : 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 : CommHopfAlgCat k} (φ : H ⟶ L) : baseChangeFunctor.map φ = baseChangeMap φ

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

noncomputable def TauCeti.CommHopfAlgCat.baseChangeTowerIso (k : Type u) (K : Type w) [CommRing k] [CommRing K] [Algebra k K] {E : Type v} [CommRing E] [Algebra k E] [Algebra E K] [IsScalarTower k E K] (H : CommHopfAlgCat k) : baseChange (baseChange H) ≅ baseChange H

Base change of commutative Hopf algebras composes in stages. For a tower k → E → K, extending a coordinate Hopf algebra to E and then to K agrees with extending it to K in one step.

Contravariantly this says that the fibre of an affine group scheme over K may be computed through an intermediate ring, which is how a group split by a finite extension is recognised over an algebraic closure.

Equations

• TauCeti.CommHopfAlgCat.baseChangeTowerIso k K H = CommHopfAlgCat.isoMk (TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv k E (↑H) K)

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeTowerIso_hom_apply (k : Type u) (K : Type w) [CommRing k] [CommRing K] [Algebra k K] {E : Type v} [CommRing E] [Algebra k E] [Algebra E K] [IsScalarTower k E K] (H : CommHopfAlgCat k) (s : K) (e : E) (h : ↑H) : (CommHopfAlgCat.Hom.hom (baseChangeTowerIso k K H).hom) (s ⊗ₜ[E] (e ⊗ₜ[k] h)) = (e • s) ⊗ₜ[k] h

The tower comparison of coordinate Hopf algebras absorbs the intermediate scalar.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeTowerIso_inv_apply (k : Type u) (K : Type w) [CommRing k] [CommRing K] [Algebra k K] {E : Type v} [CommRing E] [Algebra k E] [Algebra E K] [IsScalarTower k E K] (H : CommHopfAlgCat k) (s : K) (h : ↑H) : (CommHopfAlgCat.Hom.hom (baseChangeTowerIso k K H).inv) (s ⊗ₜ[k] h) = s ⊗ₜ[E] (1 ⊗ₜ[k] h)

The inverse tower comparison inserts the unit of the intermediate ring.

noncomputable def TauCeti.CommHopfAlgCat.baseChangePointsMulEquiv {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] (A : CommAlgCat K) (H : 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 : 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 : 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 : 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 : 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.

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

The points of a commutative Hopf K-algebra presented as a scalar extension. An isomorphism e : L ≅ K ⊗[k] H identifies the points of L on a value algebra A with the points of H on A with its scalars restricted to k; the carrier L need not be the tensor product itself. This is baseChangePointsMulEquiv preceded by transport along e.

Equations

• TauCeti.CommHopfAlgCat.baseChangeIsoPointsMulEquiv e A = (TauCeti.AlgHom.mapDomainMulEquiv (CommHopfAlgCat.ofIso e.symm)).trans (TauCeti.CommHopfAlgCat.baseChangePointsMulEquiv A H)

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeIsoPointsMulEquiv_apply_apply {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {L : CommHopfAlgCat K} (e : L ≅ baseChange H) (A : CommAlgCat K) (f : ↑(HopfAlgebra.points A)) (h : ↑H) : ((baseChangeIsoPointsMulEquiv e A) f).ofConv h = f.ofConv ((CategoryTheory.ConcreteCategory.hom e.inv) (1 ⊗ₜ[k] h))

The presented point equivalence evaluates a point of L at the image of 1 ⊗ h under the presenting isomorphism.

theorem TauCeti.CommHopfAlgCat.baseChangeIsoPointsMulEquiv_mapPointsFunctor {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H G : CommHopfAlgCat k} {HK GK : CommHopfAlgCat K} (e : HK ≅ baseChange H) (gG : baseChange G ⟶ GK) (f : H ⟶ G) (fK : HK ⟶ GK) (hcompat : CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp (baseChangeMap f) gG) = fK) (A : CommAlgCat K) (q : ↑(HopfAlgebra.points A)) : (baseChangeIsoPointsMulEquiv e A) (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom fK))) = WithConv.toConv (((baseChangePointsMulEquiv A G) (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom gG)))).ofConv.comp ↑(CommHopfAlgCat.Hom.hom f))

Point transport through a scalar-extension presentation commutes with a compatible square of coordinate morphisms.

theorem TauCeti.CommHopfAlgCat.baseChangeIsoPointsMulEquiv_mapPoints {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {L : CommHopfAlgCat K} (e : L ≅ baseChange H) {A B : CommAlgCat K} (χ : A ⟶ B) (f : ↑(HopfAlgebra.points A)) : (baseChangeIsoPointsMulEquiv e B) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints χ)) f) = (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints ((CommAlgCat.restrictScalars (algebraMap k K)).map χ))) ((baseChangeIsoPointsMulEquiv e A) f)

The presented point equivalence is natural in the value algebra.

theorem CommHopfAlgCat.baseChangeMap_surjective_of_iso {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : CommHopfAlgCat k} {H' L' : CommHopfAlgCat K} (f : H ⟶ L) (hf : Function.Surjective ⇑(Hom.hom f)) (eH : H' ≅ TauCeti.CommHopfAlgCat.baseChange H) (eL : TauCeti.CommHopfAlgCat.baseChange L ≅ L') : Function.Surjective ⇑(Hom.hom (CategoryTheory.CategoryStruct.comp eH.hom (CategoryTheory.CategoryStruct.comp (TauCeti.CommHopfAlgCat.baseChangeMap f) eL.hom)))

A surjective coordinate map remains surjective after scalar extension and transport through isomorphic presentations of its source and target.