Documentation

TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Weight.Levi.BaseChange

Base change of general-linear weight Levis #

The weight Levi attached to w : Fin N → ℤ commutes with arbitrary extension of the commutative base ring as an affine group scheme. Its coordinate Hopf algebra is the quotient of O(GL_N) by the entries between distinct weight blocks. The general-linear base-change isomorphism preserves those entries, so the quotient comparison preserves the Hopf structure. This permits transporting closed subgroups and their unipotence to the geometric fibre.

The comparison is compatible with the ambient general-linear coordinate maps, and its action on scalar tensors of quotient coordinates is explicit. Repeated weights and rank zero are allowed. The universe restriction on the bundled isomorphism is inherited from coordinateHopfAlgebraBaseChangeIso.

The two opposite weight parabolics impose vanishing of entries in opposite strict weight directions. Together their relations kill exactly the entries between distinct weight blocks, so their intersection is the weight Levi.

References #

source
theorem TauCeti.GeneralLinear.map_baseChangeHopfIdeal_weightLeviDefiningHopfIdeal (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] {N : ℕ} (w : Fin N → ℤ) :
(CommHopfAlgCat.baseChangeHopfIdeal (weightLeviDefiningHopfIdeal R w)).map (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K N).hom) = weightLeviDefiningHopfIdeal K w

The ambient general-linear base-change isomorphism carries the scalar extension of the weight-Levi defining Hopf ideal onto the defining Hopf ideal over the extended base.

source
noncomputable def TauCeti.GeneralLinear.weightLeviCoordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] {N : ℕ} (w : Fin N → ℤ) :
CommHopfAlgCat.baseChange (weightLeviCoordinateHopfAlgebra R w) ≅ weightLeviCoordinateHopfAlgebra K w

Scalar extension of a weight-Levi coordinate Hopf algebra is canonically the weight-Levi coordinate Hopf algebra over the new base.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.GeneralLinear.baseChangeMap_mkQuotient_comp_weightLeviCoordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] {N : ℕ} (w : Fin N → ℤ) :
    CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra R N) (weightLeviDefiningHopfIdeal R w))) (weightLeviCoordinateHopfAlgebraBaseChangeIso R K w).hom = CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K N).hom (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra K N) (weightLeviDefiningHopfIdeal K w))

    The weight-Levi base-change isomorphism commutes with restriction of ambient general-linear coordinates to the Levi.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.weightLeviCoordinateHopfAlgebraBaseChangeIso_hom_tmul_mk (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] {N : ℕ} (w : Fin N → ℤ) (s : K) (x : ↑(coordinateHopfAlgebra R N)) :
    (CategoryTheory.ConcreteCategory.hom (weightLeviCoordinateHopfAlgebraBaseChangeIso R K w).hom) (s ⊗ₜ[R] (Ideal.Quotient.mk (weightLeviDefiningHopfIdeal R w).toIdeal) x) = (Ideal.Quotient.mk (weightLeviDefiningHopfIdeal K w).toIdeal) ((CategoryTheory.ConcreteCategory.hom (coordinateHopfAlgebraBaseChangeIso R K N).hom) (s ⊗ₜ[R] x))

    On a scalar tensor of a quotient coordinate, the Levi comparison is induced by the ambient general-linear comparison.

    source
    @[simp]
    theorem TauCeti.GeneralLinear.weightLeviCoordinateHopfAlgebraBaseChangeIso_inv_mk (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] {N : ℕ} (w : Fin N → ℤ) (s : K) (x : ↑(coordinateHopfAlgebra R N)) :
    (CategoryTheory.ConcreteCategory.hom (weightLeviCoordinateHopfAlgebraBaseChangeIso R K w).inv) ((Ideal.Quotient.mk (weightLeviDefiningHopfIdeal K w).toIdeal) ((CategoryTheory.ConcreteCategory.hom (coordinateHopfAlgebraBaseChangeIso R K N).hom) (s ⊗ₜ[R] x))) = s ⊗ₜ[R] (Ideal.Quotient.mk (weightLeviDefiningHopfIdeal R w).toIdeal) x

    The inverse Levi comparison sends a quotient of an ambient base-changed coordinate back to the corresponding scalar tensor of a quotient coordinate.