feat: port AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (#5224)

Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
leanprover-community · Jul 7, 2023 · be46ce4 · be46ce4
1 parent c6660d9
commit be46ce4
Show file tree

Hide file tree

Showing 2 changed files with 417 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -442,6 +442,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian
+import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
 import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
 import Mathlib.AlgebraicGeometry.Properties
 import Mathlib.AlgebraicGeometry.Pullbacks