chore(algebraic_geometry/open_immersion): split (#19149)

Split `algebraic_geometry/open_immersion` into a 1000-line file which doesn't mention schemes and a 1000-line file which does. This should open more porting targets (the first file should be available for porting immediately), but also helps towards a reorganization I have in mind for after-port: moving the [pre]sheafed-space and [locally-]ringed-space material from `algebraic_geometry` into a new folder in `topology` or `geometry`.
leanprover-community · Jun 5, 2023 · 533f62f · 533f62f
1 parent 1336155
commit 533f62f
Show file tree

Hide file tree

Showing 6 changed files with 1,089 additions and 1,062 deletions.
diff --git a/src/algebraic_geometry/AffineScheme.lean b/src/algebraic_geometry/AffineScheme.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import algebraic_geometry.Gamma_Spec_adjunction
-import algebraic_geometry.open_immersion
+import algebraic_geometry.open_immersion.Scheme
 import category_theory.limits.opposites
 import ring_theory.localization.inv_submonoid
 

diff --git a/src/algebraic_geometry/gluing.lean b/src/algebraic_geometry/gluing.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import algebraic_geometry.presheafed_space.gluing
+import algebraic_geometry.open_immersion.Scheme
 
 /-!
 # Gluing Schemes

diff --git a/src/algebraic_geometry/locally_ringed_space/has_colimits.lean b/src/algebraic_geometry/locally_ringed_space/has_colimits.lean
@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import algebraic_geometry.locally_ringed_space
 import algebra.category.Ring.constructions
-import algebraic_geometry.open_immersion
+import algebraic_geometry.open_immersion.basic
 import category_theory.limits.constructions.limits_of_products_and_equalizers
 
 /-!