The lattices of characters and cocharacters

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Char (S G : Scheme) [G.Over S] [Grp_Class (G.asOver S)] : Type u

The characters of the group scheme G over S are the group morphisms G ⟶/S 𝔾ₘ[S].

Equations

• X(S, G) = G.HomGrp 𝔾ₘ[S] S

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Cochar (S G : Scheme) [G.Over S] [Grp_Class (G.asOver S)] : Type u

The cocharacters of the group scheme G over S are the group morphisms 𝔾ₘ[S] ⟶/S G.

Equations

• X*(S, G) = 𝔾ₘ[S].HomGrp G S

def AlgebraicGeometry.Scheme.«termX(_,_)» : Lean.ParserDescr

The characters of the group scheme G over S are the group morphisms G ⟶/S 𝔾ₘ[S].

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.Scheme.«termX*(_,_)» : Lean.ParserDescr

The cocharacters of the group scheme G over S are the group morphisms 𝔾ₘ[S] ⟶/S G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.charPairingAux {S G : Scheme} [G.Over S] [CommGrp_Class (G.asOver S)] : X*(S, G) →+ X(S, G) →+ X(S, 𝔾ₘ[S])

The perfect pairing between characters and cocharacters, valued in the characters of the algebraic torus.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.charPairingAux_apply_apply {S G : Scheme} [G.Over S] [CommGrp_Class (G.asOver S)] (χ : X*(S, G)) (χ' : X(S, G)) : (charPairingAux χ) χ' = HomGrp.comp χ χ'

def AlgebraicGeometry.Scheme.charGrpAlg (R : CommRingCat) [IsDomain ↑R] {G : Type u} [AddCommGroup G] : X(Spec R, (Spec R).Diag G) ≃+ G

Characters of a diagonal group scheme over a domain are exactly the input group.

Note: This is true over a general ring using Cartier duality, but we do not prove that.

Equations

• AlgebraicGeometry.Scheme.charGrpAlg R = AlgebraicGeometry.Scheme.diagHomEquiv.symm.trans (FreeAbelianGroup.liftAddEquiv.symm.trans (AddEquiv.piUnique fun (x : PUnit.{?u.32 + 1}) => G))

theorem AlgebraicGeometry.Scheme.charGrpAlg_symm_apply {R : CommRingCat} [IsDomain ↑R] {G : Type u} [AddCommGroup G] (g : G) : (charGrpAlg R).symm g = (Spec R).diagHomGrp (FreeAbelianGroup.lift fun (x : PUnit.{u + 1}) => g)

theorem AlgebraicGeometry.Scheme.charGrpAlg_apply_diag {R : CommRingCat} [IsDomain ↑R] {G : Type u} [AddCommGroup G] (f : FreeAbelianGroup PUnit.{u + 1} →+ G) : (charGrpAlg R) ((Spec R).diagHomGrp f) = f (FreeAbelianGroup.of 0)

def AlgebraicGeometry.Scheme.cocharGrpAlg (R : CommRingCat) [IsDomain ↑R] {G : Type u} [AddCommGroup G] : X*(Spec R, (Spec R).Diag G) ≃+ (G →+ ℤ)

Cocharacters of a diagonal group scheme over a domain are exactly the dual of the input group.

Note: This is true over a general ring using Cartier duality, but we do not prove that.

Equations

• AlgebraicGeometry.Scheme.cocharGrpAlg R = AlgebraicGeometry.Scheme.diagHomEquiv.symm.trans (AddMonoidHom.postcompAddEquiv (FreeAbelianGroup.punitEquiv PUnit.{?u.27 + 1}))

theorem AlgebraicGeometry.Scheme.cocharGrpAlg_symm_apply {R : CommRingCat} [IsDomain ↑R] {G : Type u} [AddCommGroup G] (g : G →+ ℤ) : (cocharGrpAlg R).symm g = (Spec R).diagHomGrp ((FreeAbelianGroup.punitEquiv PUnit.{u + 1}).symm.toAddMonoidHom.comp g)

def AlgebraicGeometry.Scheme.charTorus {R : CommRingCat} [IsDomain ↑R] {σ : Type u} : X(Spec R, 𝔾ₘ[Spec R, σ]) ≃+ (σ →₀ ℤ)

Characters of the algebraic torus with dimensions σover a domain R are exactly ℤ^σ.

Note: This is true over a general base using Cartier duality, but we do not prove that.

Equations

• AlgebraicGeometry.Scheme.charTorus = (AlgebraicGeometry.Scheme.charGrpAlg R).trans (FreeAbelianGroup.equivFinsupp σ)

def AlgebraicGeometry.Scheme.charTorusUnit {R : CommRingCat} [IsDomain ↑R] : X(Spec R, 𝔾ₘ[Spec R]) ≃+ ℤ

Equations

• AlgebraicGeometry.Scheme.charTorusUnit = (AlgebraicGeometry.Scheme.charGrpAlg R).trans (FreeAbelianGroup.punitEquiv PUnit.{?u.18 + 1})

def AlgebraicGeometry.Scheme.cocharTorus {R : CommRingCat} [IsDomain ↑R] {σ : Type u} : X*(Spec R, 𝔾ₘ[Spec R, σ]) ≃+ (σ → ℤ)

Cocharacters of the algebraic torus with dimensions σover a domain R are exactly ℤ^σ.

Note: This is true over a general base using Cartier duality, but we do not prove that.

Equations

• AlgebraicGeometry.Scheme.cocharTorus = (AlgebraicGeometry.Scheme.cocharGrpAlg R).trans { toEquiv := FreeAbelianGroup.lift.symm, map_add' := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.charPairing (R : CommRingCat) [IsDomain ↑R] (G : Scheme) [G.Over (Spec R)] [CommGrp_Class (G.asOver (Spec R))] : X*(Spec R, G) →ₗ[ℤ] X(Spec R, G) →ₗ[ℤ] ℤ

The ℤ-valued perfect pairing between characters and cocharacters of group schemes over a domain.

Note: This exists over a general base using Cartier duality, but we do not prove that.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.isPerfPair_charPairing {R : CommRingCat} [IsDomain ↑R] {σ : Type u} [Finite σ] : (charPairing R 𝔾ₘ[Spec R, σ]).IsPerfPair