Module

IsLFPInj_relSubPicPresheaf_algEquivZeroCut.lean

Nyll.JacobianVarieties.Picard.IsLFPInj_relSubPicPresheaf_algEquivZeroCut

2 declarations indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Transfer finite-presentation injectivity from the relative Picard presheaf to its algebraically trivial cut.

Imports9

Imported by2

theorem

isLFPInj_relSubPicPresheaf_of_relPicardPresheaf

L83 ↗

JacobianVarieties.Picard.Proofs.IsLFPInj_relSubPicPresheaf_algEquivZeroCut.AlgebraicGeometry.RelPicard.isLFPInj_relSubPicPresheaf_of_relPicardPresheaf

Source context 29 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLFPInj_relSubPicPresheaf_algEquivZeroCut
attribute [-instance] AlgebraicGeometry.FGSubalgebra.tensorStage_directedSystem
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instIsDirectedLe
attribute [-instance]
  instQuasiSeparatedSpaceCarrierCarrierCommRingCatObjOppositeSchemeSpecDiagram
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instIsCofilteredOpposite
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instIsAffineObjOppositeSchemeSpecDiagram
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instNonempty
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instNonemptySubtypeLeSubalgebraValFG
attribute [-instance]
  instCompactSpaceCarrierCarrierCommRingCatObjOppositeSchemeSpecDiagram
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instIsDirectedSubtypeLeSubalgebraValFG
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instIsAffineHomMapOppositeSchemeSpecDiagram
attribute [-instance] AlgebraicGeometry.FGSubalgebra.instIsFiltered
attribute [-instance] AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
attribute [-instance] AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
attribute [-instance] AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
attribute [-instance] AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
attribute [-instance] AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
attribute [-instance] AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp] AlgebraicGeometry.FGSubalgebra.cocone_ι_app_apply
  AlgebraicGeometry.RelPicard.LFP.stageHom_val
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.AffineLimit
open scoped AlgebraicGeometry AlgebraicGeometry.RelPicard in

Lean source · statement

theorem AlgebraicGeometry.RelPicard.isLFPInj_relSubPicPresheaf_of_relPicardPresheaf
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (P : SubPicCondition c ε)
    (h : AffineLimit.IsLFPInj (relPicardPresheaf c ε)) :
    AffineLimit.IsLFPInj (relSubPicPresheaf c ε P)

theorem