Mat

📁 Source: Mathlib/CategoryTheory/Preadditive/Mat.lean

Statistics

Metric	Count
Definitions mapMatComp, mapMatId, mapMat_, Mat, equivalenceSingleObj, equivalenceSingleObjInverse, instAddCommGroupHom, instInhabitedHom, instPreadditive, Mat_, comp, id, X, additiveObjIsoBiproduct, embedding, embeddingLiftIso, equivalenceSelfOfHasFiniteBiproducts, equivalenceSelfOfHasFiniteBiproductsAux, ext, fintype, instAddCommGroupHom, instCategory, instInhabited, instInhabitedHom, instPreadditive, isoBiproductEmbedding, liftUnique, ι, instCategoryMatOfSemiring, instCoeSortMatType, instInhabitedMat	31
Theorems mapMatComp_hom_app, mapMatComp_inv_app, mapMatId_hom_app, mapMatId_inv_app, mapMat__map, mapMat__obj_X, mapMat__obj_fintype, mapMat__obj_ι, add_apply, comp_apply, comp_def, equivalenceSingleObjInverse_map, equivalenceSingleObjInverse_obj_carrier, equivalenceSingleObjInverse_obj_str, hom_ext, hom_ext_iff, id_apply, id_apply_of_ne, id_apply_self, id_def, instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, instAdditiveEmbedding, instFaithfulEmbedding, instFullEmbedding, add_apply, additiveObjIsoBiproduct_hom_π, additiveObjIsoBiproduct_hom_π_assoc, additiveObjIsoBiproduct_naturality, additiveObjIsoBiproduct_naturality', additiveObjIsoBiproduct_naturality'_assoc, additiveObjIsoBiproduct_naturality_assoc, comp_apply, comp_def, embeddingLiftIso_hom_app, embeddingLiftIso_inv_app, embedding_map, embedding_obj_X, embedding_obj_fintype, embedding_obj_ι, equivalenceSelfOfHasFiniteBiproducts_functor, equivalenceSelfOfHasFiniteBiproducts_inverse, hasFiniteBiproducts, hom_ext, hom_ext_iff, id_apply, id_apply_of_ne, id_apply_self, id_def, instHasBiproductιObjEmbeddingXOfAdditive, isoBiproductEmbedding_hom, isoBiproductEmbedding_inv, lift_additive, lift_map, lift_obj, ι_additiveObjIsoBiproduct_inv, ι_additiveObjIsoBiproduct_inv_assoc	59
Total	90

CategoryTheory

Definitions

