Commit 2023-06-05 01:10 533f62f4
View on Github →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.
Estimated changes
deleted theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset
deleted theorem algebraic_geometry.PresheafedSpace.is_open_immersion.LocallyRingedSpace_to_LocallyRingedSpace
deleted theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_condition
deleted theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset
deleted theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_to_SheafedSpace
added theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset
added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.LocallyRingedSpace_to_LocallyRingedSpace
added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset
added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_to_SheafedSpace