Module

Presheaf.lean

Nyll.AlgebraicCurves.Geometry.Picard.RelSubPic.Presheaf

8 declarations indexed from sourceView source ↗

Module documentation

Presheaves of rigidified line-bundle classes satisfying a pullback-stable Picard condition.

Imports2

Imported by59

def

pullbackAlongPullbackAlongIso

L36 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.pullbackAlongPullbackAlongIso

Documentation

The underlying line-bundle isomorphism comparing iterated pullback with pullback along a composite.

Source context 6 commands

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

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

Lean source · statement

def pullbackAlongPullbackAlongIso {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

pullbackAlongIdIso

L47 ↗

AlgebraicGeometry.RelPicard.RigidifiedLineBundle.pullbackAlongIdIso

Documentation

The underlying line-bundle isomorphism from pullback along the identity to the original bundle.

Source context 6 commands

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

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

Lean source · statement

def pullbackAlongIdIso {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε t) :
    (M.pullbackAlong ⟨𝟙 T, Category.id_comp t⟩).L ≅ M.L

def

onClasses

L58 ↗

AlgebraicGeometry.RelPicard.SubPicCondition.onClasses

Documentation

The Picard condition descended to isomorphism classes of rigidified line bundles.

Source context 6 commands

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

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

Lean source · statement

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

theorem

onClasses_mk

L62 ↗

AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk

Source context 6 commands

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

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

Lean source · statement

theorem onClasses_mk (P : SubPicCondition c ε) {T : Scheme.{u}} (t : T ⟶ Spec
    (CommRingCat.of R))
    (M : RigidifiedLineBundle c ε t) : P.onClasses t (Quotient.mk _ M) ↔ P.P t M

theorem

onClasses_classesMap

L66 ↗

AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_classesMap

Source context 6 commands

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

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

Lean source · statement

theorem onClasses_classesMap (P : SubPicCondition c ε) {T T' : Scheme.{u}} {t : T ⟶ Spec
    (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) (x :
      RigidifiedLineBundle.Classes c ε t)
    (hx : P.onClasses t x) : P.onClasses t' (RigidifiedLineBundle.classesMap ψ x)

def

relSubPicSubfunctor

L77 ↗

AlgebraicGeometry.RelPicard.relSubPicSubfunctor

Documentation

The subfunctor of relative Picard classes satisfying the given condition.

Source context 5 commands

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

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

Lean source · full declaration

def relSubPicSubfunctor (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c)
    (P : SubPicCondition c ε) : Subfunctor (relPicardPresheaf c ε) where
  obj X := {x | P.onClasses X.unop.hom x}
  map φ := fun x hx => P.onClasses_classesMap ⟨φ.unop.left, Over.w φ.unop⟩ x hx

def

relSubPicPresheaf

L84 ↗

AlgebraicGeometry.RelPicard.relSubPicPresheaf

Documentation

The presheaf of relative Picard classes satisfying the given condition.

Source context 5 commands

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

noncomputable section
namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra GoodReductionJacobian Opposite
universe u
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 relSubPicPresheaf (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) c)
    (P : SubPicCondition c ε) : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type (u + 1)

theorem

relSubPicPresheaf_map_coe

L90 ↗

AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe

Source context 5 commands

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

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

Lean source · statement

theorem relSubPicPresheaf_map_coe {P : SubPicCondition c ε} {X X' : (Over (Spec
    (CommRingCat.of R)))ᵒᵖ}
    (φ : X ⟶ X') (x : (relSubPicPresheaf c ε P).obj X) :
    ((relSubPicPresheaf c ε P).map φ x).1 = RigidifiedLineBundle.classesMap ⟨φ.unop.left, Over.w
      φ.unop⟩ x.1

Module documentation

Declarations