Documentation

Toric.GroupScheme.Character

The lattices of characters and cocharacters #

source
@[reducible, inline]
abbrev AlgebraicGeometry.Scheme.Over.char {S : Scheme} (G : CategoryTheory.Over S) [Grp_Class G] :
Type u_1
Equations
Instances For
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.Scheme.Over.cochar {S : Scheme} (G : CategoryTheory.Over S) [Grp_Class G] :
    Type u_1
    Equations
    Instances For
      source
      def AlgebraicGeometry.Scheme.Over.«termX(_)» :
      Lean.ParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def AlgebraicGeometry.Scheme.Over.charPairing {S : Scheme} {G : CategoryTheory.Over S} [CommGrp_Class G] :
        cochar G →* X(G) →* X(CategoryTheory.Over.mk (S.SplitTorus PUnit.{u_1 + 1} ↘ S))

        The perfect pairing between characters and cocharacters.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def AlgebraicGeometry.Scheme.Over.charPairingInt {S : Scheme} {G : CategoryTheory.Over S} [CommGrp_Class G] :
          X(G) →* cochar G →* ℤ
          Equations
          Instances For