Module

Exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isReduced.lean

Nyll.JacobianVarieties.Picard.Exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isReduced

1 declaration indexed from sourceView source ↗

Module documentation

Picard representability over a reduced base

Open Picard charts glue to a smooth proper geometrically connected representing scheme.

Imports16

Imported by4

theorem

exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isReduced

L546 ↗

AlgebraicGeometry.RelPicard.exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isReduced

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open _root_.JacobianVarieties.Picard.Proofs.ReducedFiniteRepresentation
universe u
open  _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
  _root_.AlgebraicGeometry.RelPicard
  _root_.NeronModelInfra _root_.GoodReductionJacobian _root_.AlgebraicGeometry.SmoothProperCurve

Lean source · statement

theorem exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isReduced
    (R : Type u) [CommRing R] [IsNoetherianRing R] [_root_.IsReduced R] {C : Scheme.{u}} (c : C ⟶
      Spec (CommRingCat.of R))
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : SmoothProperCurve.FiniteMapData c ε, m₀ ≤ 𝔉.m)
    (n g r : ℕ) (hgr : 2 * g < r)
    (γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (hγ : HasChartSections c γ) :
    ∃ D : RelativePic0Designation R c,
      Nonempty (RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) ∧
        Smooth D.toBase ∧ IsProper D.toBase ∧ GeometricallyConnected D.toBase

Module documentation

Picard representability over a reduced base

Declarations

exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isReduced