The standard algebraic torus

This file defines the standard algebraic torus over Spec R as Spec (R ⊗ ℤ[Fₙ]).

instance AlgebraicGeometry.Scheme.instIsMonHomOverHomAsOverOfAsOver_toric {S M N : Scheme} [M.Over S] [N.Over S] [CategoryTheory.MonObj (M.asOver S)] [CategoryTheory.MonObj (N.asOver S)] (e : M ≅ N) [Hom.IsOver e.hom S] [CategoryTheory.IsMonHom (Hom.asOver e.hom S)] : CategoryTheory.IsMonHom (CategoryTheory.Iso.asOver S e).hom

class AlgebraicGeometry.Scheme.IsSplitTorusOver (G S : Scheme) [G.Over S] [CategoryTheory.GrpObj (G.asOver S)] : Prop

• existsIso : ∃ (A : Type u) (x : AddCommGroup A) (_ : Module.Free ℤ A) (e : G ≅ S.Diag A) (x_2 : Hom.IsOver e.hom S), CategoryTheory.IsMonHom (Hom.asOver e.hom S)

theorem AlgebraicGeometry.Scheme.isSplitTorusOver_iff (G S : Scheme) [G.Over S] [CategoryTheory.GrpObj (G.asOver S)] : G.IsSplitTorusOver S ↔ ∃ (A : Type u) (x : AddCommGroup A) (_ : Module.Free ℤ A) (e : G ≅ S.Diag A) (x_2 : Hom.IsOver e.hom S), CategoryTheory.IsMonHom (Hom.asOver e.hom S)

instance AlgebraicGeometry.Scheme.diag_isSplitTorusOver {S : Scheme} {A : Type u} [AddCommGroup A] [Module.Free ℤ A] : (S.Diag A).IsSplitTorusOver S

theorem AlgebraicGeometry.Scheme.IsSplitTorusOver.of_isIso {G H S : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] [H.IsSplitTorusOver S] (f : G ⟶ H) [CategoryTheory.IsIso f] [Hom.IsOver f S] [CategoryTheory.IsMonHom (Hom.asOver f S)] : G.IsSplitTorusOver S

theorem AlgebraicGeometry.Scheme.IsSplitTorusOver.of_isIso' {G H S : Scheme} [G.Over S] [H.Over S] [CategoryTheory.GrpObj (G.asOver S)] [CategoryTheory.GrpObj (H.asOver S)] [G.IsSplitTorusOver S] (f : G ⟶ H) [CategoryTheory.IsIso f] [Hom.IsOver f S] [CategoryTheory.IsMonHom (Hom.asOver f S)] : H.IsSplitTorusOver S

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

theorem AlgebraicGeometry.Scheme.exists_iso_diag_finite_of_isSplitTorusOver_locallyOfFiniteType (G S : Scheme) [G.Over S] [CategoryTheory.GrpObj (G.asOver S)] [G.IsSplitTorusOver S] [hG : LocallyOfFiniteType (G ↘ S)] [Nonempty ↥S] : ∃ (ι : Type u) (_ : Finite ι) (e : G ≅ S.Diag (AddMonoidAlgebra ℤ ι)) (x : Hom.IsOver e.hom S), CategoryTheory.IsMonHom (Hom.asOver e.hom S)

Every split torus that's locally of finite type is isomorphic to 𝔾ₘⁿ for some n.

class AlgebraicGeometry.Scheme.IsTorusOver (k : Type u) [Field k] (G : Scheme) [G.Over (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.GrpObj (G.asOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] : Prop

• existsSplit : ∃ (L : Type u) (x : Field L) (x_1 : Algebra k L) (_ : Algebra.IsSeparable k L), (CategoryTheory.Limits.pullback (G ↘ Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }) (Spec.map (CommRingCat.ofHom (algebraMap k L)))).IsSplitTorusOver (Spec { carrier := L, commRing := Field.toEuclideanDomain.toCommRing })

theorem AlgebraicGeometry.Scheme.isTorusOver_iff (k : Type u) [Field k] (G : Scheme) [G.Over (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.GrpObj (G.asOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] : IsTorusOver k G ↔ ∃ (L : Type u) (x : Field L) (x_1 : Algebra k L) (_ : Algebra.IsSeparable k L), (CategoryTheory.Limits.pullback (G ↘ Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }) (Spec.map (CommRingCat.ofHom (algebraMap k L)))).IsSplitTorusOver (Spec { carrier := L, commRing := Field.toEuclideanDomain.toCommRing })

instance AlgebraicGeometry.Scheme.instIsTorusOverOfIsSplitTorusOverSpecOf {k : Type u} [Field k] {G : Scheme} [G.Over (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.GrpObj (G.asOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] [G.IsSplitTorusOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] : IsTorusOver k G

theorem AlgebraicGeometry.Scheme.IsTorusOver.of_iso {k : Type u} [Field k] {G H : Scheme} [G.Over (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [H.Over (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.GrpObj (G.asOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] [CategoryTheory.GrpObj (H.asOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] (e : G ≅ H) [Hom.IsOver e.hom (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.IsMonHom (Hom.asOver e.hom (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] [IsTorusOver k H] : IsTorusOver k G

theorem AlgebraicGeometry.Scheme.IsTorusOver.of_isIso {k : Type u} [Field k] {G H : Scheme} [G.Over (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [H.Over (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.GrpObj (G.asOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] [CategoryTheory.GrpObj (H.asOver (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] [IsTorusOver k H] (f : G ⟶ H) [CategoryTheory.IsIso f] [Hom.IsOver f (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing })] [CategoryTheory.IsMonHom (Hom.asOver f (Spec { carrier := k, commRing := Field.toEuclideanDomain.toCommRing }))] : IsTorusOver k G

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.SplitTorus (S : Scheme) (σ : Type u) : Scheme

The (split) algebraic torus over S indexed by σ.

Equations

• 𝔾ₘ[S, σ] = S.Diag (FreeAbelianGroup σ)

def AlgebraicGeometry.Scheme.«term𝔾ₘ[_,_]» : Lean.ParserDescr

The (split) algebraic torus over S indexed by σ.

Equations

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

def AlgebraicGeometry.Scheme.«term𝔾ₘ[_]» : Lean.ParserDescr

The multiplicative group over S.

Equations

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

theorem AlgebraicGeometry.Scheme.exists_iso_splitTorus_of_isSplitTorusOver (G S : Scheme) [G.Over S] [CategoryTheory.GrpObj (G.asOver S)] [G.IsSplitTorusOver S] : ∃ (σ : Type u) (e : G ≅ 𝔾ₘ[S, σ]) (x : Hom.IsOver e.hom S), CategoryTheory.IsMonHom (Hom.asOver e.hom S)

Every split torus that's locally of finite type is isomorphic to 𝔾ₘⁿ for some n.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.splitTorusIso (R : CommRingCat) (σ : Type u_2) : 𝔾ₘ[Spec R, σ] ≅ Spec { carrier := MvLaurentPolynomial σ ↑R, commRing := AddMonoidAlgebra.commRing }

The split torus with dimensions σ over Spec R is isomorphic to Spec R[ℤ^σ].

Equations

• AlgebraicGeometry.Scheme.splitTorusIso R σ = AlgebraicGeometry.Scheme.diagSpecIso R (FreeAbelianGroup σ)