NYLL
Module

AbelJacobiFamily.lean

Nyll.JacobianVarieties.Picard.AbelJacobiFamily
19 declarations indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Construct the Abel–Jacobi family from the line bundle defined by a moving point and the fixed basepoint.

Imports12
Imported by30

Declarations

def

toProdSpec

L46 ↗
AlgebraicGeometry.RelPicard.toProdSpec
Documentation

The canonical map to the pullback of the structure morphism along the identity.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
Lean source · statement
def toProdSpec : A ⟶ Limits.pullback a (𝟙 (Spec (CommRingCat.of k)))
theorem

toProdSpec_fst

L50 ↗
AlgebraicGeometry.RelPicard.toProdSpec_fst
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem toProdSpec_fst : toProdSpec a ≫ pullback.fst a (𝟙 _) = 𝟙 A
theorem

fst_toProdSpec

L53 ↗
AlgebraicGeometry.RelPicard.fst_toProdSpec
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem fst_toProdSpec : pullback.fst a (𝟙 _) ≫ toProdSpec a = 𝟙 _
def

fstPullbackToProdSpecPullbackIso

L60 ↗
AlgebraicGeometry.RelPicard.fstPullbackToProdSpecPullbackIso
Documentation

Pulling a module along the canonical map and then the first projection recovers it.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
Lean source · statement
def fstPullbackToProdSpecPullbackIso (N : (Limits.pullback a (𝟙 (Spec
  (CommRingCat.of k)))).Modules) :
    (Scheme.Modules.pullback (pullback.fst a (𝟙 _))).obj ((Scheme.Modules.pullback
      (toProdSpec a)).obj N) ≅ N
def

toProdSpecPullbackFstPullbackIso

L69 ↗
AlgebraicGeometry.RelPicard.toProdSpecPullbackFstPullbackIso
Documentation

Pulling a module along the first projection and then the canonical map recovers it.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
Lean source · statement
def toProdSpecPullbackFstPullbackIso (L : A.Modules) :
    (Scheme.Modules.pullback (toProdSpec a)).obj ((Scheme.Modules.pullback (pullback.fst a
      (𝟙 _))).obj L) ≅ L
theorem

baseChangeSnd_eq_mapOnProdOver

L78 ↗
AlgebraicGeometry.RelPicard.baseChangeSnd_eq_mapOnProdOver
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
Lean source · statement
theorem baseChangeSnd_eq_mapOnProdOver {T' : Scheme.{u}} {h : T' ⟶ Spec (CommRingCat.of k)}
    (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) h) : baseChangeSnd a t =
      mapOnProdOver a t.1 t.2
theorem

tensorUnit

L82 ↗
AlgebraicGeometry.RelPicard.IsAlgEquivZero.tensorUnit
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
Lean source · statement
theorem IsAlgEquivZero.tensorUnit (a : A ⟶ Spec (CommRingCat.of k)) : IsAlgEquivZero a
  (𝟙_ A.Modules)
theorem

of_fst_pullback_iso

L91 ↗
AlgebraicGeometry.RelPicard.IsAlgEquivZero.of_fst_pullback_iso
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
Lean source · statement
theorem IsAlgEquivZero.of_fst_pullback_iso {L : A.Modules}
    {N : (Limits.pullback a (𝟙 (Spec (CommRingCat.of k)))).Modules}
    (e : (Scheme.Modules.pullback (pullback.fst a (𝟙 _))).obj L ≅ N)
    (hN : IsAlgEquivZero a ((Scheme.Modules.pullback (toProdSpec a)).obj N)) : IsAlgEquivZero a L
theorem

ofPoint_congr

L98 ↗
AlgebraicGeometry.RelPicard.RelEffCartierDiv.ofPoint_congr
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
Lean source · statement
theorem RelEffCartierDiv.ofPoint_congr {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) [IsSeparated f] {T :
  Scheme.{u}}
    {g : T ⟶ S} {x y : T ⟶ 𝒞} (h : x = y) (hx : x ≫ f = g) (hy : y ≫ f = g) :
    RelEffCartierDiv.ofPoint f x hx = RelEffCartierDiv.ofPoint f y hy
