Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-24 00:43 36ba1acd

View on Github →

feat(algebraic_geometry): Define open_covers of Schemes. (#10931)

Estimated changes

Created src/algebra/category/CommRing/instances.lean

Modified src/algebraic_geometry/Scheme.lean

added def algebraic_geometry.Scheme.forget_to_LocallyRingedSpace

added def algebraic_geometry.Scheme.forget_to_Top

Modified src/algebraic_geometry/locally_ringed_space.lean

modified def algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

added def algebraic_geometry.LocallyRingedSpace.forget_to_Top

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.Scheme.affine_basis_cover

added theorem algebraic_geometry.Scheme.affine_basis_cover_is_basis

added theorem algebraic_geometry.Scheme.affine_basis_cover_map_range

added def algebraic_geometry.Scheme.affine_basis_cover_of_affine

added def algebraic_geometry.Scheme.affine_cover

added def algebraic_geometry.Scheme.open_cover.bind

added structure algebraic_geometry.Scheme.open_cover

added theorem algebraic_geometry.is_open_immersion.open_range