Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-24 07:29 434e2fd2

View on Github →

feat(algebraic_geometry/morphisms/universally_closed): Define universally closed morphism between schemes (#17117)

Estimated changes

Modified src/algebraic_geometry/morphisms/basic.lean

added def algebraic_geometry.morphism_property.topologically

added theorem algebraic_geometry.universally_is_local_at_target

added theorem algebraic_geometry.universally_is_local_at_target_of_morphism_restrict

Created src/algebraic_geometry/morphisms/universally_closed.lean

added theorem algebraic_geometry.morphism_restrict_base

added theorem algebraic_geometry.universally_closed.open_cover_iff

added theorem algebraic_geometry.universally_closed_eq

added theorem algebraic_geometry.universally_closed_is_local_at_target

added theorem algebraic_geometry.universally_closed_respects_iso

added theorem algebraic_geometry.universally_closed_stable_under_base_change

added theorem algebraic_geometry.universally_closed_stable_under_composition

Modified src/algebraic_geometry/open_immersion.lean

added theorem algebraic_geometry.Scheme.open_cover.supr_opens_range

added theorem algebraic_geometry.is_pullback_morphism_restrict

modified theorem algebraic_geometry.morphism_restrict_ι

Modified src/topology/local_at_target.lean

deleted theorem closed_iff_coe_preimage_of_supr_eq_top

added theorem is_closed_iff_coe_preimage_of_supr_eq_top

added theorem is_closed_map_iff_is_closed_map_of_supr_eq_top

added theorem is_open_iff_coe_preimage_of_supr_eq_top

added theorem is_open_iff_inter_of_supr_eq_top

deleted theorem open_iff_coe_preimage_of_supr_eq_top

deleted theorem open_iff_inter_of_supr_eq_top

added theorem set.restrict_preimage_is_closed_map