Module

UnrigidifiedAlgEquivZero.lean

Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedAlgEquivZero

10 declarations indexed from sourceView source ↗

Module documentation

The unrigidified degree-zero Picard presheaf

The geometric-fibre condition is invariant under tensoring with a base line bundle. It therefore defines an actual subfunctor of relative classes. At a chosen section, normalization identifies this subfunctor with the existing pointed Picard-zero functor.

Imports7

Imported by5

def

FibrewiseZero

L44 ↗

AlgebraicGeometry.RelPicard.Unrigidified.FibrewiseZero

Documentation

Algebraic equivalence to zero on all geometric fibres, without a rigidifying section.

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 FibrewiseZero {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : LineBundle c t) : Prop

theorem

fibrewiseZero_baseTwist_iff

L50 ↗

AlgebraicGeometry.RelPicard.Unrigidified.fibrewiseZero_baseTwist_iff

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

theorem fibrewiseZero_baseTwist_iff {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {M N : LineBundle c t} (h : BaseTwist c t M N) : FibrewiseZero M ↔ FibrewiseZero N

theorem

fibrewiseZero_pullback

L78 ↗

AlgebraicGeometry.RelPicard.Unrigidified.fibrewiseZero_pullback

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

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

def

classesZero

L98 ↗

AlgebraicGeometry.RelPicard.Unrigidified.classesZero

Documentation

The fibrewise zero condition descends to actual relative classes.

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 classesZero {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    Classes c t → Prop

theorem

classesZero_map

L102 ↗

AlgebraicGeometry.RelPicard.Unrigidified.classesZero_map

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

theorem classesZero_map {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t)
    (x : Classes c t) (hx : classesZero t x) : classesZero t' (classesMap ψ x)

def

zeroSubfunctor

L109 ↗

AlgebraicGeometry.RelPicard.Unrigidified.zeroSubfunctor

Documentation

The actual subfunctor of fibrewise algebraically trivial relative classes.

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 · full declaration

def zeroSubfunctor (c : C ⟶ Spec (CommRingCat.of R)) : Subfunctor (presheaf c) where
  obj X := {x | classesZero X.unop.hom x}
  map φ := fun x hx => classesZero_map ⟨φ.unop.left, Over.w φ.unop⟩ x hx

def

zeroPresheaf

L114 ↗

AlgebraicGeometry.RelPicard.Unrigidified.zeroPresheaf

Documentation

The unrigidified Picard-zero presheaf.

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 zeroPresheaf (c : C ⟶ Spec (CommRingCat.of R)) :
    (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type (u + 1)

theorem

normalize_zero_iff

L118 ↗

AlgebraicGeometry.RelPicard.Unrigidified.normalize_zero_iff

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

theorem normalize_zero_iff
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x : Classes c t) :
    classesZero t x ↔ (algEquivZeroCut c ε).onClasses t (normalize ε t x)

def

zeroClassesEquiv

L131 ↗

AlgebraicGeometry.RelPicard.Unrigidified.zeroClassesEquiv

Documentation

Normalization restricts to the fibrewise-zero classes.

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 · full declaration

def zeroClassesEquiv (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    {x : Classes c t // classesZero t x} ≃
      {x : RigidifiedLineBundle.Classes c ε t // (algEquivZeroCut c ε).onClasses t x} where
  toFun x := ⟨classesEquiv ε t x.1, (normalize_zero_iff ε t x.1).1 x.2⟩
  invFun y := ⟨(classesEquiv ε t).symm y.1, (normalize_zero_iff ε t _).2
    (by
      change (algEquivZeroCut c ε).onClasses t
        ((classesEquiv ε t) ((classesEquiv ε t).symm y.1))
      rw [Equiv.apply_symm_apply]
      exact y.2)⟩
  left_inv x := Subtype.ext ((classesEquiv ε t).symm_apply_apply x.1)
  right_inv y := Subtype.ext ((classesEquiv ε t).apply_symm_apply y.1)

def

zeroPresheafIso

L147 ↗

AlgebraicGeometry.RelPicard.Unrigidified.zeroPresheafIso

Documentation

The unrigidified and pointed Picard-zero presheaves are naturally isomorphic whenever the curve is supplied with an actual section.

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 zeroPresheafIso (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    zeroPresheaf c ≅ relSubPicPresheaf c ε (algEquivZeroCut c ε)

Module documentation

The unrigidified degree-zero Picard presheaf

Declarations