Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 16:11 b7ed03f9

View on Github →

feat(algebraic_geometry): Open immersions of presheafed spaces (#10437)

Estimated changes

Created src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.LocallyRingedSpace.is_open_immersion

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app'

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.app_inv_app

added def algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app_app

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_inv_app

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_naturality

added def algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_hom_of_restrict

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_inv_of_restrict

added def algebraic_geometry.PresheafedSpace.is_open_immersion.open_functor

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_iso

added def algebraic_geometry.SheafedSpace.is_open_immersion

added def algebraic_geometry.is_open_immersion

Modified src/algebraic_geometry/stalks.lean

added theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_inv_eq_of_restrict

Modified src/topology/sheaves/stalks.lean

added theorem Top.presheaf.stalk_pushforward.stalk_pushforward_iso_of_open_embedding