NYLL
Module

surjective_toBase_of_representsRelSubPic_algEquivZeroCut.lean

Nyll.JacobianVarieties.Picard.surjective_toBase_of_representsRelSubPic_algEquivZeroCut
1 declaration indexed from sourceView source ↗

Module documentation

The zero section makes the structure map of the representing Picard scheme surjective.

Imports4
Imported by2

Declarations

theorem

surjective_toBase_of_representsRelSubPic_algEquivZeroCut

L32 ↗
AlgebraicGeometry.RelPicard.surjective_toBase_of_representsRelSubPic_algEquivZeroCut
Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardStructureSurjective
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
Lean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.surjective_toBase_of_representsRelSubPic_algEquivZeroCut
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (D : RelativePic0Designation R c) (_h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) :
    Surjective D.toBase

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