theorem

nonempty_invModule_tensor_module_iso

L104 ↗
AlgebraicGeometry.RelPicard.Scheme.IdealSheafData.IsInvertible.nonempty_invModule_tensor_module_iso
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
Lean source · statement
theorem Scheme.IdealSheafData.IsInvertible.nonempty_invModule_tensor_module_iso {X : Scheme.{u}}
    {I : X.IdealSheafData} (hI : I.IsInvertible) : Nonempty
      (I.invModule ⊗ I.module ≅ 𝟙_ X.Modules)
abbrev

pointSubBasepointModule

L113 ↗
AlgebraicGeometry.RelPicard.pointSubBasepointModule
Documentation

The line module of a point tensored with the ideal module of the base point.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · statement
abbrev pointSubBasepointModule (t ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) :
    (Limits.pullback a (𝟙 (Spec (CommRingCat.of k)))).Modules
def

pointsSubBasepointModule

L118 ↗
AlgebraicGeometry.RelPicard.pointsSubBasepointModule
Documentation

The tensor product of the point-minus-base-point modules associated to a list of points.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · full declaration
def pointsSubBasepointModule (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) :
    List (SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) → (Limits.pullback a (𝟙 (Spec
      (CommRingCat.of k)))).Modules
  | [] => 𝟙_ _
  | P :: Ps => pointSubBasepointModule (a := a) P ε ⊗ pointsSubBasepointModule ε Ps
theorem

pointsSubBasepointModule_nil

L124 ↗
AlgebraicGeometry.RelPicard.pointsSubBasepointModule_nil
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · statement
theorem pointsSubBasepointModule_nil (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) :
    pointsSubBasepointModule (a := a) ε [] = 𝟙_ _
theorem

pointsSubBasepointModule_cons

L127 ↗
AlgebraicGeometry.RelPicard.pointsSubBasepointModule_cons
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · statement
theorem pointsSubBasepointModule_cons (ε P : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a)
    (Ps : List (SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a)) :
    pointsSubBasepointModule (a := a) ε (P :: Ps) = pointSubBasepointModule (a :=
      a) P ε ⊗ pointsSubBasepointModule ε Ps
abbrev

diagDiv

L134 ↗
AlgebraicGeometry.RelPicard.diagDiv
Documentation

The relative effective Cartier divisor defined by the diagonal section.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · statement
abbrev diagDiv : RelEffCartierDiv a 1 a
theorem

comp_point_comp

L137 ↗
AlgebraicGeometry.RelPicard.comp_point_comp
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
omit [IsSeparated a] in
Lean source · statement
theorem comp_point_comp (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) : (a ≫ ε.1) ≫ a =
  a
abbrev

constDiv

L142 ↗
AlgebraicGeometry.RelPicard.constDiv
Documentation

The relative effective Cartier divisor defined by the constant base-point section.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · statement
abbrev constDiv (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) : RelEffCartierDiv a 1 a
def

ajFamily

L147 ↗
AlgebraicGeometry.RelPicard.ajFamily
Documentation

The Abel–Jacobi family obtained from the diagonal divisor and the constant base-point divisor.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · statement
def ajFamily (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) a) : (Limits.pullback a a).Modules
theorem

isInvertible_ajFamily

L150 ↗
AlgebraicGeometry.RelPicard.isInvertible_ajFamily
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {k : Type u} [Field k] {A : Scheme.{u}} (a : A ⟶ Spec (CommRingCat.of k))
variable {a}
section
variable [IsSeparated a]
Lean source · statement
theorem isInvertible_ajFamily [SmoothOfRelativeDimension 1 a] (ε : SchemeHomOver (𝟙 (Spec
  (CommRingCat.of k))) a) :
    Scheme.Modules.IsInvertible (ajFamily (a := a) ε)

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