AlgebraicGeometry.RelPicard.smooth_of_representsRelSubPic_algEquivZeroCut_of_twoAffineOpenCover
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard
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 GoodReductionJacobianLean source · statement
theorem smooth_of_representsRelSubPic_algEquivZeroCut_of_twoAffineOpenCover
(R : Type u) [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of
R))
(𝒱 : C.TwoAffineOpenCover)
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
[LocallyOfFiniteType D.toBase] :
Smooth D.toBase