Documentation

TauCeti.Algebra.AlgebraicGroup.SpecialLinear.UpperTriangular.BaseChange

Base change of the upper-triangular Borel of SLₙ #

Scalar extension of the coordinate Hopf algebra of the upper-triangular subgroup of SLₙ is canonically its coordinate Hopf algebra over the new base. The isomorphism commutes with restriction of functions from SLₙ, and the induced point equivalence preserves the upper-triangular determinant-one matrix over every value algebra. In particular, extending the base of the standard Borel does not change its embedding in the special linear group.

No flatness or reducedness assumption on the base extension is needed. The construction uses CommHopfAlgCat.quotientBaseChangeIsoOfMapEq and the existing equality SpecialLinear.UpperTriangular.map_baseChangeHopfIdeal_definingHopfIdeal. The coordinate construction generalizes the rank-two Borel base-change construction in TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Borel.Geometry.

References #

source
noncomputable def TauCeti.SpecialLinear.UpperTriangular.coordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) :
CommHopfAlgCat.baseChange (coordinateHopfAlgebra R n) ≅ coordinateHopfAlgebra K n

Scalar extension of the upper-triangular special-linear coordinate Hopf algebra is canonically the upper-triangular coordinate Hopf algebra over the new base.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.SpecialLinear.UpperTriangular.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (coordinateMap R n)) (coordinateHopfAlgebraBaseChangeIso R K n).hom = CategoryTheory.CategoryStruct.comp (SpecialLinear.coordinateHopfAlgebraBaseChangeIso R K n).hom (coordinateMap K n)

    The Borel base-change isomorphism commutes with restriction of functions from SLₙ. Contravariantly, this identifies the base change of the Borel inclusion with the inclusion constructed over the new base.

    source
    theorem TauCeti.SpecialLinear.UpperTriangular.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom_assoc (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) {Z : CommHopfAlgCat K} (h : coordinateHopfAlgebra K n ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (coordinateMap R n)) (CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K n).hom h) = CategoryTheory.CategoryStruct.comp (SpecialLinear.coordinateHopfAlgebraBaseChangeIso R K n).hom (CategoryTheory.CategoryStruct.comp (coordinateMap K n) h)

    The Borel base-change isomorphism commutes with restriction of functions from SLₙ. Contravariantly, this identifies the base change of the Borel inclusion with the inclusion constructed over the new base.

    source
    theorem TauCeti.SpecialLinear.UpperTriangular.coordinateHopfAlgebraBaseChangeIso_hom_tmul_coordinateMap (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (s : K) (x : ↑(SpecialLinear.coordinateHopfAlgebra R n)) :
    (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom) (s ⊗ₜ[R] (CommHopfAlgCat.Hom.hom (coordinateMap R n)) x) = (CommHopfAlgCat.Hom.hom (coordinateMap K n)) ((CommHopfAlgCat.Hom.hom (SpecialLinear.coordinateHopfAlgebraBaseChangeIso R K n).hom) (s ⊗ₜ[R] x))

    On a pure tensor of a restricted ambient function, the Borel base-change isomorphism is the ambient special-linear base-change isomorphism followed by restriction.

    source
    theorem TauCeti.SpecialLinear.UpperTriangular.pointsMulEquiv_baseChangeIsoPointsMulEquiv (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (A : CommAlgCat K) (q : ↑(HopfAlgebra.points A)) :
    (pointsMulEquiv R n) ((CommHopfAlgCat.baseChangeIsoPointsMulEquiv (coordinateHopfAlgebraBaseChangeIso R K n).symm A) q) = (pointsMulEquiv K n) q

    The canonical Borel base-change point equivalence preserves the upper-triangular determinant-one matrix, over every commutative value algebra.