Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 01:42 9b298fea

View on Github →

feat(algebraic_geometry): Being quasi-compact is a local property. (#15995)

Estimated changes

Modified src/algebraic_geometry/morphisms/basic.lean

deleted theorem algebraic_geometry.affine_target_morphism_property.is_local.open_cover_iff

added theorem algebraic_geometry.affine_target_morphism_property.respects_iso_mk

added theorem algebraic_geometry.property_is_local_at_target.open_cover_iff

Modified src/algebraic_geometry/morphisms/quasi_compact.lean

added theorem algebraic_geometry.is_compact_basic_open

added theorem algebraic_geometry.quasi_compact.affine_open_cover_iff

added theorem algebraic_geometry.quasi_compact.affine_open_cover_tfae

added def algebraic_geometry.quasi_compact.affine_property

added theorem algebraic_geometry.quasi_compact.affine_property_is_local

added theorem algebraic_geometry.quasi_compact.affine_property_to_property

added theorem algebraic_geometry.quasi_compact.open_cover_iff

added theorem algebraic_geometry.quasi_compact.open_cover_tfae

added theorem algebraic_geometry.quasi_compact_eq_affine_property

added theorem algebraic_geometry.quasi_compact_iff_affine_property

added theorem algebraic_geometry.quasi_compact_over_affine_iff

added theorem algebraic_geometry.quasi_compact_respects_iso

added theorem algebraic_geometry.quasi_compact_stable_under_composition