AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_of_flat_of_comap_mapOnProdOver_eq_of_isDiscreteValuationRing
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ExtendCartierDVR
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
with_weak_namespace _root_.AlgebraicGeometry.RelEffCartierDivLean source · statement
theorem exists_I_eq_of_flat_of_comap_mapOnProdOver_eq_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)
(J : (pullback f g).IdealSheafData) [Flat (J.subschemeι ≫ pullback.snd f g)]
(hJ : J.comap (mapOnProdOver f (Spec.map (CommRingCat.ofHom (algebraMap O T'))) hψ) = E.I) :
∃ Ebar : RelEffCartierDiv f r g, Ebar.I = J ∧
Ebar.pullbackAlong (Spec.map (CommRingCat.ofHom (algebraMap O T'))) hψ = E