chore: move (locally) ringed spaces out of AlgebraicGeometry (#7330)

Create new folder `Geometry.RingedSpace` for (locally) ringed spaces and move about half of the contents of `AlgebraicGeometry` there. Files renamed: ``` AlgebraicGeometry.OpenImmersion.Scheme → AlgebraicGeometry.OpenImmersion AlgebraicGeometry.RingedSpace → Geometry.RingedSpace.Basic AlgebraicGeometry.LocallyRingedSpace → Geometry.RingedSpace.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.HasColimits → Geometry.RingedSpace.LocallyRingedSpace.HasColimits AlgebraicGeometry.OpenImmersion.Basic → Geometry.RingedSpace.OpenImmersion AlgebraicGeometry.PresheafedSpace → Geometry.RingedSpace.PresheafedSpace AlgebraicGeometry.PresheafedSpace.Gluing → Geometry.RingedSpace.PresheafedSpace.Gluing AlgebraicGeometry.PresheafedSpace.HasColimits → Geometry.RingedSpace.PresheafedSpace.HasColimits AlgebraicGeometry.SheafedSpace → Geometry.RingedSpace.SheafedSpace AlgebraicGeometry.Stalks → Geometry.RingedSpace.Stalks ``` See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/split.20AlgebraicGeometry).
leanprover-community · Sep 23, 2023 · 8276aae · 8276aae
1 parent d0f7245
commit 8276aae
Show file tree

Hide file tree

Showing 15 changed files with 27 additions and 27 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -463,20 +463,14 @@ import Mathlib.AlgebraicGeometry.FunctionField
 import Mathlib.AlgebraicGeometry.GammaSpecAdjunction
 import Mathlib.AlgebraicGeometry.Gluing
 import Mathlib.AlgebraicGeometry.Limits
-import Mathlib.AlgebraicGeometry.LocallyRingedSpace
-import Mathlib.AlgebraicGeometry.LocallyRingedSpace.HasColimits
 import Mathlib.AlgebraicGeometry.Morphisms.Basic
 import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
 import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
-import Mathlib.AlgebraicGeometry.OpenImmersion.Basic
-import Mathlib.AlgebraicGeometry.OpenImmersion.Scheme
-import Mathlib.AlgebraicGeometry.PresheafedSpace
-import Mathlib.AlgebraicGeometry.PresheafedSpace.Gluing
-import Mathlib.AlgebraicGeometry.PresheafedSpace.HasColimits
+import Mathlib.AlgebraicGeometry.OpenImmersion
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
@@ -486,11 +480,8 @@ import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
 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
 import Mathlib.AlgebraicGeometry.Spec
-import Mathlib.AlgebraicGeometry.Stalks
 import Mathlib.AlgebraicGeometry.StructureSheaf
 import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
 import Mathlib.AlgebraicTopology.CechNerve
@@ -2026,6 +2017,15 @@ import Mathlib.Geometry.Manifold.VectorBundle.Pullback
 import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.VectorBundle.Tangent
 import Mathlib.Geometry.Manifold.WhitneyEmbedding
+import Mathlib.Geometry.RingedSpace.Basic
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
+import Mathlib.Geometry.RingedSpace.OpenImmersion
+import Mathlib.Geometry.RingedSpace.PresheafedSpace
+import Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
+import Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
+import Mathlib.Geometry.RingedSpace.SheafedSpace
+import Mathlib.Geometry.RingedSpace.Stalks
 import Mathlib.GroupTheory.Abelianization
 import Mathlib.GroupTheory.Archimedean
 import Mathlib.GroupTheory.ClassEquation

diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.GammaSpecAdjunction
-import Mathlib.AlgebraicGeometry.OpenImmersion.Scheme
+import Mathlib.AlgebraicGeometry.OpenImmersion
 import Mathlib.CategoryTheory.Limits.Opposites
 import Mathlib.RingTheory.Localization.InvSubmonoid
 

diff --git a/Mathlib/AlgebraicGeometry/Gluing.lean b/Mathlib/AlgebraicGeometry/Gluing.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.AlgebraicGeometry.PresheafedSpace.Gluing
-import Mathlib.AlgebraicGeometry.OpenImmersion.Scheme
+import Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
+import Mathlib.AlgebraicGeometry.OpenImmersion
 
 #align_import algebraic_geometry.gluing from "leanprover-community/mathlib"@"533f62f4dd62a5aad24a04326e6e787c8f7e98b1"
 

diff --git a/...gebraicGeometry/OpenImmersion/Scheme.lean → Mathlib/AlgebraicGeometry/OpenImmersion.lean b/...gebraicGeometry/OpenImmersion/Scheme.lean → Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.AlgebraicGeometry.OpenImmersion.Basic
+import Mathlib.Geometry.RingedSpace.OpenImmersion
 import Mathlib.AlgebraicGeometry.Scheme
 import Mathlib.CategoryTheory.Limits.Shapes.CommSq
 

diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
@@ -6,7 +6,7 @@ Authors: Jujian Zhang
 import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
 import Mathlib.Topology.Sheaves.LocalPredicate
 import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
-import Mathlib.AlgebraicGeometry.LocallyRingedSpace
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace
 
 #align_import algebraic_geometry.projective_spectrum.structure_sheaf from "leanprover-community/mathlib"@"486cb2f3bda4a67557c6285f5bd0c3348c1eea81"
 

diff --git a/Mathlib/AlgebraicGeometry/Spec.lean b/Mathlib/AlgebraicGeometry/Spec.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Justus Springer
 -/
