NYLL
Module

RigKerDualNumber.lean

Nyll.AlgebraicCurves.Geometry.Deformation.RigKerDualNumber
11 declarations indexed from sourceView source ↗

Module documentation

Rig Ker Dual Number

Imports9
Imported by16

Declarations

abbrev

dualNumberReduction

L42 ↗
AlgebraicGeometry.RelPicard.dualNumberReduction
Documentation

The Spec morphism induced by projection from dual numbers to the base algebra.

Source context 6 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Thickening
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
abbrev dualNumberReduction : Spec (.of A) ⟶ Spec (.of (DualNumber A))
theorem

dualNumberReduction_comp_specMap

L45 ↗
AlgebraicGeometry.RelPicard.dualNumberReduction_comp_specMap
Source context 6 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Thickening
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem dualNumberReduction_comp_specMap :
    dualNumberReduction R A ≫ Scheme.TwoAffineOpenCover.specMap R (DualNumber A)
      = Scheme.TwoAffineOpenCover.specMap R A
abbrev

dualNumberReductionOver

L55 ↗
AlgebraicGeometry.RelPicard.dualNumberReductionOver
Documentation

The reduction morphism of dual numbers viewed over the original base scheme.

Source context 6 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Thickening
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
abbrev dualNumberReductionOver :
    SchemeHomOver (Scheme.TwoAffineOpenCover.specMap R A) (Scheme.TwoAffineOpenCover.specMap R
      (DualNumber A))
theorem

dualNumberReduction_catches_geometric_points

L60 ↗
AlgebraicGeometry.RelPicard.dualNumberReduction_catches_geometric_points
Source context 6 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Thickening
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
Lean source · statement
theorem dualNumberReduction_catches_geometric_points
    (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (.of k) ⟶ Spec (.of (DualNumber A))) :
    ∃ s₀ : Spec (.of k) ⟶ Spec (.of A), s₀ ≫ dualNumberReduction R A = s
def

Carrier

L92 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.Carrier
Documentation

Rigidified dual number line bundles whose underlying line bundle becomes trivial after reduction.

Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Kernel
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]
Lean source · statement
def RigKerDualNumber.Carrier : Type (u + 1)
instance

setoid

L97 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.setoid
Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Kernel
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]
Lean source · statement
instance RigKerDualNumber.setoid : Setoid (RigKerDualNumber.Carrier c ε A)
def

RigKerDualNumber

L103 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber
Documentation

Classes of rigidified dual number line bundles with trivial underlying reduction.

Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Kernel
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]
Lean source · statement
def RigKerDualNumber : Type (u + 1)
theorem

tensor_mem

L105 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.tensor_mem
Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Kernel
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]
Lean source · statement
theorem RigKerDualNumber.tensor_mem (M N : RigKerDualNumber.Carrier c ε A) :
    Nonempty (((M.1.tensor N.1).pullbackAlong (dualNumberReductionOver R A)).L ≅
      (RigidifiedLineBundle.unit (c := c) (ε := ε) (Scheme.TwoAffineOpenCover.specMap R A)).L)
theorem

unit_mem

L112 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.unit_mem
Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Kernel
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]
Lean source · statement
theorem RigKerDualNumber.unit_mem :
    Nonempty (((RigidifiedLineBundle.unit (c := c) (ε := ε)
        (Scheme.TwoAffineOpenCover.specMap R (DualNumber A))).pullbackAlong
          (dualNumberReductionOver R A)).L ≅
      (RigidifiedLineBundle.unit (c := c) (ε := ε) (Scheme.TwoAffineOpenCover.specMap R A)).L)
def

mul

L121 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.mul
Documentation

Multiplication of dual number kernel classes induced by tensor product of rigidified line bundles.

Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Kernel
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]
Lean source · statement
def RigKerDualNumber.mul : RigKerDualNumber c ε A → RigKerDualNumber c ε A → RigKerDualNumber c ε A
def

one

L127 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.one
Documentation

The dual number kernel class of the unit rigidified line bundle.

Source context 8 commands

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

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra
  GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section Kernel
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]
Lean source · statement
def RigKerDualNumber.one : RigKerDualNumber c ε A

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.