Commit 2023-06-08 09:12 bd09dbc7

View on Github →

feat: port CategoryTheory.Preadditive.Mat (#4796)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Mat.lean

added def CategoryTheory.Functor.mapMatComp

added def CategoryTheory.Functor.mapMatId

added def CategoryTheory.Functor.mapMat_

added theorem CategoryTheory.Mat.add_apply

added theorem CategoryTheory.Mat.comp_apply

added theorem CategoryTheory.Mat.comp_def

added def CategoryTheory.Mat.equivalenceSingleObj

added def CategoryTheory.Mat.equivalenceSingleObjInverse

added theorem CategoryTheory.Mat.hom_ext

added theorem CategoryTheory.Mat.id_apply

added theorem CategoryTheory.Mat.id_apply_of_ne

added theorem CategoryTheory.Mat.id_apply_self

added theorem CategoryTheory.Mat.id_def

added def CategoryTheory.Mat

added def CategoryTheory.Mat_.Hom.comp

added def CategoryTheory.Mat_.Hom.id

added def CategoryTheory.Mat_.Hom

added theorem CategoryTheory.Mat_.add_apply

added def CategoryTheory.Mat_.additiveObjIsoBiproduct

added theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π

added theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'

added theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality

added theorem CategoryTheory.Mat_.comp_apply

added theorem CategoryTheory.Mat_.comp_def

added def CategoryTheory.Mat_.embedding

added def CategoryTheory.Mat_.embeddingLiftIso

added def CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts

added def CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproductsAux

added theorem CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_functor

added theorem CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_inverse

added def CategoryTheory.Mat_.ext

added theorem CategoryTheory.Mat_.hom_ext

added theorem CategoryTheory.Mat_.id_apply

added theorem CategoryTheory.Mat_.id_apply_of_ne

added theorem CategoryTheory.Mat_.id_apply_self

added theorem CategoryTheory.Mat_.id_def

added def CategoryTheory.Mat_.isoBiproductEmbedding

added def CategoryTheory.Mat_.lift

added def CategoryTheory.Mat_.liftUnique

added theorem CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv

added structure CategoryTheory.Mat_