Module

Exists_representsRelSubPic_baseChange.lean

Nyll.JacobianVarieties.Picard.Exists_representsRelSubPic_baseChange

6 declarations indexed from sourceView source ↗

Module documentation

Base change of a relative Picard representation

Transport the representing property and rigidified line bundles across a change of base.

Imports8

Imported by10

def

pullbackAlongComp

L44 ↗

JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch.pullbackAlongComp

Documentation

Identify iterated pullback of a rigidified line bundle with pullback along the composite.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra AlgebraicGeometry.SmoothProperCurve GoodReductionJacobian
open AlgebraicGeometry.RelPicard.BaseChange
namespace RepBCSketch
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

def pullbackAlongComp {T T' T'' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} {t'' : T'' ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε t) (φ : SchemeHomOver t' t) (ψ : SchemeHomOver t'' t') :
    ((M.pullbackAlong φ).pullbackAlong ψ).L ≅ (M.pullbackAlong (postComp φ ψ)).L

def

pullbackAlongCongr

L52 ↗

JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch.pullbackAlongCongr

Documentation

Identify pullbacks of a rigidified line bundle along equal morphisms.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra AlgebraicGeometry.SmoothProperCurve GoodReductionJacobian
open AlgebraicGeometry.RelPicard.BaseChange
namespace RepBCSketch
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

def pullbackAlongCongr {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (M : RigidifiedLineBundle c ε t) {φ ψ : SchemeHomOver t' t}
    (e : φ.1 = ψ.1) : (M.pullbackAlong φ).L ≅ (M.pullbackAlong ψ).L

def

unitPullbackAlong

L58 ↗

JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch.unitPullbackAlong

Documentation

Pullback of the unit rigidified line bundle is isomorphic to the unit bundle.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra AlgebraicGeometry.SmoothProperCurve GoodReductionJacobian
open AlgebraicGeometry.RelPicard.BaseChange
namespace RepBCSketch
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

def unitPullbackAlong {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    ((RigidifiedLineBundle.unit (c := c) (ε := ε) t).pullbackAlong ψ).L ≅
      (RigidifiedLineBundle.unit (c := c) (ε := ε) t').L

def

isoOfToRIso

L67 ↗

JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch.isoOfToRIso

Documentation

Recover an isomorphism over the extended base from its restriction to the original base.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra AlgebraicGeometry.SmoothProperCurve GoodReductionJacobian
open AlgebraicGeometry.RelPicard.BaseChange
namespace RepBCSketch
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
variable (R' : Type u) [CommRing R'] [Algebra R R']

Lean source · statement

def isoOfToRIso {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R')}
    (X M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t)
    (i : (toR c ε R' X).L ≅ (toR c ε R' M).L) : X.L ≅ M.L

theorem

mem_iff

L73 ↗

JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange.RepBCSketch.mem_iff

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_representsRelSubPic_baseChange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra AlgebraicGeometry.SmoothProperCurve GoodReductionJacobian
open AlgebraicGeometry.RelPicard.BaseChange
namespace RepBCSketch
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
variable (R' : Type u) [CommRing R'] [Algebra R R']

Lean source · statement

theorem mem_iff {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
    (M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t) :
    (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)).P t M ↔
      (algEquivZeroCut c ε).P (t ≫ specMap R R') (toR c ε R' M)

theorem