feat: port AlgebraicGeometry.PresheafedSpace (#4093)

leanprover-community · May 21, 2023 · 6d77e3b · 6d77e3b
1 parent d3369c5
commit 6d77e3b
Show file tree

Hide file tree

Showing 2 changed files with 600 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -331,6 +331,7 @@ import Mathlib.Algebra.TrivSqZeroExt
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.AlgebraicGeometry.PresheafedSpace
 import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
 import Mathlib.AlgebraicTopology.CechNerve
 import Mathlib.AlgebraicTopology.DoldKan.Compatibility