Commit 2023-03-26 21:07 8f189461

View on Github →

feat: port CategoryTheory.GlueData (#3099)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/GlueData.lean

added def CategoryTheory.GlueData.diagram

added def CategoryTheory.GlueData.diagramIso

added theorem CategoryTheory.GlueData.diagramIso_app_left

added theorem CategoryTheory.GlueData.diagramIso_app_right

added theorem CategoryTheory.GlueData.diagramIso_hom_app_left

added theorem CategoryTheory.GlueData.diagramIso_hom_app_right

added theorem CategoryTheory.GlueData.diagramIso_inv_app_left

added theorem CategoryTheory.GlueData.diagramIso_inv_app_right

added theorem CategoryTheory.GlueData.diagram_fst

added theorem CategoryTheory.GlueData.diagram_fstFrom

added theorem CategoryTheory.GlueData.diagram_l

added theorem CategoryTheory.GlueData.diagram_left

added theorem CategoryTheory.GlueData.diagram_r

added theorem CategoryTheory.GlueData.diagram_right

added theorem CategoryTheory.GlueData.diagram_snd

added theorem CategoryTheory.GlueData.diagram_sndFrom

added theorem CategoryTheory.GlueData.glue_condition

added def CategoryTheory.GlueData.glued

added def CategoryTheory.GlueData.gluedIso

added theorem CategoryTheory.GlueData.hasColimit_mapGlueData_diagram

added theorem CategoryTheory.GlueData.hasColimit_multispan_comp

added def CategoryTheory.GlueData.mapGlueData

added def CategoryTheory.GlueData.sigmaOpens

added theorem CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry

added theorem CategoryTheory.GlueData.t'_iij

added theorem CategoryTheory.GlueData.t'_iji

added theorem CategoryTheory.GlueData.t'_inv

added theorem CategoryTheory.GlueData.t'_jii

added theorem CategoryTheory.GlueData.t_inv

added theorem CategoryTheory.GlueData.types_ι_jointly_surjective

added theorem CategoryTheory.GlueData.types_π_surjective

added def CategoryTheory.GlueData.vPullbackCone

added def CategoryTheory.GlueData.vPullbackConeIsLimitOfMap

added def CategoryTheory.GlueData.ι

added theorem CategoryTheory.GlueData.ι_gluedIso_hom

added theorem CategoryTheory.GlueData.ι_gluedIso_inv

added theorem CategoryTheory.GlueData.ι_jointly_surjective

added def CategoryTheory.GlueData.π

added structure CategoryTheory.GlueData