-import Mathlib.AlgebraicGeometry.LocallyRingedSpace
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace
 import Mathlib.AlgebraicGeometry.StructureSheaf
 import Mathlib.RingTheory.Localization.LocalizationLocalization
 import Mathlib.Topology.Sheaves.SheafCondition.Sites

diff --git a/Mathlib/AlgebraicGeometry/RingedSpace.lean → Mathlib/Geometry/RingedSpace/Basic.lean b/Mathlib/AlgebraicGeometry/RingedSpace.lean → Mathlib/Geometry/RingedSpace/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Justus Springer, Andrew Yang
 -/
 import Mathlib.Algebra.Category.Ring.FilteredColimits
-import Mathlib.AlgebraicGeometry.SheafedSpace
+import Mathlib.Geometry.RingedSpace.SheafedSpace
 import Mathlib.Topology.Sheaves.Stalks
 import Mathlib.Algebra.Category.Ring.Colimits
 import Mathlib.Algebra.Category.Ring.Limits

diff --git a/...AlgebraicGeometry/LocallyRingedSpace.lean → ...metry/RingedSpace/LocallyRingedSpace.lean b/...AlgebraicGeometry/LocallyRingedSpace.lean → ...metry/RingedSpace/LocallyRingedSpace.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Mathlib.AlgebraicGeometry.RingedSpace
-import Mathlib.AlgebraicGeometry.Stalks
+import Mathlib.Geometry.RingedSpace.Basic
+import Mathlib.Geometry.RingedSpace.Stalks
 
 #align_import algebraic_geometry.locally_ringed_space from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
 

diff --git a/...metry/LocallyRingedSpace/HasColimits.lean → ...Space/LocallyRingedSpace/HasColimits.lean b/...metry/LocallyRingedSpace/HasColimits.lean → ...Space/LocallyRingedSpace/HasColimits.lean
@@ -3,9 +3,9 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.AlgebraicGeometry.LocallyRingedSpace
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace
 import Mathlib.Algebra.Category.Ring.Constructions
-import Mathlib.AlgebraicGeometry.OpenImmersion.Basic
+import Mathlib.Geometry.RingedSpace.OpenImmersion
 import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 
 #align_import algebraic_geometry.locally_ringed_space.has_colimits from "leanprover-community/mathlib"@"533f62f4dd62a5aad24a04326e6e787c8f7e98b1"

diff --git a/...lgebraicGeometry/OpenImmersion/Basic.lean → ...b/Geometry/RingedSpace/OpenImmersion.lean b/...lgebraicGeometry/OpenImmersion/Basic.lean → ...b/Geometry/RingedSpace/OpenImmersion.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
-import Mathlib.AlgebraicGeometry.LocallyRingedSpace
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace
 
 #align_import algebraic_geometry.open_immersion.basic from "leanprover-community/mathlib"@"533f62f4dd62a5aad24a04326e6e787c8f7e98b1"
 

diff --git a/...ib/AlgebraicGeometry/PresheafedSpace.lean → ...Geometry/RingedSpace/PresheafedSpace.lean b/...ib/AlgebraicGeometry/PresheafedSpace.lean → ...Geometry/RingedSpace/PresheafedSpace.lean
diff --git a/...braicGeometry/PresheafedSpace/Gluing.lean → ...y/RingedSpace/PresheafedSpace/Gluing.lean b/...braicGeometry/PresheafedSpace/Gluing.lean → ...y/RingedSpace/PresheafedSpace/Gluing.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.Topology.Gluing
-import Mathlib.AlgebraicGeometry.OpenImmersion.Basic
-import Mathlib.AlgebraicGeometry.LocallyRingedSpace.HasColimits
+import Mathlib.Geometry.RingedSpace.OpenImmersion
+import Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
 
 #align_import algebraic_geometry.presheafed_space.gluing from "leanprover-community/mathlib"@"533f62f4dd62a5aad24a04326e6e787c8f7e98b1"
 

diff --git a/...Geometry/PresheafedSpace/HasColimits.lean → ...gedSpace/PresheafedSpace/HasColimits.lean b/...Geometry/PresheafedSpace/HasColimits.lean → ...gedSpace/PresheafedSpace/HasColimits.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.AlgebraicGeometry.PresheafedSpace
+import Mathlib.Geometry.RingedSpace.PresheafedSpace
 import Mathlib.Topology.Category.TopCat.Limits.Basic
 import Mathlib.Topology.Sheaves.Limits
 

diff --git a/Mathlib/AlgebraicGeometry/SheafedSpace.lean → ...ib/Geometry/RingedSpace/SheafedSpace.lean b/Mathlib/AlgebraicGeometry/SheafedSpace.lean → ...ib/Geometry/RingedSpace/SheafedSpace.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.AlgebraicGeometry.PresheafedSpace.HasColimits
+import Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
 import Mathlib.Topology.Sheaves.Functors
 
 #align_import algebraic_geometry.sheafed_space from "leanprover-community/mathlib"@"f384f5d1a4e39f36817b8d22afff7b52af8121d1"

diff --git a/Mathlib/AlgebraicGeometry/Stalks.lean → Mathlib/Geometry/RingedSpace/Stalks.lean b/Mathlib/AlgebraicGeometry/Stalks.lean → Mathlib/Geometry/RingedSpace/Stalks.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.AlgebraicGeometry.PresheafedSpace
+import Mathlib.Geometry.RingedSpace.PresheafedSpace
 import Mathlib.CategoryTheory.Limits.Final
 import Mathlib.Topology.Sheaves.Stalks