NYLL
Module

BaseChange.lean

Nyll.AlgebraicCurves.Geometry.Picard.RelSubPic.BaseChange
37 declarations indexed from sourceView source ↗

Module documentation

Scalar extension of Picard conditions and the induced equivalences of rigidified line-bundle classes.

Imports7
Imported by44

Declarations

def

κ

L39 ↗
AlgebraicGeometry.RelPicard.BaseChange.κ
Documentation

The canonical isomorphism comparing iterated scalar extension with the composite base morphism.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def κ {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    pullback (baseChange R c R') t' ≅ pullback c (t' ≫ specMap R R')
theorem

κ_hom_snd

L43 ↗
AlgebraicGeometry.RelPicard.BaseChange.κ_hom_snd
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem κ_hom_snd {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    (κ c R' t').hom ≫ pullback.snd c (t' ≫ specMap R R') = pullback.snd (baseChange R c R') t'
theorem

κ_hom_fst

L47 ↗
AlgebraicGeometry.RelPicard.BaseChange.κ_hom_fst
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem κ_hom_fst {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    (κ c R' t').hom ≫ pullback.fst c (t' ≫ specMap R R') =
      pullback.fst (baseChange R c R') t' ≫ pullback.fst c (specMap R R')
theorem

rigSection_fst'

L52 ↗
AlgebraicGeometry.RelPicard.BaseChange.rigSection_fst'
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
omit [Algebra R R'] in
Lean source · statement
theorem rigSection_fst' {T : Scheme.{u}} (cc : C ⟶ Spec (CommRingCat.of R')) (t : T ⟶ Spec
    (CommRingCat.of R'))
    (e : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) cc) :
    rigSection cc t e ≫ pullback.fst cc t = t ≫ e.1
theorem

rigSection_snd'

L58 ↗
AlgebraicGeometry.RelPicard.BaseChange.rigSection_snd'
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
omit [Algebra R R'] in
Lean source · statement
theorem rigSection_snd' {T : Scheme.{u}} (cc : C ⟶ Spec (CommRingCat.of R')) (t : T ⟶ Spec
    (CommRingCat.of R'))
    (e : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) cc) :
    rigSection cc t e ≫ pullback.snd cc t = 𝟙 T
theorem

baseChangeSnd_fst'

L64 ↗
AlgebraicGeometry.RelPicard.BaseChange.baseChangeSnd_fst'
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
omit [Algebra R R'] in
Lean source · statement
theorem baseChangeSnd_fst' {T T' : Scheme.{u}} (cc : C ⟶ Spec (CommRingCat.of R'))
    {t : T ⟶ Spec (CommRingCat.of R')} {t' : T' ⟶ Spec (CommRingCat.of R')} (ψ : SchemeHomOver
      t' t) :
    baseChangeSnd cc ψ ≫ pullback.fst cc t = pullback.fst cc t'
theorem

baseChangeSnd_snd'

L70 ↗
AlgebraicGeometry.RelPicard.BaseChange.baseChangeSnd_snd'
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
omit [Algebra R R'] in
Lean source · statement
theorem baseChangeSnd_snd' {T T' : Scheme.{u}} (cc : C ⟶ Spec (CommRingCat.of R'))
    {t : T ⟶ Spec (CommRingCat.of R')} {t' : T' ⟶ Spec (CommRingCat.of R')} (ψ : SchemeHomOver
      t' t) :
    baseChangeSnd cc ψ ≫ pullback.snd cc t = pullback.snd cc t' ≫ ψ.1
theorem

rigSection_κ_hom

L76 ↗
AlgebraicGeometry.RelPicard.BaseChange.rigSection_κ_hom
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem rigSection_κ_hom {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    rigSection (baseChange R c R') t' (sectionBaseChange R' ε) ≫ (κ c R' t').hom =
      rigSection c (t' ≫ specMap R R') ε
theorem

rigSection_κ_inv

L85 ↗
AlgebraicGeometry.RelPicard.BaseChange.rigSection_κ_inv
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem rigSection_κ_inv {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    rigSection c (t' ≫ specMap R R') ε ≫ (κ c R' t').inv =
      rigSection (baseChange R c R') t' (sectionBaseChange R' ε)
def

overR

L93 ↗
AlgebraicGeometry.RelPicard.BaseChange.overR
Documentation

The relative test-scheme morphism obtained by composing the base maps with Spec R' to Spec R.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def overR {T T'' : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')} {t'' : T'' ⟶ Spec
    (CommRingCat.of R')}
    (ψ : SchemeHomOver t'' t') : SchemeHomOver (t'' ≫ specMap R R') (t' ≫ specMap R R')
theorem

baseChangeSnd_κ_hom

L98 ↗
AlgebraicGeometry.RelPicard.BaseChange.baseChangeSnd_κ_hom
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem baseChangeSnd_κ_hom {T T'' : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    {t'' : T'' ⟶ Spec (CommRingCat.of R')} (ψ : SchemeHomOver t'' t') :
    baseChangeSnd (baseChange R c R') ψ ≫ (κ c R' t').hom =
      (κ c R' t'').hom ≫ baseChangeSnd c (overR R' ψ)
def

toR

L114 ↗
AlgebraicGeometry.RelPicard.BaseChange.toR
Documentation

A rigidified line bundle over the scalar-extended curve, viewed over the original base via the canonical pullback isomorphism.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · full declaration
def toR {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t') :
    RigidifiedLineBundle c ε (t' ≫ specMap R R') where
  L := (Scheme.Modules.pullback (κ c R' t').inv).obj M.L
  isInvertible := M.isInvertible.pullback _
  rigidified :=
    ⟨(Scheme.Modules.pullbackComp (rigSection c (t' ≫ specMap R R') ε) (κ c R' t').inv).app M.L ≪≫
      (Scheme.Modules.pullbackCongr (rigSection_κ_inv c ε R' t')).app M.L ≪≫ M.rigidified.some⟩
def

ofR

L124 ↗
AlgebraicGeometry.RelPicard.BaseChange.ofR
Documentation

A rigidified line bundle over the original base, transported to the scalar-extended curve.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · full declaration
def ofR {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    (M : RigidifiedLineBundle c ε (t' ≫ specMap R R')) :
    RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t' where
  L := (Scheme.Modules.pullback (κ c R' t').hom).obj M.L
  isInvertible := M.isInvertible.pullback _
  rigidified :=
    ⟨(Scheme.Modules.pullbackComp (rigSection (baseChange R c R') t' (sectionBaseChange R' ε))
        (κ c R' t').hom).app M.L ≪≫
      (Scheme.Modules.pullbackCongr (rigSection_κ_hom c ε R' t')).app M.L ≪≫ M.rigidified.some⟩
def

toR_ofR_iso

L135 ↗
AlgebraicGeometry.RelPicard.BaseChange.toR_ofR_iso
Documentation

The underlying line-bundle isomorphism after transport to the extended curve and back.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def toR_ofR_iso {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    (M : RigidifiedLineBundle c ε (t' ≫ specMap R R')) : (toR c ε R' (ofR c ε R' M)).L ≅ M.L
def

ofR_toR_iso

L142 ↗
AlgebraicGeometry.RelPicard.BaseChange.ofR_toR_iso
Documentation

The underlying line-bundle isomorphism after transport to the original curve and back.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def ofR_toR_iso {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t') :
    (ofR c ε R' (toR c ε R' M)).L ≅ M.L
theorem

baseChangeSnd_κ_inv

L149 ↗
AlgebraicGeometry.RelPicard.BaseChange.baseChangeSnd_κ_inv
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem baseChangeSnd_κ_inv {T T'' : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    {t'' : T'' ⟶ Spec (CommRingCat.of R')} (ψ : SchemeHomOver t'' t') :
    baseChangeSnd c (overR R' ψ) ≫ (κ c R' t').inv = (κ c R' t'').inv ≫ baseChangeSnd
      (baseChange R c R') ψ
def

toR_pullbackAlong_iso

L159 ↗
AlgebraicGeometry.RelPicard.BaseChange.toR_pullbackAlong_iso
Documentation

The underlying isomorphism expressing compatibility of transport to the original base with pullback.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def toR_pullbackAlong_iso {T T'' : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    {t'' : T'' ⟶ Spec (CommRingCat.of R')} (ψ : SchemeHomOver t'' t')
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t') :
    ((toR c ε R' M).pullbackAlong (overR R' ψ)).L ≅ (toR c ε R' (M.pullbackAlong ψ)).L
def

toR_unit_iso

L169 ↗
AlgebraicGeometry.RelPicard.BaseChange.toR_unit_iso
Documentation

Transport to the original base preserves the underlying unit line bundle.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def toR_unit_iso {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    (toR c ε R' (RigidifiedLineBundle.unit t')).L ≅
      (RigidifiedLineBundle.unit (c := c) (ε := ε) (t' ≫ specMap R R')).L
def

restrict

L175 ↗
AlgebraicGeometry.RelPicard.BaseChange.restrict
Documentation

The Picard condition on the scalar-extended curve obtained from the original condition.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · full declaration
def restrict (P : SubPicCondition c ε) :
    SubPicCondition (baseChange R c R') (sectionBaseChange R' ε) where
  P := fun t' M => P.P (t' ≫ specMap R R') (toR c ε R' M)
  unit_mem := fun t' => P.congr _ _ _ ⟨(toR_unit_iso c ε R' t').symm⟩ (P.unit_mem (t' ≫ specMap
    R R'))
  congr := fun t' _ _ h hM => P.congr _ _ _ ⟨(Scheme.Modules.pullback (κ c R' t').inv).mapIso
    h.some⟩ hM
  pullback_mem := fun _ _ ψ M hM =>
    P.congr _ _ _ ⟨toR_pullbackAlong_iso c ε R' ψ M⟩ (P.pullback_mem _ _ (overR R' ψ) _ hM)
theorem

restrict_P

L185 ↗
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem restrict_P (P : SubPicCondition c ε) {T : Scheme.{u}} (t' : T ⟶ Spec
    (CommRingCat.of R'))
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t') :
    (restrict c ε R' P).P t' M ↔ P.P (t' ≫ specMap R R') (toR c ε R' M)
theorem

subPicCondition_ext

L190 ↗
AlgebraicGeometry.RelPicard.BaseChange.subPicCondition_ext
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
omit [Algebra R R'] in
Lean source · statement
theorem subPicCondition_ext {cc : C ⟶ Spec (CommRingCat.of R')}
    {e : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) cc} {P Q : SubPicCondition cc e}
    (h : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) (M : RigidifiedLineBundle cc e
      t), P.P t M ↔ Q.P t M) :
    P = Q
def

fibreMap

L209 ↗
AlgebraicGeometry.RelPicard.BaseChange.fibreMap
Documentation

The forward fibre morphism induced by the canonical iterated-pullback isomorphism.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
section fibres
variable {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) {k : Type u} [Field k]
  (σ : Spec (CommRingCat.of k) ⟶ T)
Lean source · statement
def fibreMap :
    pullback (pullback.snd (baseChange R c R') t') σ ⟶ pullback (pullback.snd c (t' ≫ specMap R
      R')) σ
def

fibreMap'

L216 ↗
AlgebraicGeometry.RelPicard.BaseChange.fibreMap'
Documentation

The reverse fibre morphism induced by the inverse canonical iterated-pullback isomorphism.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
section fibres
variable {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) {k : Type u} [Field k]
  (σ : Spec (CommRingCat.of k) ⟶ T)
Lean source · statement
def fibreMap' :
    pullback (pullback.snd c (t' ≫ specMap R R')) σ ⟶ pullback (pullback.snd (baseChange R c R')
      t') σ
theorem

fibreMap_fibreAt

L223 ↗
AlgebraicGeometry.RelPicard.BaseChange.fibreMap_fibreAt
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
section fibres
variable {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) {k : Type u} [Field k]
  (σ : Spec (CommRingCat.of k) ⟶ T)
Lean source · statement
theorem fibreMap_fibreAt : fibreMap c R' t' σ ≫ fibreAt c (t' ≫ specMap R R') σ = fibreAt
    (baseChange R c R') t' σ
theorem

fibreMap'_fibreAt

L227 ↗
AlgebraicGeometry.RelPicard.BaseChange.fibreMap'_fibreAt
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
section fibres
variable {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) {k : Type u} [Field k]
  (σ : Spec (CommRingCat.of k) ⟶ T)
Lean source · statement
theorem fibreMap'_fibreAt :
    fibreMap' c R' t' σ ≫ fibreAt (baseChange R c R') t' σ = fibreAt c (t' ≫ specMap R R') σ
theorem

fibreMap_fst

L231 ↗
AlgebraicGeometry.RelPicard.BaseChange.fibreMap_fst
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
section fibres
variable {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) {k : Type u} [Field k]
  (σ : Spec (CommRingCat.of k) ⟶ T)
Lean source · statement
theorem fibreMap_fst : fibreMap c R' t' σ ≫ pullback.fst (pullback.snd c (t' ≫ specMap R R')) σ =
    pullback.fst (pullback.snd (baseChange R c R') t') σ ≫ (κ c R' t').hom
theorem

fibreMap'_fst

L235 ↗
AlgebraicGeometry.RelPicard.BaseChange.fibreMap'_fst
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
section fibres
variable {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) {k : Type u} [Field k]
  (σ : Spec (CommRingCat.of k) ⟶ T)
Lean source · statement
theorem fibreMap'_fst : fibreMap' c R' t' σ ≫ pullback.fst (pullback.snd (baseChange R c R') t') σ =
    pullback.fst (pullback.snd c (t' ≫ specMap R R')) σ ≫ (κ c R' t').inv
theorem

fibrewiseAlgEquivZero_toR_iff

L241 ↗
AlgebraicGeometry.RelPicard.BaseChange.fibrewiseAlgEquivZero_toR_iff
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem fibrewiseAlgEquivZero_toR_iff {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t') :
    FibrewiseAlgEquivZero (toR c ε R' M) ↔ FibrewiseAlgEquivZero M
theorem

restrict_algEquivZeroCut

L264 ↗
AlgebraicGeometry.RelPicard.BaseChange.restrict_algEquivZeroCut
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem restrict_algEquivZeroCut :
    restrict c ε R' (algEquivZeroCut c ε) = algEquivZeroCut (baseChange R c R')
      (sectionBaseChange R' ε)
def

classesEquiv

L272 ↗
AlgebraicGeometry.RelPicard.BaseChange.classesEquiv
Documentation

The equivalence of rigidified line-bundle classes across the canonical pullback isomorphism.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · full declaration
def classesEquiv {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    RigidifiedLineBundle.Classes (baseChange R c R') (sectionBaseChange R' ε) t' ≃
      RigidifiedLineBundle.Classes c ε (t' ≫ specMap R R') where
  toFun := Quotient.map (toR c ε R') (fun _ _ h => ⟨(Scheme.Modules.pullback (κ c R'
    t').inv).mapIso h.some⟩)
  invFun := Quotient.map (ofR c ε R') (fun _ _ h => ⟨(Scheme.Modules.pullback (κ c R'
    t').hom).mapIso h.some⟩)
  left_inv := fun x => by
    induction x using Quotient.ind
    exact Quotient.sound ⟨ofR_toR_iso c ε R' _⟩
  right_inv := fun x => by
    induction x using Quotient.ind
    exact Quotient.sound ⟨toR_ofR_iso c ε R' _⟩
theorem

onClasses_classesEquiv

L286 ↗
AlgebraicGeometry.RelPicard.BaseChange.onClasses_classesEquiv
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem onClasses_classesEquiv (P : SubPicCondition c ε) {T : Scheme.{u}} (t' : T ⟶ Spec
    (CommRingCat.of R'))
    (x : RigidifiedLineBundle.Classes (baseChange R c R') (sectionBaseChange R' ε) t') :
    P.onClasses (t' ≫ specMap R R') (classesEquiv c ε R' t' x) ↔ (restrict c ε R' P).onClasses
      t' x
theorem

classesEquiv_classesMap

L294 ↗
AlgebraicGeometry.RelPicard.BaseChange.classesEquiv_classesMap
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem classesEquiv_classesMap {T T'' : Scheme.{u}}
    {t' : T ⟶ Spec (CommRingCat.of R')} {t'' : T'' ⟶ Spec (CommRingCat.of R')} (ψ :
      SchemeHomOver t'' t')
    (x : RigidifiedLineBundle.Classes (baseChange R c R') (sectionBaseChange R' ε) t') :
    classesEquiv c ε R' t'' (RigidifiedLineBundle.classesMap ψ x) =
      RigidifiedLineBundle.classesMap (overR R' ψ) (classesEquiv c ε R' t' x)
def

relSubPicPresheafRestrictIso

L306 ↗
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso
Documentation

The presheaf isomorphism identifying the restricted Picard condition with base restriction.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def relSubPicPresheafRestrictIso (P : SubPicCondition c ε) :
    relSubPicPresheaf (baseChange R c R') (sectionBaseChange R' ε) (restrict c ε R' P) ≅
      (Over.map (specMap R R')).op ⋙ relSubPicPresheaf c ε P
def

relSubPicPresheafAlgEquivZeroCutIso

L329 ↗
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafAlgEquivZeroCutIso
Documentation

The presheaf isomorphism comparing algebraic-equivalence-to-zero classes before and after scalar extension.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def relSubPicPresheafAlgEquivZeroCutIso :
    relSubPicPresheaf (baseChange R c R') (sectionBaseChange R' ε)
        (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) ≅
      (Over.map (specMap R R')).op ⋙ relSubPicPresheaf c ε (algEquivZeroCut c ε)
theorem

relSubPicPresheaf_eqToHom_app_coe

L336 ↗
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheaf_eqToHom_app_coe
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
omit [Algebra R R'] in
Lean source · statement
theorem relSubPicPresheaf_eqToHom_app_coe {cc : C ⟶ Spec (CommRingCat.of R')}
    {e : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) cc} {P₁ P₂ : SubPicCondition cc e} (h : P₁
      = P₂)
    (X : (Over (Spec (CommRingCat.of R')))ᵒᵖ) (x : (relSubPicPresheaf cc e P₁).obj X) :
    ((eqToHom (congrArg (relSubPicPresheaf cc e) h)).app X x).1 = x.1
theorem

relSubPicPresheafRestrictIso_hom_app_coe

L344 ↗
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem relSubPicPresheafRestrictIso_hom_app_coe (P : SubPicCondition c ε)
    (X : (Over (Spec (CommRingCat.of R')))ᵒᵖ)
    (x : (relSubPicPresheaf (baseChange R c R') (sectionBaseChange R' ε) (restrict c ε R'
      P)).obj X) :
    ((relSubPicPresheafRestrictIso c ε R' P).hom.app X x).1 = classesEquiv c ε R' X.unop.hom x.1
theorem

relSubPicPresheafRestrictIso_inv_app_coe

L351 ↗
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian Opposite
namespace AlgebraicGeometry.RelPicard.BaseChange
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
theorem relSubPicPresheafRestrictIso_inv_app_coe (P : SubPicCondition c ε)
    (X : (Over (Spec (CommRingCat.of R')))ᵒᵖ)
    (y : ((Over.map (specMap R R')).op ⋙ relSubPicPresheaf c ε P).obj X) :
    ((relSubPicPresheafRestrictIso c ε R' P).inv.app X y).1 = (classesEquiv c ε R'
      X.unop.hom).symm y.1

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