AdditiveFunctor

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

Statistics

Metric	Count
Definitions AdditiveFunctor, forget, of, ofExact, ofLeftExact, ofRightExact, mapAddHom, additiveFunctor, «term_⥤+_»	9
Theorems forget_map, forget_obj, forget_obj_of, ofExact_map, ofExact_map_hom, ofExact_obj_fst, ofLeftExact_map, ofLeftExact_map_hom, ofLeftExact_obj_fst, ofRightExact_map, ofRightExact_map_hom, ofRightExact_obj_fst, of_fst, of_obj, inverse_additive, map_add, additive_of_comp_faithful, additive_of_full_essSurj_comp, additive_of_iso, additive_of_preservesBinaryBiproducts, additive_of_preserves_binary_products, coe_mapAddHom, fullSubcategoryInclusion_additive, hasZeroObject_of_additive, inducedFunctor_additive, instAdditiveComp, instAdditiveFullSubcategoryLift, instAdditiveId, instAdditiveObjEvaluation, mapAddHom_apply, map_add, map_neg, map_nsmul, map_sub, map_sum, map_zsmul, preservesFiniteBiproductsOfAdditive, preservesFiniteCoproductsOfAdditive, preservesFiniteProductsOfAdditive, preservesZeroMorphisms_of_additive, additiveFunctor_iff, exactFunctor_le_additiveFunctor, instAdditiveAdditiveFunctorFunctorForget, instAdditiveObjFunctorAdditiveFunctor, instAdditiveObjFunctorAdditiveFunctor_1, leftExactFunctor_le_additiveFunctor, rightExactFunctor_le_additiveFunctor	47
Total	56

CategoryTheory

Definitions

Name	Category	Theorems
AdditiveFunctor 📖	CompOp	13 math math: AdditiveFunctor.ofExact_obj_fst, AdditiveFunctor.ofLeftExact_map, AdditiveFunctor.ofRightExact_map, AdditiveFunctor.ofExact_map, AdditiveFunctor.forget_obj_of, AdditiveFunctor.forget_obj, AdditiveFunctor.ofLeftExact_obj_fst, AdditiveFunctor.forget_map, AdditiveFunctor.ofRightExact_obj_fst, instAdditiveAdditiveFunctorFunctorForget, AdditiveFunctor.ofExact_map_hom, AdditiveFunctor.ofLeftExact_map_hom, AdditiveFunctor.ofRightExact_map_hom
additiveFunctor 📖	CompOp	21 math math: instAdditiveObjFunctorAdditiveFunctor, instAdditiveObjFunctorAdditiveFunctor_1, exactFunctor_le_additiveFunctor, AdditiveFunctor.ofExact_obj_fst, AdditiveFunctor.ofLeftExact_map, AdditiveFunctor.ofRightExact_map, AdditiveFunctor.ofExact_map, AdditiveFunctor.forget_obj_of, AdditiveFunctor.forget_obj, leftExactFunctor_le_additiveFunctor, AdditiveFunctor.ofLeftExact_obj_fst, AdditiveFunctor.forget_map, AdditiveFunctor.ofRightExact_obj_fst, AdditiveFunctor.of_obj, AdditiveFunctor.of_fst, instAdditiveAdditiveFunctorFunctorForget, AdditiveFunctor.ofExact_map_hom, rightExactFunctor_le_additiveFunctor, AdditiveFunctor.ofLeftExact_map_hom, additiveFunctor_iff, AdditiveFunctor.ofRightExact_map_hom
«term_⥤+_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
additiveFunctor_iff 📖	mathematical	—	additiveFunctor Functor.Additive	—	—
exactFunctor_le_additiveFunctor 📖	mathematical	—	ObjectProperty Functor Category.toCategoryStruct Functor.category Pi.hasLe Prop.le exactFunctor additiveFunctor	—	LE.le.trans exactFunctor_le_leftExactFunctor leftExactFunctor_le_additiveFunctor
instAdditiveAdditiveFunctorFunctorForget 📖	mathematical	—	Functor.Additive AdditiveFunctor Functor ObjectProperty.FullSubcategory.category Functor.category additiveFunctor Preadditive.fullSubcategory functorCategoryPreadditive AdditiveFunctor.forget	—	—
instAdditiveObjFunctorAdditiveFunctor 📖	mathematical	—	Functor.Additive ObjectProperty.FullSubcategory.obj Functor Functor.category additiveFunctor	—	ObjectProperty.FullSubcategory.property
instAdditiveObjFunctorAdditiveFunctor_1 📖	mathematical	—	Functor.Additive ObjectProperty.FullSubcategory.obj Functor Functor.category additiveFunctor	—	ObjectProperty.FullSubcategory.property
leftExactFunctor_le_additiveFunctor 📖	mathematical	—	ObjectProperty Functor Category.toCategoryStruct Functor.category Pi.hasLe Prop.le leftExactFunctor additiveFunctor	—	Functor.additive_of_preservesBinaryBiproducts Functor.preservesZeroMorphisms_of_preserves_terminal_object Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesFiniteLimits.preservesFiniteLimits Limits.preservesBinaryBiproducts_of_preservesBinaryProducts
rightExactFunctor_le_additiveFunctor 📖	mathematical	—	ObjectProperty Functor Category.toCategoryStruct Functor.category Pi.hasLe Prop.le rightExactFunctor additiveFunctor	—	Functor.additive_of_preservesBinaryBiproducts Functor.preservesZeroMorphisms_of_preserves_initial_object Limits.PreservesColimitsOfShape.preservesColimit Limits.PreservesFiniteColimits.preservesFiniteColimits Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts

