Commit 2021-12-18 18:09 ecec43a2

View on Github →

feat(algebraic_geometry/open_immersion): Easy results about open immersions. (#10776)

Estimated changes

Modified src/algebraic_geometry/open_immersion.lean

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.LocallyRingedSpace_to_LocallyRingedSpace

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.SheafedSpace_to_SheafedSpace

added def algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace

added def algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_hom_val

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_LocallyRingedSpace_to_SheafedSpace

added def algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace

added def algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom_base

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_hom_c

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_SheafedSpace_to_PresheafedSpace

added theorem algebraic_geometry.SheafedSpace.is_open_immersion.of_stalk_iso