Module

PicDualNumberDeformationClassSpec.lean

Nyll.JacobianVarieties.Picard.PicDualNumberDeformationClassSpec

4 declarations indexed from sourceView source ↗

Module documentation

Cech classes of dual-number deformations

The overlap unit and compatibility condition specify the Cech class of a rigidified deformation.

Imports7

Mathlib.Algebra.Algebra.Hom
Mathlib.Algebra.DualNumber
Mathlib.LinearAlgebra.Quotient.Defs
Nyll.AlgebraicCurves.Geometry.Deformation.RigKerDualNumber
Nyll.AlgebraicCurves.Geometry.Schemes.TwoAffineOpenCoverH1BaseChange
Nyll.SchemeTheory.Modules.TensorSections
Nyll.JacobianVarieties.Picard.RepresentsRelSubPicKerPoints

Imported by21

abbrev

dualNumberThickening

L43 ↗

AlgebraicGeometry.RelPicard.dualNumberThickening

Documentation

The morphism of base changed covers induced by the inclusion into dual numbers.

Source context 6 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace AlgebraicGeometry.RelPicard
section Thickening
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of R))

Lean source · statement

abbrev dualNumberThickening :
    HomOver (IsScalarTower.toAlgHom R A (DualNumber A)).toRingHom
      (𝒱.pullback c A) (pullback.snd c (specMap R A))
      (𝒱.pullback c (DualNumber A)) (pullback.snd c (specMap R (DualNumber A)))

def

oneAddEpsMul

L50 ↗

AlgebraicGeometry.RelPicard.oneAddEpsMul

Documentation

The overlap unit represented by one plus epsilon times the pulled back section.

Source context 6 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace AlgebraicGeometry.RelPicard
section Thickening
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of R))

Lean source · statement

def oneAddEpsMul (f : ((𝒱.pullback c A).cover (pullback.snd c (specMap R A))).A01) :
    ((𝒱.pullback c (DualNumber A)).cover (pullback.snd c (specMap R (DualNumber A)))).A01

abbrev

H1StructureSheaf

L63 ↗

AlgebraicGeometry.RelPicard.H1StructureSheaf

Documentation

First Cech cohomology of the structure sheaf on the base changed cover.

Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace AlgebraicGeometry.RelPicard
section Spec
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
variable (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙 (Spec (.of R))) c)
variable (A : Type u) [CommRing A] [Algebra R A] (𝒱 : C.TwoAffineOpenCover)

Lean source · statement

abbrev H1StructureSheaf : Type u

def

IsDeformationClassMap

L67 ↗

AlgebraicGeometry.RelPicard.IsDeformationClassMap

Documentation

Compatibility of a rigidified dual-number deformation with its Cech overlap class.

Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry NeronModelInfra
  AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace AlgebraicGeometry.RelPicard
section Spec
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
variable (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙 (Spec (.of R))) c)
variable (A : Type u) [CommRing A] [Algebra R A] (𝒱 : C.TwoAffineOpenCover)

Lean source · statement

def IsDeformationClassMap (δ : RigKerDualNumber c ε A → H1StructureSheaf c A 𝒱) : Prop

Module documentation

Cech classes of dual-number deformations

Declarations

dualNumberThickening

oneAddEpsMul

H1StructureSheaf

IsDeformationClassMap