Commit 2021-12-20 07:48 ade581e9

View on Github →

feat(algebraic_geometry): Open immersions of locally ringed spaces have pullbacks (#10917)

Estimated changes

Modified src/algebraic_geometry/locally_ringed_space.lean

added theorem algebraic_geometry.LocallyRingedSpace.comp_val

added def algebraic_geometry.LocallyRingedSpace.of_restrict

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift

added theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_fac

added theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_range

added theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_uniq

added def algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left

added def algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_cone_of_left_is_limit

added theorem algebraic_geometry.LocallyRingedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset

Modified src/category_theory/reflects_isomorphisms.lean