AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_zeroSchemeIdeal_of_ne_zero_of_isProper
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_exists_I_eq_zeroSchemeIdeal_of_ne_zero_of_isProper
attribute [-instance]
AlgebraicCurve.Place.instIsScalarTowerSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Divisor.instDistribMulActionAlgEquiv
AlgebraicCurve.Place.instSMulAlgEquiv
AlgebraicCurve.Place.instIsPrincipalIdealRingSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Place.instIsDiscreteValuationRingSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Pic0.instDistribMulActionAlgEquiv
AlgebraicCurve.Place.instAlgebraSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Place.instMulActionAlgEquiv
AlgebraicCurve.Pic0.instSMulAlgEquiv
AlgebraicCurve.CurveModel.isProper
AlgebraicCurve.CurveModel.isIntegral
AlgebraicCurve.CurveModel.smooth
attribute [-simp]
AlgebraicCurve.Place.mk.injEq
AlgebraicCurve.Divisor.degree_single
AlgebraicCurve.Divisor.smul_single
AlgebraicCurve.Place.smul_toValuationSubring
AlgebraicCurve.Place.heightOneSpectrum_asIdeal
AlgebraicCurve.Place.coe_algebraMap
AlgebraicCurve.Place.ord_one
AlgebraicCurve.Place.coe_smulRingEquiv_apply
AlgebraicCurve.Pic0.coe_degZeroSMulHom
AlgebraicCurve.Place.deg_smul
AlgebraicCurve.Pic0.mk_zero
AlgebraicCurve.Place.mk.sizeOf_spec
AlgebraicCurve.Divisor.degree_smul
AlgebraicCurve.Pic0.mk_add
AlgebraicCurve.Place.ord_zero
AlgebraicCurve.Place.ofHeightOneSpectrum_toValuationSubring
AlgebraicCurve.CurveModel.mk.injEq
AlgebraicCurve.CurveModel.mk.sizeOf_spec
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpaceLean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_zeroSchemeIdeal_of_ne_zero_of_isProper
{𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsProper f] [SmoothOfRelativeDimension 1 f]
[GeometricallyIrreducible f]
{k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ S)
{M : (pullback f x).Modules} (hM : Scheme.Modules.IsInvertible M)
(s : 𝟙_ (pullback f x).Modules ⟶ M) (hs : s ≠ 0) :
∃ (r : ℕ) (D : RelEffCartierDiv f r x), D.I = Scheme.Modules.zeroSchemeIdeal s