feat: port AlgebraicGeometry.Pullbacks (#5583)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
leanprover-community · Jun 29, 2023 · 80d2e74 · 80d2e74
1 parent eef7daf
commit 80d2e74
Show file tree

Hide file tree

Showing 2 changed files with 720 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -430,6 +430,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian
 import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
 import Mathlib.AlgebraicGeometry.Properties
+import Mathlib.AlgebraicGeometry.Pullbacks
 import Mathlib.AlgebraicGeometry.RingedSpace
 import Mathlib.AlgebraicGeometry.Scheme
 import Mathlib.AlgebraicGeometry.SheafedSpace