Name	Category	Theorems
Mat 📖	CompOp	14 math math: Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.equivalenceSingleObjInverse_obj_carrier, Mat.comp_apply, Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.id_apply_of_ne, Mat.add_apply, Mat.comp_def, Mat.id_apply, Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.id_apply_self, Mat.equivalenceSingleObjInverse_map, Mat.equivalenceSingleObjInverse_obj_str, Mat.id_def
Mat_ 📖	CompData	48 math math: Mat_.additiveObjIsoBiproduct_hom_π, Functor.mapMat__obj_X, Functor.mapMat__obj_ι, Mat_.embedding_obj_ι, Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat_.additiveObjIsoBiproduct_naturality, Functor.mapMatComp_hom_app, Mat_.ι_additiveObjIsoBiproduct_inv_assoc, Mat_.additiveObjIsoBiproduct_naturality', Mat_.embedding_obj_X, Mat_.id_apply_self, Mat_.lift_obj, Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat_.instHasBiproductιObjEmbeddingXOfAdditive, Mat.equivalenceSingleObjInverse_obj_carrier, Mat_.embeddingLiftIso_hom_app, Mat_.isoBiproductEmbedding_hom, Mat_.Embedding.instAdditiveEmbedding, Mat_.embeddingLiftIso_inv_app, Mat_.add_apply, Mat_.equivalenceSelfOfHasFiniteBiproducts_functor, Mat_.Embedding.instFaithfulEmbedding, Mat_.embedding_obj_fintype, Mat_.lift_additive, Mat_.ι_additiveObjIsoBiproduct_inv, Mat_.additiveObjIsoBiproduct_naturality_assoc, Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat_.lift_map, Mat_.equivalenceSelfOfHasFiniteBiproducts_inverse, Functor.mapMat__obj_fintype, Mat_.isoBiproductEmbedding_inv, Mat_.comp_apply, Mat_.hasFiniteBiproducts, Functor.mapMat__map, Functor.mapMatId_hom_app, Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat_.id_apply, Mat.equivalenceSingleObjInverse_map, Mat_.id_def, Mat_.Embedding.instFullEmbedding, Mat.equivalenceSingleObjInverse_obj_str, Mat_.id_apply_of_ne, Functor.mapMatId_inv_app, Mat_.embedding_map, Mat_.comp_def, Functor.mapMatComp_inv_app, Mat_.additiveObjIsoBiproduct_naturality'_assoc, Mat_.additiveObjIsoBiproduct_hom_π_assoc
instCategoryMatOfSemiring 📖	CompOp	14 math math: Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.equivalenceSingleObjInverse_obj_carrier, Mat.comp_apply, Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.id_apply_of_ne, Mat.add_apply, Mat.comp_def, Mat.id_apply, Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Mat.id_apply_self, Mat.equivalenceSingleObjInverse_map, Mat.equivalenceSingleObjInverse_obj_str, Mat.id_def
instCoeSortMatType 📖	CompOp	—
instInhabitedMat 📖	CompOp	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapMatComp 📖	CompOp	2 math math: mapMatComp_hom_app, mapMatComp_inv_app
mapMatId 📖	CompOp	2 math math: mapMatId_hom_app, mapMatId_inv_app
mapMat_ 📖	CompOp	8 math math: mapMat__obj_X, mapMat__obj_ι, mapMatComp_hom_app, mapMat__obj_fintype, mapMat__map, mapMatId_hom_app, mapMatId_inv_app, mapMatComp_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMatComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory mapMat_ comp instAdditiveComp CategoryTheory.Iso.hom CategoryTheory.Functor category mapMatComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj	—	instAdditiveComp
mapMatComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory comp mapMat_ instAdditiveComp CategoryTheory.Iso.inv CategoryTheory.Functor category mapMatComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj	—	instAdditiveComp
mapMatId_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory mapMat_ id instAdditiveId CategoryTheory.Iso.hom CategoryTheory.Functor category mapMatId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj	—	instAdditiveId
mapMatId_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory id mapMat_ instAdditiveId CategoryTheory.Iso.inv CategoryTheory.Functor category mapMatId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj	—	instAdditiveId
mapMat__map 📖	mathematical	—	map CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory mapMat_ CategoryTheory.Mat_.X	—	—
mapMat__obj_X 📖	mathematical	—	CategoryTheory.Mat_.X obj CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory mapMat_	—	—
mapMat__obj_fintype 📖	mathematical	—	CategoryTheory.Mat_.fintype obj CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory mapMat_	—	—
mapMat__obj_ι 📖	mathematical	—	CategoryTheory.Mat_.ι obj CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory mapMat_	—	—

CategoryTheory.Mat

Definitions

