NYLL
Module

RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
10 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Faithfully flat affine pullback descends a relative effective Cartier divisor, using the tensor- product kernel formula.

Imports19
Imported by2

Declarations

theorem

ker_algebraMap_eq_map_ker

L55 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.Algebra.IsPushout.ker_algebraMap_eq_map_ker
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace Algebra
open _root_.Algebra
namespace IsPushout
open _root_.Algebra.IsPushout
open _root_.Algebra
Lean source · statement
theorem ker_algebraMap_eq_map_ker
    (R B C P : Type*) [CommRing R] [CommRing B] [CommRing C] [CommRing P]
    [Algebra R B] [Algebra R C] [Algebra B P] [Algebra C P] [Algebra R P]
    [IsScalarTower R B P] [IsScalarTower R C P] [Algebra.IsPushout R B C P]
    (hC : Function.Surjective (algebraMap R C)) :
    RingHom.ker (algebraMap B P) = (RingHom.ker (algebraMap R C)).map (algebraMap R B)
theorem

ker_eq_map_ker_of_isPushout

L97 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.CommRingCat.ker_eq_map_ker_of_isPushout
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace CommRingCat
open _root_.CommRingCat
Lean source · statement
theorem ker_eq_map_ker_of_isPushout {R B C P : CommRingCat.{u}} {f : R ⟶ B} {g : R ⟶ C}
    {inl : B ⟶ P} {inr : C ⟶ P} (h : IsPushout f g inl inr)
    (hg : Function.Surjective g.hom) :
    RingHom.ker inl.hom = (RingHom.ker g.hom).map f.hom
theorem

ideal_comap_top

L121 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_top
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}
Lean source · statement
theorem ideal_comap_top [IsAffine X] [IsAffine Y] (I : X.IdealSheafData) (f : Y ⟶ X) :
    (I.comap f).ideal ⟨⊤, isAffineOpen_top Y⟩ =
      (I.ideal ⟨⊤, isAffineOpen_top X⟩).map f.appTop.hom
theorem

ideal_comap_of_le

L132 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_le
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}
Lean source · statement
theorem ideal_comap_of_le (I : X.IdealSheafData) (f : Y ⟶ X) (U : X.affineOpens)
    (V : Y.affineOpens) (hVU : (V : Y.Opens) ≤ f ⁻¹ᵁ (U : X.Opens)) :
    (I.comap f).ideal V = (I.ideal U).map (f.appLE U V hVU).hom
theorem

ideal_comap_of_isAffineHom

L168 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isAffineHom
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}
Lean source · statement
theorem ideal_comap_of_isAffineHom (I : X.IdealSheafData) (f : Y ⟶ X) [IsAffineHom f]
    (U : X.affineOpens) :
    (I.comap f).ideal ⟨f ⁻¹ᵁ U, U.2.preimage f⟩ = (I.ideal U).map (f.app U).hom
lemma

codescendsAlong_faithfullyFlat'

L182 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.RingHom.Flat.codescendsAlong_faithfullyFlat'
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
open scoped _root_.RingHom _root_.RingHom.Flat in
Lean source · full declaration
lemma RingHom.Flat.codescendsAlong_faithfullyFlat' :
    RingHom.CodescendsAlong (fun f => RingHom.Flat f) (fun f => RingHom.FaithfullyFlat f) := by
  refine RingHom.CodescendsAlong.mk _ RingHom.Flat.respectsIso ?_
  intro R S T _ _ _ _ _ h H
  rw [RingHom.faithfullyFlat_algebraMap_iff] at h
  rw [RingHom.flat_algebraMap_iff] at H ⊢
  exact Module.Flat.of_flat_tensorProduct R T S
instance

descendsAlong_surjective_inf_flat_inf_quasicompact'

L196 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.AlgebraicGeometry.Flat.descendsAlong_surjective_inf_flat_inf_quasicompact'
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
open scoped _root_.AlgebraicGeometry _root_.AlgebraicGeometry.Flat in
Lean source · statement
instance AlgebraicGeometry.Flat.descendsAlong_surjective_inf_flat_inf_quasicompact' :
    MorphismProperty.DescendsAlong @AlgebraicGeometry.Flat
      (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
lemma

isPullback_mapOnProdOver_kernelPair

L217 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.AlgebraicGeometry.RelEffCartierDiv.AffineDescent.isPullback_mapOnProdOver_kernelPair
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace AffineDescent
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} [IsAffine 𝒞] [IsAffine S] {f : 𝒞 ⟶ S} {r : ℕ}
  {X Y R : Scheme.{u}} [IsAffine X] [IsAffine Y] {gX : X ⟶ S} {gY : Y ⟶ S} {gR : R ⟶ S}
  (p : X ⟶ Y) (hp : p ≫ gY = gX)
  (s t : R ⟶ X) (hs : s ≫ gX = gR) (ht : t ≫ gX = gR) (hR : IsPullback s t p p)
