Theorems · Definition · algebraic geometry

AlgebraicGeometry.pushoutSection

{X Y S T : AlgebraicGeometry.Scheme} →
  {f : T ⟶ S} →
    {g : Y ⟶ X} →
      {iX : X ⟶ S} →
        {iY : Y ⟶ T} →
          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} →
                        UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT →
                          (CategoryTheory.Limits.pushout (AlgebraicGeometry.Scheme.Hom.appLE iX US UX hUSX)
                              (AlgebraicGeometry.Scheme.Hom.appLE f US UT hUST) ⟶
                            Y.presheaf.obj (Opposite.op UY))

The canonical map Γ(X, Uₓ) ⊗[Γ(S, Uₛ)] Γ(T, Uₜ) ⟶ Γ(X ×ₛ T, pr₁ ⁻¹ Uₓ ∩ pr₂ ⁻¹ Uₜ). This is an isomorphism under various circumstances.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Flat

Cited by

12 results in Mathlib

Foundations

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