Relative base change of the type-E7 minuscule carrier

The full-weight type-E₇ minuscule carrier over a commutative ring is obtained by base change from its integral coordinate Hopf algebra. Consequently, for a scalar tower ℤ → R → S, extending the carrier from R to S agrees with constructing the carrier directly over S.

This comparison is the relative form of the existing integral base-change presentation. It is the isomorphism used when geometric properties of a carrier over a field are checked after extension to an algebraic closure.

Main declarations

• TauCeti.E7Minuscule.coordinateHopfAlgebraBaseChangeIso: scalar extension of the coordinate Hopf algebra from R to S is the coordinate Hopf algebra over S.
• TauCeti.E7Minuscule.finiteTypeCoordinateHopfAlgebraBaseChangeIso: the same comparison in the category of finite-type commutative Hopf algebras.

References

• B. Conrad, Reductive Group Schemes, §1.
• R. W. Carter, Simple Groups of Lie Type, §4.4.

noncomputable def TauCeti.E7Minuscule.coordinateHopfAlgebraBaseChangeIso (R : Type u) (S : Type (max u v)) [CommRing R] [CommRing S] [Algebra R S] : CommHopfAlgCat.baseChange (coordinateHopfAlgebra R) ≅ coordinateHopfAlgebra S

Scalar extension of the full-weight type-E₇ minuscule carrier from R to S agrees with the carrier obtained directly by base change from its integral model to S.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.coordinateHopfAlgebraBaseChangeIso_hom_tmul (R : Type u) (S : Type (max u v)) [CommRing R] [CommRing S] [Algebra R S] (s : S) (r : R) (x : ↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) definingIdeal)) : (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R S).hom) (s ⊗ₜ[R] (CommHopfAlgCat.Hom.hom (baseChangeCoordinateIso R).inv) (r ⊗ₜ[ℤ] x)) = (CommHopfAlgCat.Hom.hom (baseChangeCoordinateIso S).inv) ((r • s) ⊗ₜ[ℤ] x)

On a pure tensor represented through the integral presentation over R, scalar extension absorbs the intermediate coefficient into the scalar over S.

@[simp]

theorem TauCeti.E7Minuscule.coordinateHopfAlgebraBaseChangeIso_inv_tmul (R : Type u) (S : Type (max u v)) [CommRing R] [CommRing S] [Algebra R S] (s : S) (x : ↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 56) definingIdeal)) : (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R S).inv) ((CommHopfAlgCat.Hom.hom (baseChangeCoordinateIso S).inv) (s ⊗ₜ[ℤ] x)) = s ⊗ₜ[R] (CommHopfAlgCat.Hom.hom (baseChangeCoordinateIso R).inv) (1 ⊗ₜ[ℤ] x)

The inverse scalar-extension comparison inserts the unit of the intermediate ring in the integral presentation.

noncomputable def TauCeti.E7Minuscule.finiteTypeCoordinateHopfAlgebraBaseChangeIso (R : Type u) (S : Type (max u v)) [CommRing R] [CommRing S] [Algebra R S] : (finiteTypeCoordinateHopfAlgebra R).baseChange ≅ finiteTypeCoordinateHopfAlgebra S

The finite-type coordinate Hopf algebra of the full-weight type-E₇ minuscule carrier commutes with scalar extension.

Equations

• TauCeti.E7Minuscule.finiteTypeCoordinateHopfAlgebraBaseChangeIso R S = TauCeti.FiniteTypeCommHopfAlgCat.baseChangeIsoOfObjIso ⋯ ⋯ (TauCeti.E7Minuscule.coordinateHopfAlgebraBaseChangeIso R S)

@[simp]

theorem TauCeti.E7Minuscule.finiteTypeCoordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (S : Type (max u v)) [CommRing R] [CommRing S] [Algebra R S] : (finiteTypeCoordinateHopfAlgebraBaseChangeIso R S).hom.hom = (CategoryTheory.eqToIso ⋯ ≪≫ coordinateHopfAlgebraBaseChangeIso R S ≪≫ CategoryTheory.eqToIso ⋯).hom

The underlying commutative-Hopf-algebra morphism of the finite-type scalar-extension comparison is the coordinate-Hopf-algebra comparison, with the object equalities made explicit.