AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_ker_and_pullbackAlong_eq_and_saturated_of_isDiscreteValuationRing
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SaturatedCartierDVR
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.IdealSheafData in
open _root_.AlgebraicGeometry.IdealSheafData in
with_weak_namespace _root_.AlgebraicGeometry.RelEffCartierDivLean source · statement
theorem exists_I_eq_ker_and_pullbackAlong_eq_and_saturated_of_isDiscreteValuationRing
{𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsProper f]
{O : Type u} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
(g : Spec (CommRingCat.of O) ⟶ S)
(T' : Type u) [Field T'] [Algebra O T'] [IsFractionRing O T']
{gT : Spec (CommRingCat.of T') ⟶ S}
(hψ : Spec.map (CommRingCat.ofHom (algebraMap O T')) ≫ g = gT)
{r : ℕ} (E : RelEffCartierDiv f r gT) :
∃ Ebar : RelEffCartierDiv f r g,
Ebar.I = (E.I.subschemeι ≫
mapOnProdOver f (Spec.map (CommRingCat.ofHom (algebraMap O T'))) hψ).ker ∧
Ebar.pullbackAlong (Spec.map (CommRingCat.ofHom (algebraMap O T'))) hψ = E ∧
∀ (ϖ : O), Irreducible ϖ → ∀ (U : (pullback f g).affineOpens) (s : Γ(pullback f g, U)),
(pullback f g).presheaf.map (homOfLE (le_top : (U : (pullback f g).Opens) ≤ ⊤)).op
((pullback.snd f g).appTop ((Scheme.ΓSpecIso (CommRingCat.of O)).inv ϖ)) * s ∈
Ebar.I.ideal U →
s ∈ Ebar.I.ideal U