include hR in
omit [IsAffine 𝒞] [IsAffine S] [IsAffine X] [IsAffine Y] in
Lean source · statement
lemma isPullback_mapOnProdOver_kernelPair :
    IsPullback (mapOnProdOver f s hs) (mapOnProdOver f t ht)
      (mapOnProdOver f p hp) (mapOnProdOver f p hp)
lemma

faithfullyFlat_appTop_mapOnProdOver

L231 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine.AlgebraicGeometry.RelEffCartierDiv.AffineDescent.faithfullyFlat_appTop_mapOnProdOver
Source context 16 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace AffineDescent
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} [IsAffine 𝒞] [IsAffine S] {f : 𝒞 ⟶ S} {r : ℕ}
  {X Y R : Scheme.{u}} [IsAffine X] [IsAffine Y] {gX : X ⟶ S} {gY : Y ⟶ S} {gR : R ⟶ S}
  (p : X ⟶ Y) (hp : p ≫ gY = gX)
  (s t : R ⟶ X) (hs : s ≫ gX = gR) (ht : t ≫ gX = gR) (hR : IsPullback s t p p)
variable [IsFinite p] [Flat p] [Surjective p]
include hp in
omit [IsFinite p] in
Lean source · full declaration
lemma faithfullyFlat_appTop_mapOnProdOver :
    letI := (mapOnProdOver f p hp).appTop.hom.toAlgebra
    Module.FaithfullyFlat Γ(pullback f gY, ⊤) Γ(pullback f gX, ⊤) := by
  have : IsAffine (pullback f gY) := isAffine_of_isAffineHom (pullback.snd f gY)
  have : IsAffine (pullback f gX) := isAffine_of_isAffineHom (pullback.snd f gX)
  set π := mapOnProdOver f p hp
  have : Flat π := MorphismProperty.of_isPullback (isPullback_mapOnProdOver f p hp).flip
    inferInstance
  have : Surjective π :=
    MorphismProperty.of_isPullback (isPullback_mapOnProdOver f p hp).flip inferInstance
  let := π.appTop.hom.toAlgebra
  have : Module.Flat Γ(pullback f gY, ⊤) Γ(pullback f gX, ⊤) := Scheme.Hom.flat_appTop π
  refine Module.FaithfullyFlat.of_comap_surjective ?_
  have hsurj : Surjective (Spec.map π.appTop) := by
    have : Spec.map π.appTop = (pullback f gX).isoSpec.inv ≫ π ≫ (pullback f gY).isoSpec.hom := by
      rw [← Scheme.isoSpec_hom_naturality, Iso.inv_hom_id_assoc]
    rw [this]
    infer_instance
  exact hsurj.surj
theorem

existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine

L258 ↗
AlgebraicGeometry.RelEffCartierDiv.existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
open _root_.AlgebraicGeometry in
with_weak_namespace _root_.AlgebraicCurves.RelativeDivisors.Proofs
with_weak_namespace RelEffCartierDiv_existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
with_weak_namespace AlgebraicGeometry
open RelEffCartierDiv.AffineDescent in
Lean source · statement
theorem
  _root_.AlgebraicGeometry.RelEffCartierDiv.existsUnique_pullbackAlong_eq_of_isPullback_of_isAffine
    {𝒞 S : Scheme.{u}} [IsAffine 𝒞] [IsAffine S] {f : 𝒞 ⟶ S} {r : ℕ}
    {X Y R : Scheme.{u}} [IsAffine X] [IsAffine Y] {gX : X ⟶ S} {gY : Y ⟶ S} {gR : R ⟶ S}
    (p : X ⟶ Y) (hp : p ≫ gY = gX)
    [IsFinite p] [Flat p] [LocallyOfFinitePresentation p] [Surjective p]
    (s t : R ⟶ X) (hs : s ≫ gX = gR) (ht : t ≫ gX = gR) (hR : IsPullback s t p p)
    (D : RelEffCartierDiv f r gX) (hD : D.pullbackAlong s hs = D.pullbackAlong t ht) :
    ∃! DY : RelEffCartierDiv f r gY, DY.pullbackAlong p hp = D

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.