Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 07:52 b6b47ed5

View on Github →

feat(algebraic_geometry/presheafed_space): Open immersions of presheafed spaces has pullbacks. (#10069)

Estimated changes

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.PresheafedSpace.is_open_immersion.iso_of_range_eq

added def algebraic_geometry.PresheafedSpace.is_open_immersion.lift

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.lift_fac

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.lift_uniq

added def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_condition

added def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_fst

added def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_is_limit

added def algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift_fst

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_cone_of_left_lift_snd

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.pullback_snd_is_iso_of_range_subset