Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 10:22 718ea932

View on Github →

feat(category_theory): Glue data (#10436)

Estimated changes

Created src/category_theory/glue_data.lean

added def category_theory.glue_data.diagram

added theorem category_theory.glue_data.diagram_L

added theorem category_theory.glue_data.diagram_R

added theorem category_theory.glue_data.diagram_fst

added theorem category_theory.glue_data.diagram_fst_from

added def category_theory.glue_data.diagram_iso

added theorem category_theory.glue_data.diagram_iso_app_left

added theorem category_theory.glue_data.diagram_iso_app_right

added theorem category_theory.glue_data.diagram_iso_hom_app_left

added theorem category_theory.glue_data.diagram_iso_hom_app_right

added theorem category_theory.glue_data.diagram_iso_inv_app_left

added theorem category_theory.glue_data.diagram_iso_inv_app_right

added theorem category_theory.glue_data.diagram_left

added theorem category_theory.glue_data.diagram_right

added theorem category_theory.glue_data.diagram_snd

added theorem category_theory.glue_data.diagram_snd_from

added theorem category_theory.glue_data.glue_condition

added def category_theory.glue_data.glued

added def category_theory.glue_data.map_glue_data

added def category_theory.glue_data.sigma_opens

added theorem category_theory.glue_data.t'_comp_eq_pullback_symmetry

added theorem category_theory.glue_data.t'_iij

added theorem category_theory.glue_data.t'_iji

added theorem category_theory.glue_data.t'_inv

added theorem category_theory.glue_data.t'_jii

added theorem category_theory.glue_data.t_inv

added def category_theory.glue_data.ι

added def category_theory.glue_data.π

added structure category_theory.glue_data