Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-24 07:29 558f5830

View on Github →

feat(src/algebraic_geometry/morphisms/quasi_separated): Define quasi-separated morphisms. (#17080)

Estimated changes

Modified src/algebraic_geometry/morphisms/quasi_compact.lean

added theorem algebraic_geometry.compact_space_iff_quasi_compact

added theorem algebraic_geometry.quasi_compact.affine_property_stable_under_base_change

added theorem algebraic_geometry.quasi_compact.is_local_at_target

added theorem algebraic_geometry.quasi_compact_stable_under_base_change

Created src/algebraic_geometry/morphisms/quasi_separated.lean

added theorem algebraic_geometry.is_affine_open.is_quasi_separated

added theorem algebraic_geometry.quasi_compact_affine_property_diagonal_eq

added theorem algebraic_geometry.quasi_compact_affine_property_iff_quasi_separated_space

added theorem algebraic_geometry.quasi_separated.affine_open_cover_iff

added theorem algebraic_geometry.quasi_separated.affine_open_cover_tfae

added def algebraic_geometry.quasi_separated.affine_property

added theorem algebraic_geometry.quasi_separated.affine_property_is_local

added theorem algebraic_geometry.quasi_separated.is_local_at_target

added theorem algebraic_geometry.quasi_separated.open_cover_iff

added theorem algebraic_geometry.quasi_separated.open_cover_tfae

added theorem algebraic_geometry.quasi_separated_eq_affine_property

added theorem algebraic_geometry.quasi_separated_eq_affine_property_diagonal

added theorem algebraic_geometry.quasi_separated_eq_diagonal_is_quasi_compact

added theorem algebraic_geometry.quasi_separated_of_comp

added theorem algebraic_geometry.quasi_separated_over_affine_iff

added theorem algebraic_geometry.quasi_separated_respects_iso

added theorem algebraic_geometry.quasi_separated_space_iff_affine

added theorem algebraic_geometry.quasi_separated_space_iff_quasi_separated

added theorem algebraic_geometry.quasi_separated_space_of_quasi_separated

added theorem algebraic_geometry.quasi_separated_stable_under_base_change

added theorem algebraic_geometry.quasi_separated_stable_under_composition