AlgebraicGeometry.RelEffCartierDiv.exists_supportedIn_universal_of_smooth_opens
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_exists_supportedIn_universal_of_smooth_opens
attribute [-instance]
AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
AlgebraicGeometry.isClosedImmersion_graphOver
instNeg
instSMulInt
instAddCommGroup
instAdd
instSub
instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
instSMulNat
instZero
attribute [-simp] AlgebraicGeometry.prodKerGraph_one AlgebraicGeometry.fibrePowOver.proj_comp
AlgebraicGeometry.prodKerGraph_zero AlgebraicGeometry.RelEffCartierDiv.empty_I
AlgebraicGeometry.fibrePowOver.proj_comp_assoc AlgebraicGeometry.graphOver_fst_assoc
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc AlgebraicGeometry.graphOver_fst
AlgebraicGeometry.RelEffCartierDiv.ofPoint_I AlgebraicGeometry.graphOver_snd
AlgebraicGeometry.graphOver_snd_assoc AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
AlgebraicCurve.SymmetricPowerPackage.mk.injEq
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelEffCartierDivLean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.exists_supportedIn_universal_of_smooth_opens
{𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) [IsSeparated f] (U : 𝒞.Opens)
[SmoothOfRelativeDimension 1 (U.ι ≫ f)]
(hcov : ∀ (V : S.affineOpens) (F : Finset ↥U), (∀ x ∈ F, (U.ι ≫ f) x ∈ (V : S.Opens)) →
∃ W : (↑U : Scheme.{u}).Opens, IsAffineOpen W ∧ W ≤ (U.ι ≫ f) ⁻¹ᵁ (V : S.Opens) ∧ ∀ x ∈ F, x
∈ W)
(r : ℕ) :
∃ (Y : Scheme.{u}) (y : Y ⟶ S) (Duniv : RelEffCartierDiv f r y), Duniv.SupportedIn U ∧
∀ ⦃T : Scheme.{u}⦄ (g : T ⟶ S) (D : RelEffCartierDiv f r g), D.SupportedIn U →
∃! φ : {φ : T ⟶ Y // φ ≫ y = g}, PullsBackOver Duniv φ.1 φ.2 D