Module

Representation.lean

Nyll.JacobianVarieties.Picard.Representation

5 declarations indexed from sourceView source ↗

Module documentation

Universal families for relative sub-Picard conditions

A Poincaré family on a designated scheme classifies the line bundles satisfying a sub-Picard condition through unique maps over the base. Its restriction to the chosen zero section is trivial. The chosen classifying map is characterized by this universal property.

Imports3

Imported by177

structure

RepresentsRelSubPic

L36 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic

Documentation

A Poincaré family with a unique classifying map and a trivial zero-section restriction.

Source context 4 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra GoodReductionJacobian
universe u
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · full declaration

structure RepresentsRelSubPic (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (P : SubPicCondition c ε) (D : RelativePic0Designation R c) : Type (u + 1) where

  /-- The rigidified Poincaré family on the designated carrier. -/
  poincare : RigidifiedLineBundle c ε D.toBase
  /-- The Poincaré family satisfies the sub-Picard condition. -/
  poincare_mem : P.P D.toBase poincare

  /-- Every family satisfying the condition has a unique classifying map over the base. -/
  univ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c ε t), P.P t M →
    ∃! g : SchemeHomOver t D.toBase, Nonempty ((poincare.pullbackAlong g).L ≅ M.L)

  /-- The underlying line bundle pulled back to the zero section is the unit bundle. -/
  zero : Nonempty ((poincare.pullbackAlong ⟨D.zeroSection, D.zeroSection_toBase⟩).L ≅
    (RigidifiedLineBundle.unit (c := c) (ε := ε) (𝟙 _)).L)

def

classify

L60 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.classify

Documentation

Choose the unique map classifying a family satisfying the sub-Picard condition.

Source context 6 commands

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

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

Lean source · statement

def classify (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c ε t) (hM : P.P t M) : SchemeHomOver t D.toBase

theorem

classify_spec

L65 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.classify_spec

Source context 6 commands

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

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

Lean source · statement

theorem classify_spec (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c ε t) (hM : P.P t M) :
    Nonempty ((h.poincare.pullbackAlong (h.classify t M hM)).L ≅ M.L)

theorem

classify_unique

L71 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.classify_unique

Source context 6 commands

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

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

Lean source · statement

theorem classify_unique (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R))
    (M : RigidifiedLineBundle c ε t) (hM : P.P t M) (g : SchemeHomOver t D.toBase)
    (hg : Nonempty ((h.poincare.pullbackAlong g).L ≅ M.L)) : g = h.classify t M hM

theorem

ext_of_iso

L77 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.ext_of_iso

Source context 6 commands

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

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

Lean source · statement

theorem ext_of_iso (h : RepresentsRelSubPic c ε P D) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of R))
    (g g' : SchemeHomOver t D.toBase)
    (hgg' : Nonempty ((h.poincare.pullbackAlong g).L ≅
      (h.poincare.pullbackAlong g').L)) : g = g'

Module documentation

Universal families for relative sub-Picard conditions

Declarations

RepresentsRelSubPic

classify

classify_spec

classify_unique

ext_of_iso