Name	Category	Theorems
equivalenceSingleObj 📖	CompOp	—
equivalenceSingleObjInverse 📖	CompOp	7 math math: instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, equivalenceSingleObjInverse_obj_carrier, instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, equivalenceSingleObjInverse_map, equivalenceSingleObjInverse_obj_str
instAddCommGroupHom 📖	CompOp	1 math math: add_apply
instInhabitedHom 📖	CompOp	—
instPreadditive 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	Quiver.Hom CategoryTheory.Mat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMatOfSemiring Ring.toSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupHom Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
comp_apply 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Mat CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMatOfSemiring Finset.sum FintypeCat.carrier NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ FintypeCat.instFintypeCarrier Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
comp_def 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Mat CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMatOfSemiring Finset.sum FintypeCat.carrier NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ FintypeCat.instFintypeCarrier Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
equivalenceSingleObjInverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Mat_ CategoryTheory.SingleObj MulOpposite CategoryTheory.Mat_.instCategory CategoryTheory.SingleObj.category MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CategoryTheory.instPreadditiveSingleObj MulOpposite.instRing CategoryTheory.Mat CategoryTheory.instCategoryMatOfSemiring equivalenceSingleObjInverse MulOpposite.unop	—	—
equivalenceSingleObjInverse_obj_carrier 📖	mathematical	—	FintypeCat.carrier CategoryTheory.Functor.obj CategoryTheory.Mat_ CategoryTheory.SingleObj MulOpposite CategoryTheory.Mat_.instCategory CategoryTheory.SingleObj.category MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CategoryTheory.instPreadditiveSingleObj MulOpposite.instRing CategoryTheory.Mat CategoryTheory.instCategoryMatOfSemiring equivalenceSingleObjInverse CategoryTheory.Mat_.ι	—	—
equivalenceSingleObjInverse_obj_str 📖	mathematical	—	FintypeCat.str CategoryTheory.Functor.obj CategoryTheory.Mat_ CategoryTheory.SingleObj MulOpposite CategoryTheory.Mat_.instCategory CategoryTheory.SingleObj.category MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CategoryTheory.instPreadditiveSingleObj MulOpposite.instRing CategoryTheory.Mat CategoryTheory.instCategoryMatOfSemiring equivalenceSingleObjInverse CategoryTheory.Mat_.fintype	—	—
hom_ext 📖	—	—	—	—	Matrix.ext_iff
hom_ext_iff 📖	—	—	—	—	hom_ext
id_apply 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMatOfSemiring FintypeCat.carrier AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
id_apply_of_ne 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMatOfSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
id_apply_self 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMatOfSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	—
id_def 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryMatOfSemiring FintypeCat.carrier AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.Mat_ CategoryTheory.SingleObj MulOpposite CategoryTheory.Mat CategoryTheory.Mat_.instCategory CategoryTheory.SingleObj.category MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CategoryTheory.instPreadditiveSingleObj MulOpposite.instRing CategoryTheory.instCategoryMatOfSemiring equivalenceSingleObjInverse	—	—
instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Mat_ CategoryTheory.SingleObj MulOpposite CategoryTheory.Mat_.instCategory CategoryTheory.SingleObj.category MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CategoryTheory.instPreadditiveSingleObj MulOpposite.instRing CategoryTheory.Mat CategoryTheory.instCategoryMatOfSemiring equivalenceSingleObjInverse	—	CategoryTheory.Mat_.hom_ext MulOpposite.unop_injective
instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Mat_ CategoryTheory.SingleObj MulOpposite CategoryTheory.Mat_.instCategory CategoryTheory.SingleObj.category MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CategoryTheory.instPreadditiveSingleObj MulOpposite.instRing CategoryTheory.Mat CategoryTheory.instCategoryMatOfSemiring equivalenceSingleObjInverse	—	—
instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Mat_ CategoryTheory.SingleObj MulOpposite CategoryTheory.Mat_.instCategory CategoryTheory.SingleObj.category MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CategoryTheory.instPreadditiveSingleObj MulOpposite.instRing CategoryTheory.Mat CategoryTheory.instCategoryMatOfSemiring equivalenceSingleObjInverse	—	instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse

CategoryTheory.Mat_

Definitions

