Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-13 12:25 6609204b

View on Github →

feat(algebraic_geometry): Gluing presheafed spaces (#10269)

Estimated changes

Created src/algebraic_geometry/presheafed_space/gluing.lean

added theorem algebraic_geometry.PresheafedSpace.coe_to_fun_eq

added def algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open

added def algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open_π

added theorem algebraic_geometry.PresheafedSpace.glue_data.f_inv_app_f_app

added def algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map

added theorem algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app'

added theorem algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app

added theorem algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app_assoc

added theorem algebraic_geometry.PresheafedSpace.glue_data.pullback_base

added theorem algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app'

added theorem algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app

added def algebraic_geometry.PresheafedSpace.glue_data.to_Top_glue_data

added theorem algebraic_geometry.PresheafedSpace.glue_data.ι_image_preimage_eq

added def algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app

added theorem algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π

added def algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_app

added def algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_eq_map

added theorem algebraic_geometry.PresheafedSpace.glue_data.ι_open_embedding

added theorem algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_eq_id

added theorem algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_π

added structure algebraic_geometry.PresheafedSpace.glue_data

Modified src/topology/category/Top/limits.lean

added theorem Top.pullback_fst_image_snd_preimage

added theorem Top.pullback_snd_image_fst_preimage