Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-25 21:05 abf96572

View on Github →

feat(algebraic_geometry): Results about open immersions of schemes. (#10977)

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

deleted def algebraic_geometry.Scheme.to_LocallyRingedSpace

modified structure algebraic_geometry.Scheme

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.LocallyRingedSpace.is_open_immersion.iso_restrict

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.Scheme_eq_of_LocallyRingedSpace_eq

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.Scheme_to_Scheme

added def algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme

added def algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_hom_val

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.to_Scheme_to_LocallyRingedSpace

added theorem algebraic_geometry.Scheme.affine_basis_cover_obj

added def algebraic_geometry.Scheme.affine_basis_cover_ring