Module

SquareZeroDeformation.lean

Nyll.AlgebraicCurves.Geometry.Deformation.SquareZeroDeformation

23 declarations indexed from sourceView source ↗

Module documentation

Square Zero Deformation

Imports1

Nyll.AlgebraicCurves.Geometry.Picard.Functor

Imported by4

instance

isLocalRing

L32 ↗

AlgebraicGeometry.SquareZero.isLocalRing

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

instance isLocalRing : IsLocalRing (TrivSqZeroExt K V)

instance

isLocalRing'

L42 ↗

AlgebraicGeometry.SquareZero.isLocalRing'

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

instance isLocalRing' : IsLocalRing (CommRingCat.of (TrivSqZeroExt K V))

abbrev

spec

L46 ↗

AlgebraicGeometry.SquareZero.spec

Documentation

The spectrum of the trivial square-zero extension of K by V.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

abbrev spec : Scheme.{u}

def

toBase

L49 ↗

AlgebraicGeometry.SquareZero.toBase

Documentation

The structure morphism of the square-zero spectrum to the spectrum of K.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

def toBase : spec K V ⟶ Spec (CommRingCat.of K)

def

basePoint

L53 ↗

AlgebraicGeometry.SquareZero.basePoint

Documentation

The closed base point induced by the projection of the square-zero extension onto K.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

def basePoint : Spec (CommRingCat.of K) ⟶ spec K V

theorem

basePoint_toBase

L56 ↗

AlgebraicGeometry.SquareZero.basePoint_toBase

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

theorem basePoint_toBase : basePoint K V ≫ toBase K V = 𝟙 _

def

basePointOver

L61 ↗

AlgebraicGeometry.SquareZero.basePointOver

Documentation

The base point regarded as a morphism over the spectrum of K.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

def basePointOver : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) (toBase K V)

theorem

basePointOver_coe

L64 ↗

AlgebraicGeometry.SquareZero.basePointOver_coe

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]

Lean source · statement

theorem basePointOver_coe : (basePointOver K V).1 = basePoint K V

def

specMap

L71 ↗

AlgebraicGeometry.SquareZero.specMap

Documentation

