Character-cocharacter pairing

Stream: toric

[Yaël Dillies]

I would like to announce that the first phase of Toric is now over: The character-cocharacter pairing of a split torus and the proof that it's perfect are both sorry-free.

[Yaël Dillies]

... ie all the following code is sorry-free:

import Toric

noncomputable section

open AlgebraicGeometry Scheme

/-!
Let `S` be a scheme and `G` be a group scheme over `S`.

We denote the characters of `G` by `X(S, G)` and the cocharacters by `X*(S, G)`.
-/

example {S G : Scheme} [G.Over S] [Grp_Class (G.asOver S)] : Type := X(S, G)
example {S G : Scheme} [G.Over S] [Grp_Class (G.asOver S)] : Type := X*(S, G)

/-!
Let `R` be a domain and `G` be a split torus over `R`.

Then we have a pairing between `X(Spec R, G)` and `X*(Spec R, G)`.

If furthermore `G := 𝔾ₘ[Spec R, σ]` is the explicit torus with finite dimensions given by `σ`,
then this pairing is perfect.
-/

example {R : CommRingCat.{0}} [IsDomain R] {G : Scheme} [G.Over (Spec R)]
    [CommGrp_Class (G.asOver (Spec R))] [IsSplitTorus (Spec R) G] :
    X*(Spec R, G) →ₗ[ℤ] X(Spec R, G) →ₗ[ℤ] ℤ := charPairing R G

example {R : CommRingCat} [IsDomain R] {σ : Type} [Finite σ] :
    (charPairing R 𝔾ₘ[Spec R, σ]).IsPerfPair := isPerfPair_charPairing