Module

RelSubPicGlue.lean

Nyll.JacobianVarieties.Picard.RelSubPicGlue

11 declarations indexed from sourceView source ↗

Module documentation

Gluing relative sub-Picard representations

Representations of the sub-Picard presheaf determine relative Picard designations and their zero sections. A locally surjective family of representable open charts glues to a designation representing the presheaf through its total sheaf.

Imports4

Imported by7

def

designationOfRepresentableBy

L37 ↗

AlgebraicGeometry.RelPicard.designationOfRepresentableBy

Documentation

The relative Picard designation obtained from a representing object, with its zero section.

Source context 4 commands

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

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

Lean source · full declaration

def designationOfRepresentableBy {Y : Scheme.{u}} {p : Y ⟶ Spec (CommRingCat.of R)}
    (e : (relSubPicPresheaf c ε P).RepresentableBy (Over.mk p)) : RelativePic0Designation R c where
  P := Y
  toBase := p
  zeroSection := (e.homEquiv.symm
    (⟨relPicardPresheaf.unitClass c ε (Over.mk (𝟙 _)), P.unit_mem _⟩ :
      (relSubPicPresheaf c ε P).obj (op (Over.mk (𝟙 (Spec (CommRingCat.of R))))))).left
  zeroSection_toBase := Over.w _

theorem

designationOfRepresentableBy_P

L46 ↗

AlgebraicGeometry.RelPicard.designationOfRepresentableBy_P

Source context 4 commands

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

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

Lean source · statement

theorem designationOfRepresentableBy_P {Y : Scheme.{u}} {p : Y ⟶ Spec (CommRingCat.of R)}
    (e : (relSubPicPresheaf c ε P).RepresentableBy (Over.mk p)) :
    (designationOfRepresentableBy e).P = Y

theorem

designationOfRepresentableBy_toBase

L50 ↗

AlgebraicGeometry.RelPicard.designationOfRepresentableBy_toBase

Source context 4 commands

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

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

Lean source · statement

theorem designationOfRepresentableBy_toBase {Y : Scheme.{u}}
    {p : Y ⟶ Spec (CommRingCat.of R)}
    (e : (relSubPicPresheaf c ε P).RepresentableBy (Over.mk p)) :
    (designationOfRepresentableBy e).toBase = p

theorem

homEquiv_zeroSection_designationOfRepresentableBy

L56 ↗

AlgebraicGeometry.RelPicard.homEquiv_zeroSection_designationOfRepresentableBy

Source context 4 commands

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

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

Lean source · statement

theorem homEquiv_zeroSection_designationOfRepresentableBy {Y : Scheme.{u}}
    {p : Y ⟶ Spec (CommRingCat.of R)}
    (e : (relSubPicPresheaf c ε P).RepresentableBy (Over.mk p)) :
    (e.homEquiv (Over.homMk (designationOfRepresentableBy e).zeroSection
        (designationOfRepresentableBy e).zeroSection_toBase :
        Over.mk (𝟙 (Spec (CommRingCat.of R))) ⟶ Over.mk p)).1 =
      relPicardPresheaf.unitClass c ε (Over.mk (𝟙 _))

theorem

nonempty_of_representableBy'

L74 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_of_representableBy'

Source context 4 commands

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

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

Lean source · statement

theorem RepresentsRelSubPic.nonempty_of_representableBy' {Y : Scheme.{u}}
    {p : Y ⟶ Spec (CommRingCat.of R)}
    (e : (relSubPicPresheaf c ε P).RepresentableBy (Over.mk p)) :
    Nonempty (RepresentsRelSubPic c ε P (designationOfRepresentableBy e))

theorem

nonempty_of_overTotal_representableBy

L81 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_of_overTotal_representableBy

Source context 4 commands

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

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

Lean source · statement

theorem RepresentsRelSubPic.nonempty_of_overTotal_representableBy {Y : Scheme.{u}}
    (e : (relSubPicPresheaf c ε P).overTotal.RepresentableBy Y) :
    Nonempty (RepresentsRelSubPic c ε P
      (designationOfRepresentableBy (Functor.RepresentableBy.ofOverTotal e)))

abbrev

relSubPicTotalSheaf

L88 ↗

AlgebraicGeometry.RelPicard.relSubPicTotalSheaf

Documentation

The total sheaf on schemes associated to the relative sub-Picard sheaf over the base.

