Commit 2023-03-02 21:38 064dbd9e

View on Github →

feat: port/CategoryTheory.StructuredArrow (#2486)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/DiscreteCategory.lean

Created Mathlib/CategoryTheory/StructuredArrow.lean

added theorem CategoryTheory.CostructuredArrow.comp_left

added theorem CategoryTheory.CostructuredArrow.epi_of_epi_left

added theorem CategoryTheory.CostructuredArrow.eq_mk

added def CategoryTheory.CostructuredArrow.eta

added theorem CategoryTheory.CostructuredArrow.ext

added theorem CategoryTheory.CostructuredArrow.ext_iff

added def CategoryTheory.CostructuredArrow.homMk

added theorem CategoryTheory.CostructuredArrow.id_left

added def CategoryTheory.CostructuredArrow.isoMk

added def CategoryTheory.CostructuredArrow.map

added theorem CategoryTheory.CostructuredArrow.map_comp

added theorem CategoryTheory.CostructuredArrow.map_id

added theorem CategoryTheory.CostructuredArrow.map_mk

added def CategoryTheory.CostructuredArrow.mk

added def CategoryTheory.CostructuredArrow.mkIdTerminal

added theorem CategoryTheory.CostructuredArrow.mk_hom_eq_self

added theorem CategoryTheory.CostructuredArrow.mk_left

added theorem CategoryTheory.CostructuredArrow.mk_right

added theorem CategoryTheory.CostructuredArrow.mono_of_mono_left

added def CategoryTheory.CostructuredArrow.post

added def CategoryTheory.CostructuredArrow.pre

added def CategoryTheory.CostructuredArrow.proj

added theorem CategoryTheory.CostructuredArrow.right_eq_id

added def CategoryTheory.CostructuredArrow.toStructuredArrow'

added def CategoryTheory.CostructuredArrow.toStructuredArrow

added theorem CategoryTheory.CostructuredArrow.w

added def CategoryTheory.CostructuredArrow

added theorem CategoryTheory.StructuredArrow.comp_right

added theorem CategoryTheory.StructuredArrow.epi_of_epi_right

added theorem CategoryTheory.StructuredArrow.eq_mk

added def CategoryTheory.StructuredArrow.eta

added theorem CategoryTheory.StructuredArrow.ext

added theorem CategoryTheory.StructuredArrow.ext_iff

added def CategoryTheory.StructuredArrow.homMk'

added def CategoryTheory.StructuredArrow.homMk

added theorem CategoryTheory.StructuredArrow.id_right

added def CategoryTheory.StructuredArrow.isoMk

added theorem CategoryTheory.StructuredArrow.left_eq_id

added def CategoryTheory.StructuredArrow.map

added theorem CategoryTheory.StructuredArrow.map_comp

added theorem CategoryTheory.StructuredArrow.map_id

added theorem CategoryTheory.StructuredArrow.map_mk

added def CategoryTheory.StructuredArrow.mk

added def CategoryTheory.StructuredArrow.mkIdInitial

added theorem CategoryTheory.StructuredArrow.mk_hom_eq_self

added theorem CategoryTheory.StructuredArrow.mk_left

added theorem CategoryTheory.StructuredArrow.mk_right

added theorem CategoryTheory.StructuredArrow.mono_of_mono_right

added def CategoryTheory.StructuredArrow.post

added def CategoryTheory.StructuredArrow.pre

added def CategoryTheory.StructuredArrow.proj

added def CategoryTheory.StructuredArrow.toCostructuredArrow'

added def CategoryTheory.StructuredArrow.toCostructuredArrow

added theorem CategoryTheory.StructuredArrow.w

added def CategoryTheory.StructuredArrow

added def CategoryTheory.costructuredArrowOpEquivalence

added def CategoryTheory.structuredArrowOpEquivalence