AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_of_isProper_of_support_finite
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_exists_I_eq_of_isProper_of_support_finite
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_of_isProper_of_support_finite
{𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsProper f]
{k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ S)
(I : (pullback f x).IdealSheafData) (hfin : (I.support : Set ↥(pullback f x)).Finite) :
∃ (r : ℕ) (D : RelEffCartierDiv f r x), D.I = I