Commit 2022-12-01 15:35 c5ffca6d

View on Github →

port: several files from category_theory (#749) mathlib git sha: 8350c34a64b9bc3fc64335df8006bffcadc7baa6 Also ports the reassoc attribute.

depends on: #755

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/Basic.lean

added theorem CategoryTheory.cancel_epi

added theorem CategoryTheory.cancel_epi_id

added theorem CategoryTheory.cancel_mono

added theorem CategoryTheory.cancel_mono_id

added theorem CategoryTheory.comp_dite

added theorem CategoryTheory.comp_ite

added theorem CategoryTheory.dite_comp

added theorem CategoryTheory.epi_comp

added theorem CategoryTheory.epi_of_epi

added theorem CategoryTheory.epi_of_epi_fac

added theorem CategoryTheory.eq_of_comp_left_eq'

added theorem CategoryTheory.eq_of_comp_left_eq

added theorem CategoryTheory.eq_of_comp_right_eq'

added theorem CategoryTheory.eq_of_comp_right_eq

added theorem CategoryTheory.eq_whisker

added theorem CategoryTheory.id_of_comp_left_id

added theorem CategoryTheory.id_of_comp_right_id

added theorem CategoryTheory.ite_comp

added theorem CategoryTheory.mono_comp

added theorem CategoryTheory.mono_of_mono

added theorem CategoryTheory.mono_of_mono_fac

added theorem CategoryTheory.whisker_eq

added def Std.Tactic.Ext.extCore'

Created Mathlib/CategoryTheory/Functor/Basic.lean

added def CategoryTheory.Functor.comp

added theorem CategoryTheory.Functor.comp_map

added theorem CategoryTheory.Functor.id_map

added theorem CategoryTheory.Functor.id_obj

added theorem CategoryTheory.Functor.map_dite

added theorem CategoryTheory.Functor.toPrefunctor_comp

added structure CategoryTheory.Functor

Created Mathlib/CategoryTheory/Functor/Category.lean

added theorem CategoryTheory.NatTrans.app_naturality

added theorem CategoryTheory.NatTrans.comp_app

added theorem CategoryTheory.NatTrans.congr_app

added theorem CategoryTheory.NatTrans.epi_of_epi_app

added theorem CategoryTheory.NatTrans.exchange

added theorem CategoryTheory.NatTrans.ext'

added def CategoryTheory.NatTrans.hcomp

added theorem CategoryTheory.NatTrans.hcomp_id_app

added theorem CategoryTheory.NatTrans.id_app

added theorem CategoryTheory.NatTrans.id_hcomp_app

added theorem CategoryTheory.NatTrans.mono_of_mono_app

added theorem CategoryTheory.NatTrans.naturality_app

added theorem CategoryTheory.NatTrans.vcomp_app'

added theorem CategoryTheory.NatTrans.vcomp_eq_comp

added theorem CategoryTheory.map_hom_inv_app

added theorem CategoryTheory.map_inv_hom_app

Created Mathlib/CategoryTheory/Iso.lean

added def CategoryTheory.Functor.mapIso

added theorem CategoryTheory.Functor.mapIso_refl

added theorem CategoryTheory.Functor.mapIso_symm

added theorem CategoryTheory.Functor.mapIso_trans

added theorem CategoryTheory.Functor.map_hom_inv

added theorem CategoryTheory.Functor.map_inv

added theorem CategoryTheory.Functor.map_inv_hom

added theorem CategoryTheory.IsIso.Iso.inv_hom

added theorem CategoryTheory.IsIso.Iso.inv_inv

added theorem CategoryTheory.IsIso.comp_inv_eq

added theorem CategoryTheory.IsIso.eq_comp_inv

added theorem CategoryTheory.IsIso.eq_inv_comp

added theorem CategoryTheory.IsIso.eq_inv_of_hom_inv_id

added theorem CategoryTheory.IsIso.eq_inv_of_inv_hom_id

added theorem CategoryTheory.IsIso.hom_inv_id

added theorem CategoryTheory.IsIso.hom_inv_id_assoc

added theorem CategoryTheory.IsIso.inv_comp

added theorem CategoryTheory.IsIso.inv_comp_eq

added theorem CategoryTheory.IsIso.inv_eq_inv

added theorem CategoryTheory.IsIso.inv_eq_of_hom_inv_id

added theorem CategoryTheory.IsIso.inv_eq_of_inv_hom_id

added theorem CategoryTheory.IsIso.inv_hom_id

added theorem CategoryTheory.IsIso.inv_hom_id_assoc

added theorem CategoryTheory.IsIso.inv_id

added theorem CategoryTheory.IsIso.inv_inv

added theorem CategoryTheory.IsIso.of_isIso_comp_left

added theorem CategoryTheory.IsIso.of_isIso_comp_right

added theorem CategoryTheory.IsIso.of_isIso_fac_left

added theorem CategoryTheory.IsIso.of_isIso_fac_right

added theorem CategoryTheory.Iso.cancel_iso_hom_left

added theorem CategoryTheory.Iso.cancel_iso_hom_right

added theorem CategoryTheory.Iso.cancel_iso_hom_right_assoc

added theorem CategoryTheory.Iso.cancel_iso_inv_left

added theorem CategoryTheory.Iso.cancel_iso_inv_right

added theorem CategoryTheory.Iso.cancel_iso_inv_right_assoc

added theorem CategoryTheory.Iso.comp_hom_eq_id

added theorem CategoryTheory.Iso.comp_inv_eq

added theorem CategoryTheory.Iso.comp_inv_eq_id

added theorem CategoryTheory.Iso.eq_comp_inv

added theorem CategoryTheory.Iso.eq_inv_comp

added theorem CategoryTheory.Iso.ext

added theorem CategoryTheory.Iso.hom_comp_eq_id

added theorem CategoryTheory.Iso.hom_eq_inv

added theorem CategoryTheory.Iso.inv_comp_eq

added theorem CategoryTheory.Iso.inv_comp_eq_id

added theorem CategoryTheory.Iso.inv_eq_inv

added theorem CategoryTheory.Iso.inv_ext'

added theorem CategoryTheory.Iso.inv_ext

added theorem CategoryTheory.Iso.nonempty_iso_symm

added def CategoryTheory.Iso.refl

added theorem CategoryTheory.Iso.refl_symm

added theorem CategoryTheory.Iso.refl_trans

added theorem CategoryTheory.Iso.self_symm_id

added theorem CategoryTheory.Iso.self_symm_id_assoc

added def CategoryTheory.Iso.symm

added theorem CategoryTheory.Iso.symm_eq_iff

added theorem CategoryTheory.Iso.symm_hom

added theorem CategoryTheory.Iso.symm_inv

added theorem CategoryTheory.Iso.symm_mk

added theorem CategoryTheory.Iso.symm_self_id

added theorem CategoryTheory.Iso.symm_self_id_assoc

added theorem CategoryTheory.Iso.symm_symm_eq

added def CategoryTheory.Iso.trans

added theorem CategoryTheory.Iso.trans_assoc

added theorem CategoryTheory.Iso.trans_mk

added theorem CategoryTheory.Iso.trans_refl

added theorem CategoryTheory.Iso.trans_symm

added structure CategoryTheory.Iso

added theorem CategoryTheory.asIso_hom

added theorem CategoryTheory.asIso_inv

added theorem CategoryTheory.comp_hom_eq_id

added theorem CategoryTheory.comp_inv_eq_id

added theorem CategoryTheory.eq_of_inv_eq_inv

added theorem CategoryTheory.hom_comp_eq_id

added theorem CategoryTheory.inv_comp_eq_id

added theorem CategoryTheory.isIso_of_comp_hom_eq_id

added theorem CategoryTheory.isIso_of_hom_comp_eq_id

Created Mathlib/CategoryTheory/NatTrans.lean

added theorem CategoryTheory.NatTrans.id_app'

added def CategoryTheory.NatTrans.vcomp

added theorem CategoryTheory.NatTrans.vcomp_app

added structure CategoryTheory.NatTrans

added theorem CategoryTheory.congr_app

Created Mathlib/Combinatorics/Quiver/Basic.lean

added def Prefunctor.comp

added theorem Prefunctor.comp_assoc

added theorem Prefunctor.ext

added def Prefunctor.id

added structure Prefunctor

added def Quiver.Empty

added def Quiver.Hom.op

added def Quiver.Hom.unop

added def Quiver.IsThin

added theorem Quiver.empty_arrow

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/Reassoc.lean

added def CategoryTheory.categorySimp

added theorem CategoryTheory.eq_whisker'

added def CategoryTheory.reassoc

Modified lake-manifest.json