Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-05 12:35 68cc6138

View on Github →

feat(algebraic_geometry/open_immersion): Restricting a morphism twice is isomorphic to one restriction. (#15710)

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

modified def algebraic_geometry.Scheme.affine_basic_open

added theorem algebraic_geometry.is_affine_open.image_is_open_immersion

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.Scheme.open_cover_of_supr_eq_top

added def algebraic_geometry.is_open_immersion.opens_range

added def algebraic_geometry.morphism_restrict_eq

added def algebraic_geometry.morphism_restrict_opens_range

added def algebraic_geometry.morphism_restrict_restrict

added def algebraic_geometry.morphism_restrict_restrict_basic_open

Modified src/category_theory/arrow.lean

added def category_theory.arrow.iso_mk'

Modified src/category_theory/morphism_property.lean

added theorem category_theory.morphism_property.respects_iso.arrow_iso_iff

added theorem category_theory.morphism_property.respects_iso.arrow_mk_iso_iff