FunctorCategory

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

Statistics

Metric	Count
Definitions appHom, functorCategoryPreadditive, instAddHomFunctor, instNegHomFunctor, instZeroHomFunctor	5
Theorems appHom_apply, app_add, app_neg, app_nsmul, app_sub, app_sum, app_units_zsmul, app_zero, app_zsmul	9
Total	14

CategoryTheory

Definitions

Name	Category	Theorems
functorCategoryPreadditive 📖	CompOp	89 math math: HomologicalComplex.mapBifunctor₁₂.ι_D₃_assoc, HomologicalComplex.mapBifunctor₁₂.d_eq, CatCenter.app_sub, Linear.smulOfRingMorphism_smul_eq', Functor.commShiftIso_map₂CochainComplex_flip_hom_app, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, HomologicalComplex.ι_mapBifunctorAssociatorX_hom, HomologicalComplex.mapBifunctor₁₂.ι_D₁_assoc, HomologicalComplex.mapBifunctorMapHomotopy.comm₁, HomologicalComplex.mapBifunctor₁₂.hom_ext_iff, HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc, HomologicalComplex.mapBifunctor₁₂.ι_D₂_assoc, NatTrans.app_nsmul, instPreservesFiniteBiproductsTensorRight, HomologicalComplex.mapBifunctorAssociatorX_hom_D₂, Module.Flat.iff_rTensor_preserves_shortComplex_exact, HomologicalComplex.mapBifunctorMapHomotopy.zero₁, Linear.smulOfRingMorphism_smul_eq, CatCenter.app_add, HomologicalComplex.mapBifunctor₁₂.d₂_eq_zero, HomologicalComplex.mapBifunctor₁₂.ιOrZero_eq_zero, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, HomologicalComplex.mapBifunctorAssociatorX_hom_D₃_assoc, HomologicalComplex.mapBifunctor₁₂.ι_D₁, ModuleCat.smulNatTrans_apply_app, HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom, HomologicalComplex.tensor_unit_d₂, HomologicalComplex.mapBifunctorAssociatorX_hom_D₂_assoc, MonoidalPreadditive.instAdditiveFunctorCurriedTensor, Functor.commShiftIso_map₂CochainComplex_inv_app, HomologicalComplex.mapBifunctor₁₂.ι_D₃, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, NatTrans.app_sum, HomologicalComplex.mapBifunctorAssociatorX_hom_D₁, NatTrans.appHom_apply, Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, HomologicalComplex.mapBifunctor₁₂.d₃_eq_zero, Functor.commShiftIso_map₂CochainComplex_flip_inv_app, presheafToSheaf_additive, MonoidalPreadditive.instAdditiveFunctorFlipCurriedTensor, CatCenter.app_neg_one_zpow, CatCenter.localization_zero, NatTrans.appLinearMap_apply, instPreservesHomologyFunctorAddCommGrpCatColim, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, Functor.instAdditiveObjEvaluation, CochainComplex.instHasMapBifunctorObjIntShiftFunctor, GrothendieckTopology.MayerVietorisSquare.shortComplex_f, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, NatTrans.app_smul, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, HomologicalComplex.mapBifunctorAssociatorX_hom_D₃, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, HomologicalComplex.mapBifunctor₁₂.d₁_eq_zero, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, Sheaf.Hom.add_app, NatTrans.app_units_zsmul, HomologicalComplex.unit_tensor_d₁, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, instAdditiveAdditiveFunctorFunctorForget, Action.functorCategoryEquivalence_linear, HomologicalComplex.mapBifunctor₁₂.ι_eq, HomologicalComplex.mapBifunctor₁₂.d₁_eq, NatTrans.app_zsmul, ContinuousCohomology.MultiInd.d_succ, HomologicalComplex.mapBifunctor₁₂.d₃_eq, Linear.toCatCenter_apply_app, HomologicalComplex.mapBifunctor₁₂.ι_D₂, CatCenter.app_neg, Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex, HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc_assoc, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, CommShift₂Setup.int_ε, Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex, Action.functorCategoryEquivalence_additive, Functor.commShiftIso_map₂CochainComplex_hom_app, HomologicalComplex.mapBifunctor₁₂.d₂_eq, NatTrans.app_sub, HomologicalComplex.mapBifunctorAssociatorX_hom_D₁_assoc, PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, CatCenter.localization_add, Module.Flat.rTensor_shortComplex_exact, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc, instAdditiveFunctorColim, CommShift₂Setup.int_z, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f
instAddHomFunctor 📖	CompOp	2 math math: Localization.liftNatTrans_add, NatTrans.app_add
instNegHomFunctor 📖	CompOp	1 math math: NatTrans.app_neg
instZeroHomFunctor 📖	CompOp	17 math math: Triangulated.TStructure.truncGEδLT_comp_truncLTι, Triangulated.TStructure.truncGEπ_comp_truncGEδLT_assoc, Triangulated.TStructure.truncLTι_comp_truncGEπ_assoc, Abelian.Preradical.ι_π_assoc, Abelian.Preradical.toColon_hom_left_colonπ_assoc, Triangulated.TStructure.eTruncGEπ_top, Abelian.Preradical.ι_π, ContinuousCohomology.MultiInd.d_comp_d_assoc, NatTrans.app_zero, Abelian.Preradical.toColon_hom_left_colonπ, Triangulated.TStructure.truncGEδLT_comp_truncLTι_assoc, Triangulated.TStructure.truncGEπ_comp_truncGEδLT, ContinuousCohomology.MultiInd.d_comp_d, Triangulated.TStructure.truncLTι_comp_truncGEπ, Triangulated.TStructure.eTruncLT_ι_bot, GrothendieckTopology.diagramNatTrans_zero, GrothendieckTopology.plusMap_zero

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
appHom 📖	CompOp	1 math math: appHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
appHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive AddMonoidHom.instFunLike appHom app	—	—
app_add 📖	mathematical	—	app Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.instAddHomFunctor CategoryTheory.Functor.obj AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
app_neg 📖	mathematical	—	app Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.instNegHomFunctor CategoryTheory.Functor.obj NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
app_nsmul 📖	mathematical	—	app Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.obj	—	AddMonoidHom.map_nsmul
app_sub 📖	mathematical	—	app Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.obj	—	—
app_sum 📖	mathematical	—	app Finset.sum Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.obj	—	map_sum AddMonoidHom.instAddMonoidHomClass Finset.sum_congr
app_units_zsmul 📖	mathematical	—	app Units Int.instMonoid Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.obj	—	app_zsmul
app_zero 📖	mathematical	—	app Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.instZeroHomFunctor CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
app_zsmul 📖	mathematical	—	app Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.obj	—	AddMonoidHom.map_zsmul

---

← Back to Index