Module

Unrigidified.lean

Nyll.AlgebraicCurves.Geometry.Picard.Unrigidified

12 declarations indexed from sourceView source ↗

Module documentation

Line bundles modulo tensoring with a line bundle from the base

This presheaf requires no section of the curve. Choosing a section gives a natural equivalence with the existing rigidified Picard presheaf by normalizing along it. No assertion of the sheaf property is included.

Imports7

Imported by3

def

LineBundle

L44 ↗

AlgebraicGeometry.RelPicard.Unrigidified.LineBundle

Documentation

An actual invertible module on a base change of the curve.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

def LineBundle {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : Type (u + 1)

def

BaseTwist

L48 ↗

AlgebraicGeometry.RelPicard.Unrigidified.BaseTwist

Documentation

Tensoring by the pullback of a base line bundle generates the relative Picard relation.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

def BaseTwist {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M N : LineBundle c t) : Prop

def

Classes

L54 ↗

AlgebraicGeometry.RelPicard.Unrigidified.Classes

Documentation

Relative classes are the quotient by the equivalence relation generated by base twists.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))

Lean source · statement

def Classes {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : Type (u + 1)

theorem

baseTwist_of_iso

L59 ↗

AlgebraicGeometry.RelPicard.Unrigidified.baseTwist_of_iso

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
variable {c}

Lean source · statement

theorem baseTwist_of_iso {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {M N : LineBundle c t} (e : M.1 ≅ N.1) : BaseTwist c t M N

def

pullbackAlong

L66 ↗

AlgebraicGeometry.RelPicard.Unrigidified.pullbackAlong

Documentation

Pull back the actual module, with its existing invertibility proof.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
variable {c}

Lean source · statement

def pullbackAlong {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t)
    (M : LineBundle c t) : LineBundle c t'

theorem

baseTwist_pullback

L72 ↗

AlgebraicGeometry.RelPicard.Unrigidified.baseTwist_pullback

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
variable {c}

Lean source · statement

theorem baseTwist_pullback {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t)
    {M N : LineBundle c t} (h : BaseTwist c t M N) :
    BaseTwist c t' (pullbackAlong ψ M) (pullbackAlong ψ N)

def

classesMap

L86 ↗

AlgebraicGeometry.RelPicard.Unrigidified.classesMap

Documentation

The induced map of relative line-bundle classes.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
variable {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

presheaf

L92 ↗

AlgebraicGeometry.RelPicard.Unrigidified.presheaf

Documentation

The unrigidified relative Picard presheaf, before any sheafification.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
variable {c}

Lean source · full declaration

def presheaf (c : C ⟶ Spec (CommRingCat.of R)) :
    (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type (u + 1) where
  obj X := Classes c X.unop.hom
  map {X Y} φ := TypeCat.ofHom (classesMap
    (c := c) (⟨φ.unop.left, Over.w φ.unop⟩ : SchemeHomOver Y.unop.hom X.unop.hom))
  map_id X := TypeCat.homEquiv.injective (funext fun x => by
    induction x using Quot.ind with
    | _ M =>
      exact Quot.sound (baseTwist_of_iso
        ((Scheme.Modules.pullbackCongr (baseChangeSnd_id c X.unop.hom)).app M.1 ≪≫
          (Scheme.Modules.pullbackId (pullback c X.unop.hom)).app M.1)))
  map_comp {X Y Z} φ ψ := TypeCat.homEquiv.injective (funext fun x => by
    induction x using Quot.ind with
    | _ M =>
      exact Quot.sound (baseTwist_of_iso
        ((Scheme.Modules.pullbackCongr
          (baseChangeSnd_comp c
            (⟨φ.unop.left, Over.w φ.unop⟩ : SchemeHomOver Y.unop.hom X.unop.hom)
            (⟨ψ.unop.left, Over.w ψ.unop⟩ : SchemeHomOver Z.unop.hom Y.unop.hom)).symm).app M.1 ≪≫
          ((Scheme.Modules.pullbackComp _ _).app M.1).symm)))

def

normalize

L116 ↗

AlgebraicGeometry.RelPicard.Unrigidified.normalize

Documentation

Normalize a relative class using the dual of its restriction to the section.

Source context 8 commands

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

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

Lean source · statement

def normalize {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    Classes c t → RigidifiedLineBundle.Classes c ε t

def

forget

L129 ↗

AlgebraicGeometry.RelPicard.Unrigidified.forget

Documentation

Forget rigidification, retaining the relative class of the actual underlying module.

Source context 8 commands

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

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

Lean source · statement

def forget {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    RigidifiedLineBundle.Classes c ε t → Classes c t

def

classesEquiv

L135 ↗

AlgebraicGeometry.RelPicard.Unrigidified.classesEquiv

Documentation

Normalization and forgetting are inverse on actual relative classes.

Source context 8 commands

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

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

Lean source · full declaration

def classesEquiv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    Classes c t ≃ RigidifiedLineBundle.Classes c ε t where
  toFun := normalize ε t
  invFun := forget ε t
  left_inv x := by
    induction x using Quot.ind with
    | _ M =>
      apply Eq.symm
      apply Quot.sound
      refine ⟨rigCorrection ε t M.1, (M.2.pullback (rigSection c t ε)).dual.1, ⟨?_⟩⟩
      exact β_ M.1 ((Scheme.Modules.pullback (pullback.snd c t)).obj (rigCorrection ε t M.1))
  right_inv x := by
    induction x using Quotient.ind with
    | _ M =>
      exact Quotient.sound (RigidifiedLineBundle.nonempty_ofInvertible_iso_of_rigidified M)

def

presheafIso

L152 ↗

AlgebraicGeometry.RelPicard.Unrigidified.presheafIso

Documentation

The normalization equivalence is natural in the test scheme.

Source context 8 commands

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

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

Lean source · statement

def presheafIso :
    presheaf c ≅ relPicardPresheaf c ε

Module documentation

Line bundles modulo tensoring with a line bundle from the base

Declarations