Commit 2023-02-02 19:23 5a884070

View on Github →

feat: port CategoryTheory.Sigma.Basic (#1147)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sigma/Basic.lean

added def CategoryTheory.Sigma.Functor.sigma

added theorem CategoryTheory.Sigma.SigmaHom.assoc

added def CategoryTheory.Sigma.SigmaHom.comp

added theorem CategoryTheory.Sigma.SigmaHom.comp_def

added theorem CategoryTheory.Sigma.SigmaHom.comp_id

added def CategoryTheory.Sigma.SigmaHom.id

added theorem CategoryTheory.Sigma.SigmaHom.id_comp

added inductive CategoryTheory.Sigma.SigmaHom

added def CategoryTheory.Sigma.desc

added def CategoryTheory.Sigma.descMap

added def CategoryTheory.Sigma.descUniq

added theorem CategoryTheory.Sigma.descUniq_hom_app

added theorem CategoryTheory.Sigma.descUniq_inv_app

added theorem CategoryTheory.Sigma.desc_map_mk

added def CategoryTheory.Sigma.incl

added def CategoryTheory.Sigma.inclCompMap

added def CategoryTheory.Sigma.inclDesc

added theorem CategoryTheory.Sigma.inclDesc_hom_app

added theorem CategoryTheory.Sigma.inclDesc_inv_app

added theorem CategoryTheory.Sigma.incl_obj

added def CategoryTheory.Sigma.map

added def CategoryTheory.Sigma.mapComp

added def CategoryTheory.Sigma.mapId

added theorem CategoryTheory.Sigma.map_map

added theorem CategoryTheory.Sigma.map_obj

added def CategoryTheory.Sigma.natIso

added def CategoryTheory.Sigma.natTrans.sigma

added def CategoryTheory.Sigma.natTrans

added theorem CategoryTheory.Sigma.natTrans_app