Source context 4 commands

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

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

Lean source · statement

abbrev relSubPicTotalSheaf
    (hG : Presieve.IsSheaf (Scheme.zariskiTopology.over (Spec (CommRingCat.of R)))
      (relSubPicPresheaf c ε P)) :
    Sheaf Scheme.zariskiTopology (Type (u + 1))

def

gluedDesignation

L105 ↗

AlgebraicGeometry.RelPicard.gluedDesignation

Documentation

The relative Picard designation obtained by gluing the locally representable open charts.

Source context 6 commands

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

universe w v u
namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra GoodReductionJacobian Opposite
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {P : SubPicCondition c ε}
section glue
variable (hG : Presieve.IsSheaf (Scheme.zariskiTopology.over (Spec (CommRingCat.of R)))
    (relSubPicPresheaf c ε P))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : ∀ i, uliftYoneda.{u + 1}.obj (X i) ⟶ (relSubPicPresheaf c ε P).overTotal)
  (hf : ∀ i, MorphismProperty.presheafULift.{u + 1} @IsOpenImmersion (f i))
  [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Limits.Sigma.desc f)]

Lean source · statement

def gluedDesignation : RelativePic0Designation R c

theorem

gluedDesignation_P

L109 ↗

AlgebraicGeometry.RelPicard.gluedDesignation_P

Source context 6 commands

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

universe w v u
namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra GoodReductionJacobian Opposite
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {P : SubPicCondition c ε}
section glue
variable (hG : Presieve.IsSheaf (Scheme.zariskiTopology.over (Spec (CommRingCat.of R)))
    (relSubPicPresheaf c ε P))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : ∀ i, uliftYoneda.{u + 1}.obj (X i) ⟶ (relSubPicPresheaf c ε P).overTotal)
  (hf : ∀ i, MorphismProperty.presheafULift.{u + 1} @IsOpenImmersion (f i))
  [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Limits.Sigma.desc f)]

Lean source · statement

theorem gluedDesignation_P :
    (gluedDesignation hG f hf).P =
      (Scheme.LocalRepresentabilityULift.glueData
        (F := relSubPicTotalSheaf hG) (f := f) hf).glued

theorem

nonempty_gluedDesignation

L114 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_gluedDesignation

Source context 6 commands

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

universe w v u
namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra GoodReductionJacobian Opposite
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {P : SubPicCondition c ε}
section glue
variable (hG : Presieve.IsSheaf (Scheme.zariskiTopology.over (Spec (CommRingCat.of R)))
    (relSubPicPresheaf c ε P))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : ∀ i, uliftYoneda.{u + 1}.obj (X i) ⟶ (relSubPicPresheaf c ε P).overTotal)
  (hf : ∀ i, MorphismProperty.presheafULift.{u + 1} @IsOpenImmersion (f i))
  [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Limits.Sigma.desc f)]

Lean source · statement

theorem RepresentsRelSubPic.nonempty_gluedDesignation :
    Nonempty (RepresentsRelSubPic c ε P (gluedDesignation hG f hf))

instance

isOpenImmersion_toGlued

L119 ↗

AlgebraicGeometry.RelPicard.isOpenImmersion_toGlued

Documentation

Each chart maps by an open immersion into the glued Picard scheme.

Source context 6 commands

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

universe w v u
namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra GoodReductionJacobian Opposite
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  {P : SubPicCondition c ε}
section glue
variable (hG : Presieve.IsSheaf (Scheme.zariskiTopology.over (Spec (CommRingCat.of R)))
    (relSubPicPresheaf c ε P))
  {ι : Type u} {X : ι → Scheme.{u}}
  (f : ∀ i, uliftYoneda.{u + 1}.obj (X i) ⟶ (relSubPicPresheaf c ε P).overTotal)
  (hf : ∀ i, MorphismProperty.presheafULift.{u + 1} @IsOpenImmersion (f i))
  [Presheaf.IsLocallySurjective Scheme.zariskiTopology (Limits.Sigma.desc f)]

Lean source · statement

instance isOpenImmersion_toGlued (i : ι) : IsOpenImmersion
    (Scheme.LocalRepresentabilityULift.toGlued (F := relSubPicTotalSheaf hG) (f := f) hf i :
      X i ⟶ (gluedDesignation hG f hf).P)

Module documentation

Gluing relative sub-Picard representations

Declarations