Mathlib Map

Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso],
  (∀ ⦃X Y S : AlgebraicGeometry.Scheme⦄ [inst : AlgebraicGeometry.IsAffine S] [inst_1 : AlgebraicGeometry.IsAffine X]
      (f : X ⟶ S) (g : Y ⟶ S), P g → P (CategoryTheory.Limits.pullback.fst f g)) →
    P.IsStableUnderBaseChange
Defined in
Mathlib.AlgebraicGeometry.Morphisms.Basic
Cited by
2 results in Mathlib
Foundations
Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.MorphismProperty.RespectsIso
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange · cited by 1HasRingHomProperty.isStab…AlgebraicGeometry.affineAnd_isStableUnderBaseChange · cited by 1AlgebraicGeometry.affineA…Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.Iso.inv · cited by 6514Iso.invAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCategoryTheory.Limits.pullback · cited by 864Limits.pullbackCategoryTheory.Limits.pullback.fst · cited by 639pullback.fstCategoryTheory.IsPullback · cited by 320CategoryTheory.IsPullbackCategoryTheory.MorphismProperty.RespectsIso · cited by 248MorphismProperty.Respects…AlgebraicGeometry.IsAffine · cited by 159AlgebraicGeometry.IsAffineCategoryTheory.IsPullback.isoPullback · cited by 42IsPullback.isoPullbackAlgebraicGeometry.AffineTargetMorphismProperty · cited by 31AlgebraicGeometry.AffineT…AlgebraicGeometry.AffineTargetMorphismProperty.toProperty · cited by 9AffineTargetMorphismPrope…AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso · cited by 8AffineTargetMorphismPrope…CategoryTheory.IsPullback.isoPullback_inv_fst · cited by 7IsPullback.isoPullback_in…AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange · cited by 4AffineTargetMorphismPrope…IsStableUnderBaseChange.mkCITED BYCITES

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.