Nyll.SchemeTheory.Affine.FaithfullyFlatSectionSurjectivity

theorem

surjective_of_isPushout_of_faithfullyFlat

CommRingCat.surjective_of_isPushout_of_faithfullyFlat

Documentation

Surjectivity descends across an actual faithfully flat ring pushout.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace CommRingCat
universe u

Lean source · statement

theorem surjective_of_isPushout_of_faithfullyFlat
    {R S A B : CommRingCat.{u}} (f : R ⟶ S) (g : R ⟶ A)
    (i : S ⟶ B) (j : A ⟶ B) (h : IsPushout f g i j)
    (hg : g.hom.FaithfullyFlat) (hj : Function.Surjective j) :
    Function.Surjective f

theorem

surjective_appTop_of_affine_faithfullyFlat_baseChange

L54 ↗

AlgebraicGeometry.surjective_appTop_of_affine_faithfullyFlat_baseChange

Documentation

Surjectivity of the actual map on global sections is detected after an affine faithfully flat base change of the common affine base.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u

Lean source · full declaration

theorem surjective_appTop_of_affine_faithfullyFlat_baseChange
    {Y X S T : Scheme.{u}} (h : Y ⟶ X) (f : X ⟶ S) (g : T ⟶ S)
    [IsAffine S] [IsAffine T] [QuasiCompact f] [QuasiSeparated f]
    [QuasiCompact (h ≫ f)] [QuasiSeparated (h ≫ f)] [Flat g] [Surjective g]
    (hSurjective : Function.Surjective
      (pullback.map (h ≫ f) g f g h (𝟙 T) (𝟙 S)
        (by rw [Category.comp_id]) (by rw [Category.id_comp, Category.comp_id])).appTop) :
    Function.Surjective h.appTop := by
  let t : pullback (h ≫ f) g ⟶ pullback f g :=
    pullback.map (h ≫ f) g f g h (𝟙 T) (𝟙 S)
      (by rw [Category.comp_id]) (by rw [Category.id_comp, Category.comp_id])
  have ht₁ : t ≫ pullback.fst f g = pullback.fst (h ≫ f) g ≫ h :=
    pullback.lift_fst _ _ _
  have ht₂ : t ≫ pullback.snd f g = pullback.snd (h ≫ f) g := by
    exact (pullback.lift_snd _ _ _).trans (Category.comp_id _)
  have hSquare : h.appTop ≫ (pullback.fst (h ≫ f) g).appTop =
      (pullback.fst f g).appTop ≫ t.appTop := by
    rw [← Scheme.Hom.comp_appTop, ← Scheme.Hom.comp_appTop, ht₁]
  have hBottom : (pullback.snd (h ≫ f) g).appTop =
      (pullback.snd f g).appTop ≫ t.appTop := by
    rw [← Scheme.Hom.comp_appTop, ht₂]
  have hOuter := isPushout_appTop_of_flat (h ≫ f) g
  rw [Scheme.Hom.comp_appTop, hBottom] at hOuter
  have hPushout : IsPushout h.appTop (pullback.fst f g).appTop
      (pullback.fst (h ≫ f) g).appTop t.appTop :=
    hOuter.of_left hSquare (isPushout_appTop_of_flat f g)
  have hFpqc := fpqc_SpecMap_pullback_fst_appTop f g
  have hFaithful : (pullback.fst f g).appTop.hom.FaithfullyFlat :=
    (flat_and_surjective_SpecMap_iff (pullback.fst f g).appTop).mp
      ⟨hFpqc.1.2, hFpqc.1.1⟩
  exact CommRingCat.surjective_of_isPushout_of_faithfullyFlat
    h.appTop (pullback.fst f g).appTop (pullback.fst (h ≫ f) g).appTop t.appTop
    hPushout hFaithful hSurjective

FaithfullyFlatSectionSurjectivity.lean

Module documentation

Faithfully flat descent of surjectivity on actual global sections

surjective_of_isPushout_of_faithfullyFlat

surjective_appTop_of_affine_faithfullyFlat_baseChange

Module documentation

Faithfully flat descent of surjectivity on actual global sections

Declarations

surjective_of_isPushout_of_faithfullyFlat

surjective_appTop_of_affine_faithfullyFlat_baseChange