Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq

∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  {ι : Type u} [Finite ι] (VX : ι → X.Opens) (hVU : iSup VX = UX),
  (∀ (i : ι), CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST ⋯ ⋯)) →
    (∀ (i j : ι), CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST ⋯ ⋯)) →
      (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f US UT hUST)).Flat →
        CategoryTheory.IsIso (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Flat

Cited by

2 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Finite