NYLL
Module

Functor.lean

Nyll.AlgebraicCurves.Geometry.Picard.Functor
16 declarations indexed from sourceView source ↗

Module documentation

The relative Picard presheaf

This file defines invertible sheaves of modules and line bundles rigidified along a chosen section. Isomorphism classes of rigidified line bundles form a presheaf under base change, with the unit bundle as its distinguished class.

Imports4
Imported by523

Declarations

def

baseChangeSnd

L41 ↗
AlgebraicGeometry.RelPicard.baseChangeSnd
Documentation

The map between base changes induced by a morphism of schemes over the base.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · statement
def baseChangeSnd {C T T' : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (s : SchemeHomOver t' t) : pullback c t' ⟶ pullback c t
def

rigSection

L48 ↗
AlgebraicGeometry.RelPicard.rigSection
Documentation

The section of a base change induced by the chosen section of the original family.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · statement
def rigSection {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (t : T ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    T ⟶ pullback c t
def

postComp

L54 ↗
AlgebraicGeometry.RelPicard.postComp
Documentation

Composition of morphisms of schemes over the fixed affine base.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · statement
def postComp {X X' T' : Scheme.{u}} {x : X ⟶ Spec (CommRingCat.of R)}
    {x' : X' ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (φ : SchemeHomOver x x') (ψ : SchemeHomOver t' x) : SchemeHomOver t' x'
theorem

baseChangeSnd_id

L59 ↗
AlgebraicGeometry.RelPicard.baseChangeSnd_id
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · statement
theorem baseChangeSnd_id {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (t : T ⟶ Spec (CommRingCat.of R)) :
    baseChangeSnd c (⟨𝟙 T, Category.id_comp t⟩ : SchemeHomOver t t) = 𝟙 (pullback c t)
theorem

baseChangeSnd_comp

L64 ↗
AlgebraicGeometry.RelPicard.baseChangeSnd_comp
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · statement
theorem baseChangeSnd_comp {C X X' T' : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {x : X ⟶ Spec (CommRingCat.of R)} {x' : X' ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (φ : SchemeHomOver x x') (ψ : SchemeHomOver t' x) :
    baseChangeSnd c ψ ≫ baseChangeSnd c φ = baseChangeSnd c (postComp φ ψ)
theorem

rigSection_baseChangeSnd

L73 ↗
AlgebraicGeometry.RelPicard.rigSection_baseChangeSnd
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · statement
theorem rigSection_baseChangeSnd {C T T' : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (g : SchemeHomOver t' t) :
    rigSection c t' ε ≫ baseChangeSnd c g = g.1 ≫ rigSection c t ε
structure

RigidifiedLineBundle

L85 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle
Documentation

An invertible module on a base changed family, trivialized along its chosen section.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · full declaration
structure RigidifiedLineBundle {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : Type (u + 1) where
  /-- The underlying sheaf of modules on the base changed family. -/
  L : (pullback c t).Modules
  /-- The underlying module is locally free of rank one. -/
  isInvertible : Scheme.Modules.IsInvertible L
  /-- The pullback along the chosen section is isomorphic to the unit module. -/
  rigidified : Nonempty ((Scheme.Modules.pullback (rigSection c t ε)).obj L ≅
    SheafOfModules.unit T.ringCatSheaf)
def

unit

L102 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.unit
Documentation

The unit line bundle with its canonical rigidification.

Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
namespace RigidifiedLineBundle
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
Lean source · full declaration
def unit {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : RigidifiedLineBundle c ε t where
  L := SheafOfModules.unit (pullback c t).ringCatSheaf
  isInvertible := Scheme.Modules.isInvertible_unit _
  rigidified := ⟨Scheme.Modules.pullbackUnitIso _⟩
instance

(anonymous instance)

L107 ↗
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
namespace RigidifiedLineBundle
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
Lean source · statement
instance {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    Inhabited (RigidifiedLineBundle c ε t)
def

pullbackAlong

L111 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.pullbackAlong
Documentation

Pullback of a rigidified line bundle along a morphism over the base.

Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
namespace RigidifiedLineBundle
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
Lean source · full declaration
def pullbackAlong {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (M : RigidifiedLineBundle c ε t)
    (ψ : SchemeHomOver t' t) : RigidifiedLineBundle c ε t' where
  L := (Scheme.Modules.pullback (baseChangeSnd c ψ)).obj M.L
  isInvertible := M.isInvertible.pullback _
  rigidified := ⟨(Scheme.Modules.pullbackComp _ _).app M.L ≪≫
    (Scheme.Modules.pullbackCongr (rigSection_baseChangeSnd c ε ψ)).app M.L ≪≫
    ((Scheme.Modules.pullbackComp _ _).app M.L).symm ≪≫
    (Scheme.Modules.pullback ψ.1).mapIso M.rigidified.some ≪≫
    Scheme.Modules.pullbackUnitIso ψ.1⟩
instance

setoid

L122 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.setoid
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
namespace RigidifiedLineBundle
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
Lean source · full declaration
instance setoid {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    Setoid (RigidifiedLineBundle c ε t) where
  r M M' := Nonempty (M.L ≅ M'.L)
  iseqv := ⟨fun _ => ⟨Iso.refl _⟩, fun ⟨i⟩ => ⟨i.symm⟩, fun ⟨i⟩ ⟨j⟩ => ⟨i ≪≫ j⟩⟩
theorem

pullbackAlong_congr

L127 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.pullbackAlong_congr
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
namespace RigidifiedLineBundle
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
Lean source · statement
theorem pullbackAlong_congr {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} {M M' : RigidifiedLineBundle c ε t}
    (ψ : SchemeHomOver t' t) (h : Nonempty (M.L ≅ M'.L)) :
    Nonempty ((M.pullbackAlong ψ).L ≅ (M'.pullbackAlong ψ).L)
def

Classes

L134 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.Classes
Documentation

Isomorphism classes of rigidified line bundles, using the underlying module isomorphism.

Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
namespace RigidifiedLineBundle
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
Lean source · statement
def Classes (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : Type (u + 1)
def

classesMap

L139 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.classesMap
Documentation

The map on line bundle classes induced by base change.

Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
namespace RigidifiedLineBundle
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
Lean source · statement
def classesMap {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    Classes c ε t → Classes c ε t'
def

relPicardPresheaf

L147 ↗
AlgebraicGeometry.RelPicard.relPicardPresheaf
Documentation

The presheaf of rigidified line bundle classes on schemes over the affine base.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · full declaration
def relPicardPresheaf {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type (u + 1) where
  obj X := RigidifiedLineBundle.Classes c ε X.unop.hom
  map {X X'} φ := TypeCat.ofHom
    (RigidifiedLineBundle.classesMap (c := c) (ε := ε)
      (⟨φ.unop.left, Over.w φ.unop⟩ : SchemeHomOver X'.unop.hom X.unop.hom))
  map_id X := TypeCat.homEquiv.injective (funext fun x => by
    induction x using Quotient.ind with
    | _ M =>
      exact Quotient.sound
        ⟨(Scheme.Modules.pullbackCongr (baseChangeSnd_id c X.unop.hom)).app M.L ≪≫
          (Scheme.Modules.pullbackId (pullback c X.unop.hom)).app M.L⟩)
  map_comp {X X' X''} φ χ := TypeCat.homEquiv.injective (funext fun x => by
    induction x using Quotient.ind with
    | _ M =>
      exact Quotient.sound
        ⟨(Scheme.Modules.pullbackCongr
            (baseChangeSnd_comp c
              (⟨φ.unop.left, Over.w φ.unop⟩ : SchemeHomOver X'.unop.hom X.unop.hom)
              (⟨χ.unop.left, Over.w χ.unop⟩ :
                SchemeHomOver X''.unop.hom X'.unop.hom)).symm).app M.L ≪≫
          ((Scheme.Modules.pullbackComp _ _).app M.L).symm⟩)
def

unitClass

L172 ↗
AlgebraicGeometry.RelPicard.relPicardPresheaf.unitClass
Documentation

The class of the unit line bundle in the relative Picard presheaf.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R]
Lean source · statement
def relPicardPresheaf.unitClass {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (X : Over (Spec (CommRingCat.of R))) :
    (relPicardPresheaf c ε).obj (Opposite.op X)

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