The scheme morphism induced contravariantly by a linear map of square-zero modules.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {W' : Type u} [AddCommGroup W'] [Module K W'] [Module Kᵐᵒᵖ W'] [IsCentralScalar K W']

Lean source · statement

def specMap (φ : V →ₗ[K] W) : spec K W ⟶ spec K V

theorem

specMap_toBase

L74 ↗

AlgebraicGeometry.SquareZero.specMap_toBase

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {W' : Type u} [AddCommGroup W'] [Module K W'] [Module Kᵐᵒᵖ W'] [IsCentralScalar K W']

Lean source · statement

theorem specMap_toBase (φ : V →ₗ[K] W) : specMap K φ ≫ toBase K V = toBase K W

theorem

basePoint_specMap

L81 ↗

AlgebraicGeometry.SquareZero.basePoint_specMap

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {W' : Type u} [AddCommGroup W'] [Module K W'] [Module Kᵐᵒᵖ W'] [IsCentralScalar K W']

Lean source · statement

theorem basePoint_specMap (φ : V →ₗ[K] W) : basePoint K W ≫ specMap K φ = basePoint K V

theorem

specMap_id

L88 ↗

AlgebraicGeometry.SquareZero.specMap_id

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {W' : Type u} [AddCommGroup W'] [Module K W'] [Module Kᵐᵒᵖ W'] [IsCentralScalar K W']

Lean source · statement

theorem specMap_id : specMap K (LinearMap.id : V →ₗ[K] V) = 𝟙 _

theorem

specMap_comp

L92 ↗

AlgebraicGeometry.SquareZero.specMap_comp

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {W' : Type u} [AddCommGroup W'] [Module K W'] [Module Kᵐᵒᵖ W'] [IsCentralScalar K W']

Lean source · statement

theorem specMap_comp (φ : V →ₗ[K] W) (ψ : W →ₗ[K] W') :
    specMap K (ψ ∘ₗ φ) = specMap K ψ ≫ specMap K φ

def

specMapOver

L98 ↗

AlgebraicGeometry.SquareZero.specMapOver

Documentation

The morphism of square-zero spectra induced by a linear map, viewed over the base.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {W' : Type u} [AddCommGroup W'] [Module K W'] [Module Kᵐᵒᵖ W'] [IsCentralScalar K W']

Lean source · statement

def specMapOver (φ : V →ₗ[K] W) : SchemeHomOver (toBase K W) (toBase K V)

theorem

specMapOver_coe

L101 ↗

AlgebraicGeometry.SquareZero.specMapOver_coe

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace SquareZero
variable (K : Type u) [Field K]
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {V}
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
variable {W' : Type u} [AddCommGroup W'] [Module K W'] [Module Kᵐᵒᵖ W'] [IsCentralScalar K W']

Lean source · statement

theorem specMapOver_coe (φ : V →ₗ[K] W) : (specMapOver K φ).1 = specMap K φ

def

TangentPoints

L110 ↗

AlgebraicGeometry.TangentPoints

Documentation

Maps from the square-zero spectrum that lie over the base and reduce to the specified point.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
section TangentPoints
variable {K : Type u} [Field K] {X : Scheme.{u}}

Lean source · statement

def TangentPoints (x : X ⟶ Spec (CommRingCat.of K)) (pt : Spec (CommRingCat.of K) ⟶ X)
    (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V] : Type u

theorem

ext

L121 ↗

AlgebraicGeometry.TangentPoints.ext

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
section TangentPoints
variable {K : Type u} [Field K] {X : Scheme.{u}}
namespace TangentPoints
variable {x : X ⟶ Spec (CommRingCat.of K)} {pt : Spec (CommRingCat.of K) ⟶ X}
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem ext {v v' : TangentPoints x pt V} (h : v.1 = v'.1) : v = v'

def

map

L124 ↗

AlgebraicGeometry.TangentPoints.map

Documentation

Transport a tangent point along a linear map of the square-zero modules.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
section TangentPoints
variable {K : Type u} [Field K] {X : Scheme.{u}}
namespace TangentPoints
variable {x : X ⟶ Spec (CommRingCat.of K)} {pt : Spec (CommRingCat.of K) ⟶ X}
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

def map (φ : V →ₗ[K] W) (v : TangentPoints x pt V) : TangentPoints x pt W

theorem

map_coe

L128 ↗

AlgebraicGeometry.TangentPoints.map_coe

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
section TangentPoints
variable {K : Type u} [Field K] {X : Scheme.{u}}
namespace TangentPoints
variable {x : X ⟶ Spec (CommRingCat.of K)} {pt : Spec (CommRingCat.of K) ⟶ X}
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem map_coe (φ : V →ₗ[K] W) (v : TangentPoints x pt V) :
    (v.map φ).1 = SquareZero.specMap K φ ≫ v.1

def

TrivialModDeformations

L140 ↗

AlgebraicGeometry.RelPicard.TrivialModDeformations

Documentation

Rigidified line bundles over the square-zero spectrum whose special fibre is trivial.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace RelPicard
variable {K : Type u} [Field K] {C : Scheme.{u}}

Lean source · statement

def TrivialModDeformations (c : C ⟶ Spec (CommRingCat.of K))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
    (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V] : Type (u + 1)

theorem

postComp_specMapOver_basePointOver

L154 ↗

AlgebraicGeometry.RelPicard.TrivialModDeformations.postComp_specMapOver_basePointOver

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace RelPicard
variable {K : Type u} [Field K] {C : Scheme.{u}}
namespace TrivialModDeformations
variable {c : C ⟶ Spec (CommRingCat.of K)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c}
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem postComp_specMapOver_basePointOver (φ : V →ₗ[K] W) :
    postComp (SquareZero.specMapOver K φ) (SquareZero.basePointOver K W) = SquareZero.basePointOver
      K V

def

map

L160 ↗

AlgebraicGeometry.RelPicard.TrivialModDeformations.map

Documentation

Pull a deformation back along the morphism induced by a linear map of square-zero modules.

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace RelPicard
variable {K : Type u} [Field K] {C : Scheme.{u}}
namespace TrivialModDeformations
variable {c : C ⟶ Spec (CommRingCat.of K)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c}
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

def map (φ : V →ₗ[K] W) (L : TrivialModDeformations c ε V) : TrivialModDeformations c ε W

theorem

map_coe

L168 ↗

AlgebraicGeometry.RelPicard.TrivialModDeformations.map_coe

Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TrivSqZeroExt NeronModelInfra
namespace AlgebraicGeometry
namespace RelPicard
variable {K : Type u} [Field K] {C : Scheme.{u}}
namespace TrivialModDeformations
variable {c : C ⟶ Spec (CommRingCat.of K)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c}
variable {V : Type u} [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable {W : Type u} [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]

Lean source · statement

theorem map_coe (φ : V →ₗ[K] W) (L : TrivialModDeformations c ε V) :
    (L.map φ).1 = L.1.pullbackAlong (SquareZero.specMapOver K φ)

Module documentation

Square Zero Deformation

Declarations