Base change of finite locally free Cartier duality

Extension of scalars carries a finite locally free bicommutative Hopf algebra over R to one over an R-algebra S, and TauCeti.ConvolutionDual.baseChangeBialgEquiv says that it commutes with finite dualization. This file records both facts in the category TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat, where Cartier duality lives.

Main declarations

• TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty_baseChange: scalar extension preserves finite local freeness and cocommutativity.
• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChange and TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeFunctor: scalar extension of finite locally free bicommutative Hopf algebras, on objects and functorially.
• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso: the scalar extension of a finite dual is the finite dual of the scalar extension, naturally by baseChangeDualIso_hom_naturality and bundled as baseChangeDualNatIso.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

This advances Layer 4, "Cartier duality", of the ReductiveGroups roadmap: compatibility with pullback of the base is what makes Cartier duality usable on fibres and after field extension.

theorem TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty_baseChange (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : finiteLocallyFreeBicommutativeHopfAlgProperty S (CommHopfAlgCat.baseChange ((finiteLocallyFreeBicommutativeHopfAlgProperty R).ι.obj H))

Scalar extension preserves finite local freeness and cocommutativity.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChange {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : FiniteLocallyFreeBicommutativeHopfAlgCat S

Scalar extension of a single finite locally free bicommutative Hopf algebra.

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChange S H = { obj := TauCeti.CommHopfAlgCat.baseChange ((TauCeti.finiteLocallyFreeBicommutativeHopfAlgProperty R).ι.obj H), property := ⋯ }

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeMap {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat R} (f : H ⟶ K) : baseChange S H ⟶ baseChange S K

Scalar extension of a morphism of finite locally free bicommutative Hopf algebras.

Equations

• TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeMap S f = CategoryTheory.ObjectProperty.homMk (TauCeti.CommHopfAlgCat.baseChangeMap f.hom)

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.toBialgHom_baseChangeMap {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat R} (f : H ⟶ K) : toBialgHom (baseChangeMap S f) = Bialgebra.TensorProduct.map (BialgHom.id S S) (toBialgHom f)

The bialgebra morphism underlying baseChangeMap tensors the morphism with the identity on the new base.

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeFunctor (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Functor (FiniteLocallyFreeBicommutativeHopfAlgCat R) (FiniteLocallyFreeBicommutativeHopfAlgCat S)

Scalar extension of finite locally free bicommutative Hopf algebras.

The body is exposed so that baseChangeFunctor R S ⋙ dualFunctor.rightOp reduces to the finite dual of a scalar extension, without which the components of baseChangeDualNatIso do not typecheck. No other declaration here depends on that reduction.

Equations

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

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeFunctor_obj (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : (baseChangeFunctor R S).obj H = baseChange S H

The object part of baseChangeFunctor is scalar extension.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeFunctor_map {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat R} (f : H ⟶ K) : (baseChangeFunctor R S).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (baseChangeMap S f) (CategoryTheory.eqToHom ⋯))

The morphism part of baseChangeFunctor is scalar extension of morphisms.

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeFunctorCompιIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : (baseChangeFunctor R S).comp (finiteLocallyFreeBicommutativeHopfAlgProperty S).ι ≅ (finiteLocallyFreeBicommutativeHopfAlgProperty R).ι.comp CommHopfAlgCat.baseChangeFunctor

Forgetting finite local freeness and cocommutativity turns the restricted scalar extension into the scalar extension of commutative Hopf algebras.

Equations

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

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : baseChange S H.dual ≅ (baseChange S H).dual

Finite dualization commutes with extension of scalars.

Equations

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

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso_hom_apply_tmul_apply_tmul {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) (a b : S) (phi : ConvolutionDual R ↑H.obj) (x : ↑H.obj) : ((CategoryTheory.ConcreteCategory.hom (baseChangeDualIso S H).hom) (a ⊗ₜ[R] phi)).ofConv (b ⊗ₜ[R] x) = a * b * (algebraMap R S) (phi.ofConv x)

The forward map of baseChangeDualIso sends a scalar-extended functional to the scalar-extended evaluation it defines. This is not a simp lemma: the scalar-extended carrier (baseChange S H).obj and the tensor product S ⊗[R] H are the same type but not the same normal form, so the left-hand side is not in simp-normal form.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso_hom_naturality {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat R} (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp (baseChangeMap S (dualMap f)) (baseChangeDualIso S H).hom = CategoryTheory.CategoryStruct.comp (baseChangeDualIso S K).hom (dualMap (baseChangeMap S f))

Finite dualization and scalar extension commute naturally.

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso_hom_naturality_assoc {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat R} (f : H ⟶ K) {Z : FiniteLocallyFreeBicommutativeHopfAlgCat S} (h : (baseChange S H).dual ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeMap S (dualMap f)) (CategoryTheory.CategoryStruct.comp (baseChangeDualIso S H).hom h) = CategoryTheory.CategoryStruct.comp (baseChangeDualIso S K).hom (CategoryTheory.CategoryStruct.comp (dualMap (baseChangeMap S f)) h)

Finite dualization and scalar extension commute naturally.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso_inv_naturality {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat R} (f : H ⟶ K) : CategoryTheory.CategoryStruct.comp (baseChangeDualIso S K).inv (baseChangeMap S (dualMap f)) = CategoryTheory.CategoryStruct.comp (dualMap (baseChangeMap S f)) (baseChangeDualIso S H).inv

The inverse form of baseChangeDualIso_hom_naturality.

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualIso_inv_naturality_assoc {R : Type u} (S : Type u) [CommRing R] [CommRing S] [Algebra R S] {H K : FiniteLocallyFreeBicommutativeHopfAlgCat R} (f : H ⟶ K) {Z : FiniteLocallyFreeBicommutativeHopfAlgCat S} (h : baseChange S H.dual ⟶ Z) : CategoryTheory.CategoryStruct.comp (baseChangeDualIso S K).inv (CategoryTheory.CategoryStruct.comp (baseChangeMap S (dualMap f)) h) = CategoryTheory.CategoryStruct.comp (dualMap (baseChangeMap S f)) (CategoryTheory.CategoryStruct.comp (baseChangeDualIso S H).inv h)

The inverse form of baseChangeDualIso_hom_naturality.

noncomputable def TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualNatIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : dualFunctor.rightOp.comp (baseChangeFunctor R S).op ≅ (baseChangeFunctor R S).comp dualFunctor.rightOp

Finite dualization commutes with scalar extension, as a natural isomorphism of functors FiniteLocallyFreeBicommutativeHopfAlgCat R ⥤ (FiniteLocallyFreeBicommutativeHopfAlgCat S)ᵒᵖ.

Equations

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

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualNatIso_hom_app (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : (baseChangeDualNatIso R S).hom.app H = (baseChangeDualIso S H).inv.op

The components of baseChangeDualNatIso are the objectwise comparisons baseChangeDualIso. They appear inverted because the natural isomorphism lands in an opposite category.

@[simp]

theorem TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.baseChangeDualNatIso_inv_app (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (H : FiniteLocallyFreeBicommutativeHopfAlgCat R) : (baseChangeDualNatIso R S).inv.app H = (baseChangeDualIso S H).hom.op

The inverse components of baseChangeDualNatIso are the objectwise comparisons baseChangeDualIso.