Documentation

TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Tangent.BaseChange

Base change of the special-linear tangent Lie algebra #

The coefficient-valued Lie algebra of SLₙ over R identifies with the Lie algebra of SLₙ over an R-algebra K. Both are the trace-zero matrices over K. tangentCoefficientLieEquiv implements this identification, and tangentBaseChangeLieEquiv_symm_derivationComp proves that it agrees with the canonical coordinate Hopf-algebra base-change isomorphism. Thus it can transport root vectors using their matrix normalization without replacing geometric base change by an unrelated abstract isomorphism. cotangentDualBaseChangeEquiv gives the corresponding scalar-extension comparison of the cotangent dual. No flatness or characteristic assumption is needed.

References #

source
noncomputable def TauCeti.SpecialLinear.tangentCoefficientLieEquiv (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) :
Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) K) ≃ₗ⁅K⁆ Derivation K (↑(coordinateHopfAlgebra K n)) (Bialgebra.CounitAlgebra K (↑(coordinateHopfAlgebra K n)) K)

Coefficient-valued tangent vectors to SLₙ identify with tangent vectors to SLₙ over the coefficient ring, preserving their trace-zero matrices and Lie bracket.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SpecialLinear.tangentMatrix_tangentCoefficientLieEquiv (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) K)) :
    (tangentMatrix n) ((tangentCoefficientLieEquiv R K n) d) = (tangentMatrix n) d

    The tangent comparison leaves the trace-zero matrix unchanged.

    source
    @[simp]
    theorem TauCeti.SpecialLinear.tangentMatrix_tangentCoefficientLieEquiv_symm (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (d : Derivation K (↑(coordinateHopfAlgebra K n)) (Bialgebra.CounitAlgebra K (↑(coordinateHopfAlgebra K n)) K)) :
    (tangentMatrix n) ((tangentCoefficientLieEquiv R K n).symm d) = (tangentMatrix n) d

    The inverse tangent comparison also leaves the trace-zero matrix unchanged.

    source
    noncomputable def TauCeti.SpecialLinear.cotangentDualBaseChangeEquiv (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) :
    TensorProduct R K (Module.Dual R (Bialgebra.CotangentSpace R ↑(coordinateHopfAlgebra R n))) ≃ₗ[K] Module.Dual K (Bialgebra.CotangentSpace K ↑(coordinateHopfAlgebra K n))

    Scalar extension of the special-linear cotangent dual, transported along the canonical coordinate-algebra base-change identification.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.SpecialLinear.cotangentLinearEquiv_cotangentDualBaseChangeEquiv (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (x : TensorProduct R K (Module.Dual R (Bialgebra.CotangentSpace R ↑(coordinateHopfAlgebra R n)))) :
      Derivation.cotangentLinearEquiv ((cotangentDualBaseChangeEquiv R K n) x) = (tangentCoefficientLieEquiv R K n) (Derivation.tangentScalarExtensionEquiv x)

      Cotangent duality turns the cotangent-dual base-change comparison into the coefficient comparison of tangent derivations.

      source
      theorem TauCeti.SpecialLinear.tangentBaseChangeLieEquiv_symm_derivationComp (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (d : Derivation K (↑(coordinateHopfAlgebra K n)) (Bialgebra.CounitAlgebra K (↑(coordinateHopfAlgebra K n)) K)) :
      tangentBaseChangeLieEquiv.symm ((derivationComp (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom)) d) = (tangentCoefficientLieEquiv R K n).symm d

      Restricting a tangent vector along the canonical coordinate base-change isomorphism recovers the coefficient tangent comparison. This certifies its geometric meaning.

      source
      theorem TauCeti.SpecialLinear.derivationComp_tangentCoefficientLieEquiv (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) K)) :
      (derivationComp (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom)) ((tangentCoefficientLieEquiv R K n) d) = tangentBaseChangeLieEquiv d

      The forward tangent comparison intertwines extension of derivations with the canonical coordinate base-change isomorphism.