AlgebraicGeometry.RelPicard.smooth_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Smooth_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
attribute [-instance]
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp]
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
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
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfra GoodReductionJacobian AlgebraicGeometry.SmoothProperCurveLean source · statement
theorem
_root_.AlgebraicGeometry.RelPicard.smooth_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
(R : Type u) [CommRing R] [IsNoetherianRing 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)
(D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
[LocallyOfFiniteType D.toBase] :
Smooth D.toBase