Theorems · Theorem · algebraic geometry

AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback

∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q] {X Y U V : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {g : U ⟶ Y}
  [inst : AlgebraicGeometry.IsAffine U] [AlgebraicGeometry.IsOpenImmersion g] {iV : V ⟶ X} {f' : V ⟶ U},
  CategoryTheory.IsPullback iV f' f g → P.diagonal f → Q.diagonal f'

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Constructors

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.HasAffinePropertyAlgebraicGeometry.IsAffineAlgebraicGeometry.IsOpenImmersion