Mathlib Changelog
v3
Changelog
About
Github
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