NYLL
Module

RepresentsRelSubPicPresheaf.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPicPresheaf
6 declarations indexed from sourceView source ↗

Module documentation

Representations of the relative sub-Picard presheaf

A representing relative Picard designation classifies the permitted rigidified line-bundle classes and determines a representation of their presheaf. Conversely, a presheaf representation compatible with the zero class supplies the designation's universal bundle.

Imports3
Imported by53

Declarations

def

pullbackClass

L41 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.pullbackClass
Documentation

The permitted line-bundle class obtained by pulling back the universal bundle.

Source context 7 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 RepresentsRelSubPic
variable {P : SubPicCondition c ε} {D : RelativePic0Designation R c}
Lean source · statement
def pullbackClass (h : RepresentsRelSubPic c ε P D) (X : Over (Spec (CommRingCat.of R)))
    (g : X ⟶ Over.mk D.toBase) : (relSubPicPresheaf c ε P).obj (op X)
def

classifyClass

L47 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.classifyClass
Documentation

The classifying morphism of a permitted rigidified line-bundle class.

Source context 7 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 RepresentsRelSubPic
variable {P : SubPicCondition c ε} {D : RelativePic0Designation R c}
Lean source · statement
def classifyClass (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x : RigidifiedLineBundle.Classes c ε t)
    (hx : P.onClasses t x) :
    SchemeHomOver t D.toBase
theorem

eq_classifyClass

L53 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.eq_classifyClass
Source context 7 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 RepresentsRelSubPic
variable {P : SubPicCondition c ε} {D : RelativePic0Designation R c}
Lean source · statement
theorem eq_classifyClass (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x : RigidifiedLineBundle.Classes c ε t)
    (hx : P.onClasses t x)
    (g : SchemeHomOver t D.toBase) (hg : Quotient.mk _ (h.poincare.pullbackAlong g) = x) :
    g = h.classifyClass t x hx
theorem

mk_pullbackAlong_classifyClass

L62 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk_pullbackAlong_classifyClass
Source context 7 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 RepresentsRelSubPic
variable {P : SubPicCondition c ε} {D : RelativePic0Designation R c}
Lean source · statement
theorem mk_pullbackAlong_classifyClass (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R)) (x : RigidifiedLineBundle.Classes c ε t)
    (hx : P.onClasses t x) :
    Quotient.mk _ (h.poincare.pullbackAlong (h.classifyClass t x hx)) = x
def

representableBy

L70 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.representableBy
Documentation

The presheaf representation induced by the universal rigidified line bundle.

Source context 7 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 RepresentsRelSubPic
variable {P : SubPicCondition c ε} {D : RelativePic0Designation R c}
Lean source · full declaration
def representableBy (h : RepresentsRelSubPic c ε P D) :
    (relSubPicPresheaf c ε P).RepresentableBy (Over.mk D.toBase) where
  homEquiv {X} :=
    { toFun := fun g => h.pullbackClass X g
      invFun := fun x =>
        Over.homMk (h.classifyClass X.hom x.1 x.2).1 (h.classifyClass X.hom x.1 x.2).2
      left_inv := fun g => Over.OverMorphism.ext (congrArg Subtype.val
        (h.eq_classifyClass X.hom _ _ ⟨g.left, Over.w g⟩ rfl)).symm
      right_inv := fun x => Subtype.ext (h.mk_pullbackAlong_classifyClass X.hom x.1 x.2) }
  homEquiv_comp {X X'} f g := by
    apply Subtype.ext
    apply Quotient.sound
    exact ⟨(h.poincare.pullbackAlongPullbackAlongIso ⟨g.left, Over.w g⟩ ⟨f.left, Over.w f⟩).symm⟩
theorem

nonempty_of_representableBy

L91 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_of_representableBy
Source context 7 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 RepresentsRelSubPic
variable {P : SubPicCondition c ε} {D : RelativePic0Designation R c}
Lean source · statement
theorem nonempty_of_representableBy
    (e : (relSubPicPresheaf c ε P).RepresentableBy (Over.mk D.toBase))
    (h0 : (e.homEquiv (Over.homMk D.zeroSection D.zeroSection_toBase :
        Over.mk (𝟙 (Spec (CommRingCat.of R))) ⟶ Over.mk D.toBase)).1 =
      relPicardPresheaf.unitClass c ε (Over.mk (𝟙 _))) :
    Nonempty (RepresentsRelSubPic c ε P D)

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