The lattices of characters and cocharacters

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Char (S G : Scheme) [G.Over S] [CategoryTheory.GrpObj (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] [CategoryTheory.GrpObj (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.

def AlgebraicGeometry.Scheme.charCongr (S : Scheme) {G H : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] (e : G ≅ H) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : X(S, G) ≃+ X(S, H)

Characters of isomorphic group schemes are isomorphic.

Equations

• S.charCongr e = AlgebraicGeometry.Scheme.HomGrp.congr e (CategoryTheory.Iso.refl 𝔾ₘ[S])

@[simp]

theorem AlgebraicGeometry.Scheme.charCongr_symm {S G H : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] (e : G ≅ H) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : (S.charCongr e).symm = S.charCongr e.symm

def AlgebraicGeometry.Scheme.cocharCongr (S : Scheme) {G H : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] [CategoryTheory.IsCommMonObj (G.asOver S)] [CategoryTheory.IsCommMonObj (H.asOver S)] (e : G ≅ H) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : X*(S, G) ≃+ X*(S, H)

Cocharacters of isomorphic commutative group schemes are isomorphic.

Equations

• S.cocharCongr e = AlgebraicGeometry.Scheme.HomGrp.congr (CategoryTheory.Iso.refl 𝔾ₘ[S]) e

@[simp]

theorem AlgebraicGeometry.Scheme.cocharCongr_symm {S G H : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] (e : G ≅ H) [CategoryTheory.IsCommMonObj (G.asOver S)] [CategoryTheory.IsCommMonObj (H.asOver S)] [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : (S.cocharCongr e).symm = S.cocharCongr e.symm

@[simp]

theorem AlgebraicGeometry.Scheme.cocharCongr_comp_charCongr {S G H : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] [CategoryTheory.IsCommMonObj (G.asOver S)] [CategoryTheory.IsCommMonObj (H.asOver S)] (e : G ≅ H) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] (a : X*(S, G)) (b : X(S, G)) : HomGrp.comp ((S.cocharCongr e) a) ((S.charCongr e) b) = HomGrp.comp a b

noncomputable def AlgebraicGeometry.Scheme.charPairingAux {S G : Scheme} [G.Over S] [CategoryTheory.CommGrpObj (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] [CategoryTheory.CommGrpObj (G.asOver S)] (χ : X*(S, G)) (χ' : X(S, G)) : (charPairingAux χ) χ' = HomGrp.comp χ χ'

def AlgebraicGeometry.Scheme.charDiag (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 base using Cartier duality, but we do not prove that.

Equations

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

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

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

def AlgebraicGeometry.Scheme.cocharDiag (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 base using Cartier duality, but we do not prove that.

Equations

• AlgebraicGeometry.Scheme.cocharDiag R G = AlgebraicGeometry.Scheme.diagHomEquiv.symm.trans (FreeAbelianGroup.uniqueEquiv PUnit.{?u.27 + 1}).addMonoidHomCongrRight

theorem AlgebraicGeometry.Scheme.cocharDiag_symm_apply {R : CommRingCat} [IsDomain ↑R] {G : Type u} [AddCommGroup G] (g : G →+ ℤ) : (cocharDiag R G).symm g = (Spec R).diagHomGrp ((FreeAbelianGroup.uniqueEquiv 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 R σ = (AlgebraicGeometry.Scheme.charDiag R (FreeAbelianGroup σ)).trans (FreeAbelianGroup.equivFinsupp σ)

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

Equations

• AlgebraicGeometry.Scheme.charTorusUnit R = (AlgebraicGeometry.Scheme.charDiag R (FreeAbelianGroup PUnit.{?u.18 + 1})).trans (FreeAbelianGroup.uniqueEquiv 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 R σ = (AlgebraicGeometry.Scheme.cocharDiag R (FreeAbelianGroup σ)).trans { toEquiv := FreeAbelianGroup.lift.symm, map_add' := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.charPairing (R : CommRingCat) [IsDomain ↑R] (G : Scheme) [G.Over (Spec R)] [CategoryTheory.CommGrpObj (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] {T : Scheme} [T.Over (Spec R)] [CategoryTheory.CommGrpObj (T.asOver (Spec R))] [T.IsSplitTorusOver (Spec { carrier := ↑R, commRing := R.commRing })] [LocallyOfFiniteType (T ↘ Spec { carrier := ↑R, commRing := R.commRing })] : (charPairing R T).IsPerfPair