AlgebraicGeometry.RelEffCartierDiv.IsUniversal.isProper
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_IsUniversal_isProper
attribute [-instance]
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
attribute [-simp]
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 AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.IsUniversal.isProper
{𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsProper f] [SmoothOfRelativeDimension 1 f]
[IsLocallyNoetherian S] {r : ℕ} {Y : Scheme.{u}} {y : Y ⟶ S}
{Duniv : RelEffCartierDiv f r y} (hU : Duniv.IsUniversal) : IsProper y