Theorems · Theorem · algebraic geometry

AlgebraicGeometry.isPushout_appTop_of_isPullback

∀ {X Y Z P : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
  [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsAffine Z],
  CategoryTheory.IsPullback fst snd f g →
    CategoryTheory.IsPushout (AlgebraicGeometry.Scheme.Hom.appTop f) (AlgebraicGeometry.Scheme.Hom.appTop g)
      (AlgebraicGeometry.Scheme.Hom.appTop fst) (AlgebraicGeometry.Scheme.Hom.appTop snd)

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Affine

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsAffineAlgebraicGeometry.IsAffineAlgebraicGeometry.IsAffine