Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isPullback

∀ {X Y Z S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {pX : Z ⟶ X} {pY : Z ⟶ Y},
  CategoryTheory.IsPullback pX pY f g →
    ∀ [AlgebraicGeometry.IsSchemeTheoreticallyDominant f] [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.Flat g],
      AlgebraicGeometry.IsSchemeTheoreticallyDominant pY

Defined in: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Cited by: 0 results in Mathlib
Foundations: Depth 235 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AlgebraicGeometry.IsSchemeTheoreticallyDominant AlgebraicGeometry.QuasiCompact AlgebraicGeometry.Flat

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites7

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

Quiver.Homstatement and proof · cited by 32,603
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CategoryTheory.IsPullbackstatement and proof · cited by 320
AlgebraicGeometry.QuasiCompactstatement and proof · cited by 102
AlgebraicGeometry.Flatstatement and proof · cited by 49
CategoryTheory.IsPullback.isoPullback_hom_sndproof · cited by 11
AlgebraicGeometry.IsSchemeTheoreticallyDominantstatement and proof · cited by 9

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.