Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 23:25 e2452546

View on Github →

feat(category_theory/monoidal): λ_ (𝟙_ C) = ρ_ (𝟙_ C) (#3556) The incredibly tedious proof from the axioms that λ_ (𝟙_ C) = ρ_ (𝟙_ C) in any monoidal category. One would hope that it falls out from a coherence theorem, but we're not close to having one, and I suspect that this result might be a step in any proof.

Estimated changes

Modified src/category_theory/monoidal/category.lean

added theorem category_theory.monoidal_category.left_unitor_conjugation

added theorem category_theory.monoidal_category.right_unitor_conjugation

Created src/category_theory/monoidal/unitors.lean

added theorem category_theory.monoidal_category.unitors_equal.cells_10_13

added theorem category_theory.monoidal_category.unitors_equal.cells_14

added theorem category_theory.monoidal_category.unitors_equal.cells_15

added theorem category_theory.monoidal_category.unitors_equal.cells_1_2

added theorem category_theory.monoidal_category.unitors_equal.cells_1_4

added theorem category_theory.monoidal_category.unitors_equal.cells_1_7

added theorem category_theory.monoidal_category.unitors_equal.cells_3_4

added theorem category_theory.monoidal_category.unitors_equal.cells_4'

added theorem category_theory.monoidal_category.unitors_equal.cells_4

added theorem category_theory.monoidal_category.unitors_equal.cells_5_6

added theorem category_theory.monoidal_category.unitors_equal.cells_6'

added theorem category_theory.monoidal_category.unitors_equal.cells_6

added theorem category_theory.monoidal_category.unitors_equal.cells_7

added theorem category_theory.monoidal_category.unitors_equal.cells_8

added theorem category_theory.monoidal_category.unitors_equal.cells_9

added theorem category_theory.monoidal_category.unitors_equal.cells_9_13

added theorem category_theory.monoidal_category.unitors_equal