NYLL
Module

UnrigidifiedBaseChange.lean

Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedBaseChange
10 declarations indexed from sourceView source ↗

Module documentation

Base change of unrigidified Picard classes

The canonical isomorphism between iterated pullbacks identifies relative classes over an extended base with restriction of the original presheaf. The comparison preserves the actual geometric-fibre condition and requires no rational point.

Imports6
Imported by2

Declarations

def

restrictBundle

L45 ↗
AlgebraicGeometry.RelPicard.Unrigidified.restrictBundle
Documentation

View an invertible module on the scalar-extended curve over the original base.

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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def restrictBundle {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R')}
    (M : LineBundle (baseChange R c R') t) : LineBundle c (t ≫ specMap R R')
def

extendBundle

L50 ↗
AlgebraicGeometry.RelPicard.Unrigidified.extendBundle
Documentation

Transport an invertible module to the scalar-extended curve.

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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def extendBundle {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R')}
    (M : LineBundle c (t ≫ specMap R R')) : LineBundle (baseChange R c R') t
theorem

baseTwist_restrict

L54 ↗
AlgebraicGeometry.RelPicard.Unrigidified.baseTwist_restrict
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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem baseTwist_restrict {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R')}
    {M N : LineBundle (baseChange R c R') t} (h : BaseTwist (baseChange R c R') t M N) :
    BaseTwist c (t ≫ specMap R R') (restrictBundle c R' M) (restrictBundle c R' N)
theorem

baseTwist_extend

L66 ↗
AlgebraicGeometry.RelPicard.Unrigidified.baseTwist_extend
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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem baseTwist_extend {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R')}
    {M N : LineBundle c (t ≫ specMap R R')} (h : BaseTwist c (t ≫ specMap R R') M N) :
    BaseTwist (baseChange R c R') t (extendBundle c R' M) (extendBundle c R' N)
def

baseChangeClassesEquiv

L76 ↗
AlgebraicGeometry.RelPicard.Unrigidified.baseChangeClassesEquiv
Documentation

The actual equivalence of relative classes across the canonical pullback isomorphism.

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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · full declaration
def baseChangeClassesEquiv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) :
    Classes (baseChange R c R') t ≃ Classes c (t ≫ specMap R R') where
  toFun := Quot.map (restrictBundle c R') (fun _ _ h => baseTwist_restrict c R' h)
  invFun := Quot.map (extendBundle c R') (fun _ _ h => baseTwist_extend c R' h)
  left_inv x := by
    induction x using Quot.ind with
    | _ M =>
      exact Quot.sound (baseTwist_of_iso
        ((Scheme.Modules.pullbackComp (κ c R' t).hom (κ c R' t).inv).app M.1 ≪≫
          (Scheme.Modules.pullbackCongr (κ c R' t).hom_inv_id).app M.1 ≪≫
          (Scheme.Modules.pullbackId _).app M.1))
  right_inv x := by
    induction x using Quot.ind with
    | _ M =>
      exact Quot.sound (baseTwist_of_iso
        ((Scheme.Modules.pullbackComp (κ c R' t).inv (κ c R' t).hom).app M.1 ≪≫
          (Scheme.Modules.pullbackCongr (κ c R' t).inv_hom_id).app M.1 ≪≫
          (Scheme.Modules.pullbackId _).app M.1))
def

baseChangeIso

L96 ↗
AlgebraicGeometry.RelPicard.Unrigidified.baseChangeIso
Documentation

Base change of the unrigidified relative Picard presheaf.

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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def baseChangeIso :
    presheaf (baseChange R c R') ≅ (Over.map (specMap R R')).op ⋙ presheaf c
theorem

fibrewiseZero_restrict_iff

L112 ↗
AlgebraicGeometry.RelPicard.Unrigidified.fibrewiseZero_restrict_iff
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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem fibrewiseZero_restrict_iff {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R')}
    (M : LineBundle (baseChange R c R') t) :
    FibrewiseZero (restrictBundle c R' M) ↔ FibrewiseZero M
theorem

classesZero_baseChange_iff

L135 ↗
AlgebraicGeometry.RelPicard.Unrigidified.classesZero_baseChange_iff
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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem classesZero_baseChange_iff {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
    (x : Classes (baseChange R c R') t) :
    classesZero (t ≫ specMap R R') (baseChangeClassesEquiv c R' t x) ↔ classesZero t x
def

zeroBaseChangeClassesEquiv

L142 ↗
AlgebraicGeometry.RelPicard.Unrigidified.zeroBaseChangeClassesEquiv
Documentation

The geometric-fibre condition cuts out corresponding subsets on either base.

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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · full declaration
def zeroBaseChangeClassesEquiv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) :
    {x : Classes (baseChange R c R') t // classesZero t x} ≃
      {x : Classes c (t ≫ specMap R R') // classesZero (t ≫ specMap R R') x} where
  toFun x := ⟨baseChangeClassesEquiv c R' t x.1, (classesZero_baseChange_iff c R' t x.1).2 x.2⟩
  invFun y := ⟨(baseChangeClassesEquiv c R' t).symm y.1,
    (classesZero_baseChange_iff c R' t _).1 (by
      rw [Equiv.apply_symm_apply]
      exact y.2)⟩
  left_inv x := Subtype.ext ((baseChangeClassesEquiv c R' t).symm_apply_apply x.1)
  right_inv y := Subtype.ext ((baseChangeClassesEquiv c R' t).apply_symm_apply y.1)
def

zeroBaseChangeIso

L154 ↗
AlgebraicGeometry.RelPicard.Unrigidified.zeroBaseChangeIso
Documentation

Base change of the unrigidified Picard-zero presheaf, without any choice of section.

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 AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open AlgebraicGeometry.RelPicard.BaseChange
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def zeroBaseChangeIso :
    zeroPresheaf (baseChange R c R') ≅ (Over.map (specMap R R')).op ⋙ zeroPresheaf c

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