feat: port AlgebraicGeometry.PresheafedSpace.HasColimits (#4285)

leanprover-community · May 25, 2023 · 039deaf · 039deaf
1 parent 5e90989
commit 039deaf
Show file tree

Hide file tree

Showing 2 changed files with 479 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -351,6 +351,7 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.AlgebraicGeometry.PresheafedSpace
+import Mathlib.AlgebraicGeometry.PresheafedSpace.HasColimits
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal