Module

SplitTorusMu.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SplitTorusMu

14 declarations indexed from sourceView source ↗

Module documentation

Split Torus Mu

Imports4

Mathlib.Algebra.MonoidAlgebra.MapDomain
Mathlib.Algebra.MonoidAlgebra.Basic
Mathlib.Data.ZMod.Basic
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

abbrev

muCoord

L31 ↗

AlgebraicGeometry.SplitTorus.muCoord

Documentation

The group algebra giving coordinates on a product of group schemes of roots of unity.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev muCoord (S : Type u) [CommRing S] (t m : ℕ) : Type u

abbrev

muScheme

L34 ↗

AlgebraicGeometry.SplitTorus.muScheme

Documentation

The affine group scheme with character group Fin t → ZMod m.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev muScheme (S : Type u) [CommRing S] (t m : ℕ) : Scheme.{u}

abbrev

muStr

L38 ↗

AlgebraicGeometry.SplitTorus.muStr

Documentation

The structure morphism of the product of group schemes of roots of unity.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev muStr (S : Type u) [CommRing S] (t m : ℕ) : muScheme S t m ⟶ Spec (CommRingCat.of S)

abbrev

torusCoord

L42 ↗

AlgebraicGeometry.SplitTorus.torusCoord

Documentation

The Laurent group algebra giving coordinates on the split torus.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev torusCoord (S : Type u) [CommRing S] (t : ℕ) : Type u

abbrev

torusScheme

L45 ↗

AlgebraicGeometry.SplitTorus.torusScheme

Documentation

The split torus with character lattice Fin t → ℤ.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev torusScheme (S : Type u) [CommRing S] (t : ℕ) : Scheme.{u}

abbrev

torusStr

L49 ↗

AlgebraicGeometry.SplitTorus.torusStr

Documentation

The structure morphism of the split torus.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev torusStr (S : Type u) [CommRing S] (t : ℕ) : torusScheme S t ⟶ Spec (CommRingCat.of S)

abbrev

muToTorus

L53 ↗

AlgebraicGeometry.SplitTorus.muToTorus

Documentation

The natural morphism from the product of groups of roots of unity into the split torus.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev muToTorus (S : Type u) [CommRing S] (t m : ℕ) : muScheme S t m ⟶ torusScheme S t

abbrev

muIncl

L59 ↗

AlgebraicGeometry.SplitTorus.muIncl

Documentation

The inclusion of groups of roots of unity induced by divisibility of their orders.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev muIncl (S : Type u) [CommRing S] (t : ℕ) {m m' : ℕ} (h : m ∣ m') : muScheme S t m ⟶ muScheme
  S t m'

abbrev

muBaseChange

L66 ↗

AlgebraicGeometry.SplitTorus.muBaseChange

Documentation

The morphism on groups of roots of unity induced by a change of coefficient ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev muBaseChange {S S' : Type u} [CommRing S] [CommRing S'] (φ : S →+* S') (t m : ℕ) :
    muScheme S' t m ⟶ muScheme S t m

abbrev

torusBaseChange

L71 ↗

AlgebraicGeometry.SplitTorus.torusBaseChange

Documentation

The morphism on split tori induced by a change of coefficient ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

abbrev torusBaseChange {S S' : Type u} [CommRing S] [CommRing S'] (φ : S →+* S') (t : ℕ) :
    torusScheme S' t ⟶ torusScheme S t

def

muPt

L79 ↗

AlgebraicGeometry.SplitTorus.muPt

Documentation

The point over an extension algebra defined by an algebra homomorphism from the roots-of-unity coordinate ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

def muPt (S S' : Type u) [CommRing S] [CommRing S'] [Algebra S S'] (t m : ℕ) (χ : muCoord S t m
  →ₐ[S] S') :
    SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap S S'))) (muStr S t m)

def

torusPt

L88 ↗

AlgebraicGeometry.SplitTorus.torusPt

Documentation

The point of the split torus defined by an algebra homomorphism from its coordinate ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

def torusPt (S S' : Type u) [CommRing S] [CommRing S'] [Algebra S S'] (t : ℕ) (χ : torusCoord S t
  →ₐ[S] S') :
    SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap S S'))) (torusStr S t)

def

torusPtId

L100 ↗

AlgebraicGeometry.SplitTorus.torusPtId

Documentation

The point of the split torus over the identity base map defined by a coordinate algebra homomorphism.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

def torusPtId (S : Type u) [CommRing S] (t : ℕ) (χ : torusCoord S t →ₐ[S] S) : SchemeHomOver (𝟙 _)
  (torusStr S t)

def

muPtId

L112 ↗

AlgebraicGeometry.SplitTorus.muPtId

Documentation

The point of the roots-of-unity group over the identity base map defined by a coordinate algebra homomorphism.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.SplitTorus

Lean source · statement

def muPtId (S : Type u) [CommRing S] (t m : ℕ) (χ : muCoord S t m →ₐ[S] S) : SchemeHomOver (𝟙 _)
  (muStr S t m)

Module documentation

Split Torus Mu

Declarations