Name	Category	Theorems
X 📖	CompOp	23 math math: additiveObjIsoBiproduct_hom_π, CategoryTheory.Functor.mapMat__obj_X, additiveObjIsoBiproduct_naturality, ι_additiveObjIsoBiproduct_inv_assoc, additiveObjIsoBiproduct_naturality', embedding_obj_X, id_apply_self, lift_obj, instHasBiproductιObjEmbeddingXOfAdditive, isoBiproductEmbedding_hom, add_apply, ι_additiveObjIsoBiproduct_inv, additiveObjIsoBiproduct_naturality_assoc, lift_map, isoBiproductEmbedding_inv, comp_apply, CategoryTheory.Functor.mapMat__map, id_apply, id_def, id_apply_of_ne, comp_def, additiveObjIsoBiproduct_naturality'_assoc, additiveObjIsoBiproduct_hom_π_assoc
additiveObjIsoBiproduct 📖	CompOp	8 math math: additiveObjIsoBiproduct_hom_π, additiveObjIsoBiproduct_naturality, ι_additiveObjIsoBiproduct_inv_assoc, additiveObjIsoBiproduct_naturality', ι_additiveObjIsoBiproduct_inv, additiveObjIsoBiproduct_naturality_assoc, additiveObjIsoBiproduct_naturality'_assoc, additiveObjIsoBiproduct_hom_π_assoc
embedding 📖	CompOp	21 math math: additiveObjIsoBiproduct_hom_π, embedding_obj_ι, additiveObjIsoBiproduct_naturality, ι_additiveObjIsoBiproduct_inv_assoc, additiveObjIsoBiproduct_naturality', embedding_obj_X, instHasBiproductιObjEmbeddingXOfAdditive, embeddingLiftIso_hom_app, isoBiproductEmbedding_hom, Embedding.instAdditiveEmbedding, embeddingLiftIso_inv_app, Embedding.instFaithfulEmbedding, embedding_obj_fintype, ι_additiveObjIsoBiproduct_inv, additiveObjIsoBiproduct_naturality_assoc, equivalenceSelfOfHasFiniteBiproducts_inverse, isoBiproductEmbedding_inv, Embedding.instFullEmbedding, embedding_map, additiveObjIsoBiproduct_naturality'_assoc, additiveObjIsoBiproduct_hom_π_assoc
embeddingLiftIso 📖	CompOp	2 math math: embeddingLiftIso_hom_app, embeddingLiftIso_inv_app
equivalenceSelfOfHasFiniteBiproducts 📖	CompOp	2 math math: equivalenceSelfOfHasFiniteBiproducts_functor, equivalenceSelfOfHasFiniteBiproducts_inverse
equivalenceSelfOfHasFiniteBiproductsAux 📖	CompOp	—
ext 📖	CompOp	—
fintype 📖	CompOp	15 math math: additiveObjIsoBiproduct_hom_π, additiveObjIsoBiproduct_naturality, ι_additiveObjIsoBiproduct_inv_assoc, additiveObjIsoBiproduct_naturality', isoBiproductEmbedding_hom, embedding_obj_fintype, ι_additiveObjIsoBiproduct_inv, additiveObjIsoBiproduct_naturality_assoc, CategoryTheory.Functor.mapMat__obj_fintype, isoBiproductEmbedding_inv, comp_apply, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_str, comp_def, additiveObjIsoBiproduct_naturality'_assoc, additiveObjIsoBiproduct_hom_π_assoc
instAddCommGroupHom 📖	CompOp	1 math math: add_apply
instCategory 📖	CompOp	48 math math: additiveObjIsoBiproduct_hom_π, CategoryTheory.Functor.mapMat__obj_X, CategoryTheory.Functor.mapMat__obj_ι, embedding_obj_ι, CategoryTheory.Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, additiveObjIsoBiproduct_naturality, CategoryTheory.Functor.mapMatComp_hom_app, ι_additiveObjIsoBiproduct_inv_assoc, additiveObjIsoBiproduct_naturality', embedding_obj_X, id_apply_self, lift_obj, CategoryTheory.Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, instHasBiproductιObjEmbeddingXOfAdditive, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_carrier, embeddingLiftIso_hom_app, isoBiproductEmbedding_hom, Embedding.instAdditiveEmbedding, embeddingLiftIso_inv_app, add_apply, equivalenceSelfOfHasFiniteBiproducts_functor, Embedding.instFaithfulEmbedding, embedding_obj_fintype, lift_additive, ι_additiveObjIsoBiproduct_inv, additiveObjIsoBiproduct_naturality_assoc, CategoryTheory.Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, lift_map, equivalenceSelfOfHasFiniteBiproducts_inverse, CategoryTheory.Functor.mapMat__obj_fintype, isoBiproductEmbedding_inv, comp_apply, hasFiniteBiproducts, CategoryTheory.Functor.mapMat__map, CategoryTheory.Functor.mapMatId_hom_app, CategoryTheory.Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, id_apply, CategoryTheory.Mat.equivalenceSingleObjInverse_map, id_def, Embedding.instFullEmbedding, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_str, id_apply_of_ne, CategoryTheory.Functor.mapMatId_inv_app, embedding_map, comp_def, CategoryTheory.Functor.mapMatComp_inv_app, additiveObjIsoBiproduct_naturality'_assoc, additiveObjIsoBiproduct_hom_π_assoc
instInhabited 📖	CompOp	—
instInhabitedHom 📖	CompOp	—
instPreadditive 📖	CompOp	9 math math: additiveObjIsoBiproduct_hom_π, ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_hom, Embedding.instAdditiveEmbedding, lift_additive, ι_additiveObjIsoBiproduct_inv, isoBiproductEmbedding_inv, hasFiniteBiproducts, additiveObjIsoBiproduct_hom_π_assoc
isoBiproductEmbedding 📖	CompOp	6 math math: additiveObjIsoBiproduct_hom_π, ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_hom, ι_additiveObjIsoBiproduct_inv, isoBiproductEmbedding_inv, additiveObjIsoBiproduct_hom_π_assoc
liftUnique 📖	CompOp	—
ι 📖	CompOp	20 math math: additiveObjIsoBiproduct_hom_π, CategoryTheory.Functor.mapMat__obj_ι, embedding_obj_ι, additiveObjIsoBiproduct_naturality, ι_additiveObjIsoBiproduct_inv_assoc, additiveObjIsoBiproduct_naturality', lift_obj, instHasBiproductιObjEmbeddingXOfAdditive, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_carrier, isoBiproductEmbedding_hom, ι_additiveObjIsoBiproduct_inv, additiveObjIsoBiproduct_naturality_assoc, lift_map, isoBiproductEmbedding_inv, comp_apply, id_apply, id_def, comp_def, additiveObjIsoBiproduct_naturality'_assoc, additiveObjIsoBiproduct_hom_π_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	Quiver.Hom CategoryTheory.Mat_ CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupHom CategoryTheory.Preadditive.homGroup X	—	—
additiveObjIsoBiproduct_hom_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms embedding X instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Iso.hom additiveObjIsoBiproduct CategoryTheory.Limits.biproduct.π CategoryTheory.Functor.map instPreadditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype fintype isoBiproductEmbedding	—	instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype CategoryTheory.Functor.hasBiproduct_of_preserves CategoryTheory.Limits.biproduct.lift_π CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp
additiveObjIsoBiproduct_hom_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms embedding X instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Iso.hom additiveObjIsoBiproduct CategoryTheory.Limits.biproduct.π CategoryTheory.Functor.map instPreadditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype fintype isoBiproductEmbedding	—	instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' additiveObjIsoBiproduct_hom_π
additiveObjIsoBiproduct_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms embedding X instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Functor.map CategoryTheory.Iso.hom additiveObjIsoBiproduct CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Finite.of_fintype fintype CategoryTheory.Limits.biproduct.matrix	—	CategoryTheory.Limits.biproduct.hom_ext instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Finite.of_fintype CategoryTheory.Category.assoc hasFiniteBiproducts additiveObjIsoBiproduct_hom_π CategoryTheory.Limits.biproduct.lift_π CategoryTheory.Limits.biproduct.matrix_π CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.biproduct.hom_ext' CategoryTheory.Functor.map_comp ι_additiveObjIsoBiproduct_inv_assoc CategoryTheory.Limits.biproduct.ι_desc Finset.sum_congr CategoryTheory.comp_dite CategoryTheory.Limits.comp_zero Finset.sum_dite_eq' CategoryTheory.Category.comp_id CategoryTheory.dite_comp CategoryTheory.Limits.zero_comp Finset.sum_dite_eq CategoryTheory.Category.id_comp
additiveObjIsoBiproduct_naturality' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding X instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Iso.inv additiveObjIsoBiproduct CategoryTheory.Functor.map CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Finite.of_fintype fintype CategoryTheory.Limits.biproduct.matrix	—	instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Finite.of_fintype CategoryTheory.Iso.inv_comp_eq CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv additiveObjIsoBiproduct_naturality
additiveObjIsoBiproduct_naturality'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding X instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Iso.inv additiveObjIsoBiproduct CategoryTheory.Functor.map CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Finite.of_fintype fintype CategoryTheory.Limits.biproduct.matrix	—	instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite Finite.of_fintype CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' additiveObjIsoBiproduct_naturality'
additiveObjIsoBiproduct_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory CategoryTheory.Functor.map CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms embedding X instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Iso.hom additiveObjIsoBiproduct CategoryTheory.Limits.biproduct.matrix Finite.of_fintype fintype	—	instHasBiproductιObjEmbeddingXOfAdditive Finite.of_fintype CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' additiveObjIsoBiproduct_naturality
comp_apply 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Mat_ CategoryTheory.Category.toCategoryStruct instCategory Finset.sum ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver X AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.univ fintype	—	—
comp_def 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Mat_ CategoryTheory.Category.toCategoryStruct instCategory Finset.sum ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver X AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Finset.univ fintype	—	—
embeddingLiftIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Mat_ instCategory embedding lift CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category embeddingLiftIso CategoryTheory.Limits.biproduct.desc CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
embeddingLiftIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Mat_ instCategory embedding lift CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category embeddingLiftIso CategoryTheory.Limits.biproduct.lift CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
embedding_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Mat_ instCategory embedding	—	—
embedding_obj_X 📖	mathematical	—	X CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding	—	—
embedding_obj_fintype 📖	mathematical	—	fintype CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding PUnit.fintype	—	—
embedding_obj_ι 📖	mathematical	—	ι CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding	—	—
equivalenceSelfOfHasFiniteBiproducts_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Mat_ instCategory equivalenceSelfOfHasFiniteBiproducts lift CategoryTheory.Functor.id CategoryTheory.Functor.instAdditiveId	—	—
equivalenceSelfOfHasFiniteBiproducts_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Mat_ instCategory equivalenceSelfOfHasFiniteBiproducts embedding	—	—
hasFiniteBiproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteBiproducts CategoryTheory.Mat_ instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	—	CategoryTheory.Limits.hasBiproduct_of_total hom_ext Finset.sum_congr CategoryTheory.dite_comp CategoryTheory.comp_dite CategoryTheory.eqToHom_trans CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp Finset.sum_sigma Finset.sum_dite_irrel Finset.sum_const_zero Finset.sum_dite_eq' id_apply_self CategoryTheory.eqToHom_refl id_apply_of_ne Finset.sum_apply Finset.sum_eq_single Finset.sum_eq_zero CategoryTheory.Category.id_comp
hom_ext 📖	—	—	—	—	DMatrix.ext_iff
hom_ext_iff 📖	—	—	—	—	hom_ext
id_apply 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat_ CategoryTheory.Category.toCategoryStruct instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver X ι CategoryTheory.eqToHom CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
id_apply_of_ne 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat_ CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	—	—
id_apply_self 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat_ CategoryTheory.Category.toCategoryStruct instCategory X	—	—
id_def 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Mat_ CategoryTheory.Category.toCategoryStruct instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver X ι CategoryTheory.eqToHom CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
instHasBiproductιObjEmbeddingXOfAdditive 📖	mathematical	—	CategoryTheory.Limits.HasBiproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding X	—	CategoryTheory.Functor.hasBiproduct_of_preserves CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.PreservesBiproductsOfShape.preserves CategoryTheory.Limits.PreservesFiniteBiproducts.preserves CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive
isoBiproductEmbedding_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Mat_ instCategory CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Functor.obj embedding X CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype fintype isoBiproductEmbedding CategoryTheory.Limits.biproduct.lift CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype
isoBiproductEmbedding_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Mat_ instCategory CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Functor.obj embedding X CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype fintype isoBiproductEmbedding CategoryTheory.Limits.biproduct.desc CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype
lift_additive 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Mat_ instCategory instPreadditive lift	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite CategoryTheory.Functor.map_add CategoryTheory.Limits.biproduct.hom_ext CategoryTheory.Limits.biproduct.hom_ext' CategoryTheory.Limits.biproduct.matrix_π CategoryTheory.Limits.biproduct.ι_desc CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.comp_add
lift_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Mat_ instCategory lift CategoryTheory.Limits.biproduct.matrix ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj X	—	CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite
lift_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory lift CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms X	—	—
ι_additiveObjIsoBiproduct_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding X CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.biproduct.ι CategoryTheory.Iso.inv additiveObjIsoBiproduct CategoryTheory.Functor.map instPreadditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype fintype isoBiproductEmbedding	—	instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype CategoryTheory.Functor.hasBiproduct_of_preserves CategoryTheory.Limits.biproduct.ι_desc_assoc CategoryTheory.Functor.map_comp CategoryTheory.Limits.biproduct.ι_desc
ι_additiveObjIsoBiproduct_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Mat_ instCategory embedding X CategoryTheory.Limits.biproduct ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.biproduct.ι CategoryTheory.Iso.inv additiveObjIsoBiproduct CategoryTheory.Functor.map instPreadditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype fintype isoBiproductEmbedding	—	instHasBiproductιObjEmbeddingXOfAdditive CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite hasFiniteBiproducts Finite.of_fintype CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_additiveObjIsoBiproduct_inv

CategoryTheory.Mat_.Embedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveEmbedding 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory CategoryTheory.Mat_.instPreadditive CategoryTheory.Mat_.embedding	—	—
instFaithfulEmbedding 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory CategoryTheory.Mat_.embedding	—	—
instFullEmbedding 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Mat_ CategoryTheory.Mat_.instCategory CategoryTheory.Mat_.embedding	—	—

CategoryTheory.Mat_.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	—
id 📖	CompOp	—

---

← Back to Index