CategoryTheory.AdditiveFunctor

Definitions

Name	Category	Theorems
forget 📖	CompOp	4 math math: forget_obj_of, forget_obj, forget_map, CategoryTheory.instAdditiveAdditiveFunctorFunctorForget
of 📖	CompOp	3 math math: forget_obj_of, of_obj, of_fst
ofExact 📖	CompOp	3 math math: ofExact_obj_fst, ofExact_map, ofExact_map_hom
ofLeftExact 📖	CompOp	3 math math: ofLeftExact_map, ofLeftExact_obj_fst, ofLeftExact_map_hom
ofRightExact 📖	CompOp	3 math math: ofRightExact_map, ofRightExact_obj_fst, ofRightExact_map_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.AdditiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor forget CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.AdditiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor forget CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—
forget_obj_of 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.AdditiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor forget of	—	—
ofExact_map 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.ExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.exactFunctor CategoryTheory.AdditiveFunctor ofExact CategoryTheory.Functor.map	—	ofExact_map_hom
ofExact_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.ExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.exactFunctor CategoryTheory.AdditiveFunctor ofExact CategoryTheory.Functor.map	—	—
ofExact_obj_fst 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.Functor.obj CategoryTheory.ExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.exactFunctor CategoryTheory.AdditiveFunctor ofExact	—	—
ofLeftExact_map 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.LeftExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.leftExactFunctor CategoryTheory.AdditiveFunctor ofLeftExact CategoryTheory.Functor.map	—	ofLeftExact_map_hom
ofLeftExact_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.LeftExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.leftExactFunctor CategoryTheory.AdditiveFunctor ofLeftExact CategoryTheory.Functor.map	—	—
ofLeftExact_obj_fst 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.Functor.obj CategoryTheory.LeftExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.leftExactFunctor CategoryTheory.AdditiveFunctor ofLeftExact	—	—
ofRightExact_map 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.RightExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.rightExactFunctor CategoryTheory.AdditiveFunctor ofRightExact CategoryTheory.Functor.map	—	ofRightExact_map_hom
ofRightExact_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.RightExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.rightExactFunctor CategoryTheory.AdditiveFunctor ofRightExact CategoryTheory.Functor.map	—	—
ofRightExact_obj_fst 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor CategoryTheory.Functor.obj CategoryTheory.RightExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.rightExactFunctor CategoryTheory.AdditiveFunctor ofRightExact	—	—
of_fst 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor of	—	—
of_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.additiveFunctor of	—	—

