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
        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] :
          X*(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) →* X(G) →* ℤ
            Equations
            Instances For