Commit 2023-02-16 18:14 6fa803ed

View on Github →

feat: port CategoryTheory.Arrow (#2315)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Arrow.lean

added theorem CategoryTheory.Arrow.hom.congr_left

added theorem CategoryTheory.Arrow.hom.congr_right

added def CategoryTheory.Arrow.homMk'

added def CategoryTheory.Arrow.homMk

added theorem CategoryTheory.Arrow.id_left

added theorem CategoryTheory.Arrow.id_right

added theorem CategoryTheory.Arrow.inv_left

added theorem CategoryTheory.Arrow.inv_left_hom_right

added theorem CategoryTheory.Arrow.inv_right

added theorem CategoryTheory.Arrow.isIso_of_iso_left_of_isIso_right

added def CategoryTheory.Arrow.isoMk

added def CategoryTheory.Arrow.isoOfNatIso

added theorem CategoryTheory.Arrow.iso_w'

added theorem CategoryTheory.Arrow.iso_w

added def CategoryTheory.Arrow.leftFunc

added def CategoryTheory.Arrow.leftToRight

added theorem CategoryTheory.Arrow.left_hom_inv_right

added def CategoryTheory.Arrow.mk

added theorem CategoryTheory.Arrow.mk_eq

added theorem CategoryTheory.Arrow.mk_inj

added theorem CategoryTheory.Arrow.mk_injective

added def CategoryTheory.Arrow.rightFunc

added def CategoryTheory.Arrow.squareToSnd

added theorem CategoryTheory.Arrow.square_from_iso_invert

added theorem CategoryTheory.Arrow.square_to_iso_invert

added theorem CategoryTheory.Arrow.w

added theorem CategoryTheory.Arrow.w_mk_right

added def CategoryTheory.Arrow

added def CategoryTheory.Functor.mapArrow