CategoryTheory.Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_additive 📖	mathematical	—	CategoryTheory.Functor.Additive inverse	—	CategoryTheory.Functor.map_injective faithful_functor fun_inv_map CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.comp_add CategoryTheory.Functor.map_add

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapAddHom 📖	CompOp	4 math math: CategoryTheory.preadditiveYonedaMap_app, coe_mapAddHom, mapAddHom_apply, mapLinearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
additive_of_comp_faithful 📖	mathematical	—	Additive	—	map_injective comp_map map_add
additive_of_full_essSurj_comp 📖	mathematical	—	Additive	—	map_surjective CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso map_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Preadditive.add_comp CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Preadditive.comp_add map_add
additive_of_iso 📖	mathematical	—	Additive	—	CategoryTheory.NatIso.naturality_1 map_add CategoryTheory.Preadditive.add_comp CategoryTheory.NatTrans.naturality CategoryTheory.Preadditive.comp_add CategoryTheory.Iso.inv_hom_id_app_assoc
additive_of_preservesBinaryBiproducts 📖	mathematical	—	Additive	—	CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Limits.biprod.add_eq_lift_id_desc map_comp hasBinaryBiproduct_of_preserves CategoryTheory.Limits.PreservesBinaryBiproducts.preserves CategoryTheory.Limits.biprod.lift_mapBiprod CategoryTheory.Limits.biprod.mapBiprod_hom_desc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc map_id
additive_of_preserves_binary_products 📖	mathematical	—	Additive	—	CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts additive_of_preservesBinaryBiproducts
coe_mapAddHom 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike mapAddHom map	—	—
fullSubcategoryInclusion_additive 📖	mathematical	—	Additive CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Preadditive.fullSubcategory CategoryTheory.ObjectProperty.ι	—	—
hasZeroObject_of_additive 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject	—	CategoryTheory.Limits.IsZero.iff_id_eq_zero map_id CategoryTheory.Limits.id_zero map_zero preservesZeroMorphisms_of_additive
inducedFunctor_additive 📖	mathematical	—	Additive CategoryTheory.InducedCategory CategoryTheory.InducedCategory.instCategory CategoryTheory.Preadditive.inducedCategory CategoryTheory.inducedFunctor	—	—
instAdditiveComp 📖	mathematical	—	Additive comp	—	map_add
instAdditiveFullSubcategoryLift 📖	mathematical	obj	Additive CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Preadditive.fullSubcategory CategoryTheory.ObjectProperty.lift	—	map_add
instAdditiveId 📖	mathematical	—	Additive id	—	—
instAdditiveObjEvaluation 📖	mathematical	—	Additive CategoryTheory.Functor category CategoryTheory.functorCategoryPreadditive obj CategoryTheory.evaluation	—	—
mapAddHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike mapAddHom map	—	—
map_add 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup obj	—	Additive.map_add
map_neg 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup obj	—	AddMonoidHom.map_neg
map_nsmul 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup obj	—	AddMonoidHom.map_nsmul
map_sub 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup obj	—	AddMonoidHom.map_sub
map_sum 📖	mathematical	—	map Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup obj	—	map_sum AddMonoidHom.instAddMonoidHomClass
map_zsmul 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup obj	—	AddMonoidHom.map_zsmul
preservesFiniteBiproductsOfAdditive 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteBiproducts CategoryTheory.Preadditive.preadditiveHasZeroMorphisms preservesZeroMorphisms_of_additive	—	preservesZeroMorphisms_of_additive nonempty_fintype Finset.sum_congr mapBicone_π mapBicone_ι map_comp map_sum map_id CategoryTheory.Limits.IsBilimit.total
preservesFiniteCoproductsOfAdditive 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteCoproducts	—	CategoryTheory.Limits.preservesCoproductsOfShape_of_preservesBiproductsOfShape preservesZeroMorphisms_of_additive Finite.of_fintype CategoryTheory.Limits.PreservesFiniteBiproducts.preserves preservesFiniteBiproductsOfAdditive
preservesFiniteProductsOfAdditive 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts	—	CategoryTheory.Limits.preservesProductsOfShape_of_preservesBiproductsOfShape preservesZeroMorphisms_of_additive Finite.of_fintype CategoryTheory.Limits.PreservesFiniteBiproducts.preserves preservesFiniteBiproductsOfAdditive
preservesZeroMorphisms_of_additive 📖	mathematical	—	PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	AddMonoidHom.map_zero

CategoryTheory.Functor.Additive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add 📖	mathematical	—	CategoryTheory.Functor.map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.obj	—	—

---

← Back to Index