Limits

📁 Source: Mathlib/CategoryTheory/Action/Limits.lean

Statistics

Metric	Count
Definitions `abelianAux`, `instAbelian`, `instAddHom`, `instHasZeroMorphisms`, `instLinear`, `instNegHom`, `instPreadditive`, `instSMulIntHom`, `instSMulNatHom`, `instSubHom`, `instZeroHom`	11
Theorems `instPreservesFiniteColimitsMapActionOfHasFiniteColimits`, `instPreservesFiniteLimitsMapActionOfHasFiniteLimits`, `mapActionPreservesColimit_of_preserves`, `mapActionPreservesColimitsOfShapeOfPreserves`, `mapActionPreservesLimit_of_preserves`, `mapActionPreservesLimitsOfShapeOfPreserves`, `preservesColimitsOfSize_of_preserves`, `preservesLimitsOfSize_of_preserves`, `add_hom`, `forget_additive`, `forget_linear`, `forget_preservesZeroMorphisms`, `forget₂_additive`, `forget₂_linear`, `forget₂_preservesZeroMorphisms`, `functorCategoryEquivalence_additive`, `functorCategoryEquivalence_linear`, `functorCategoryEquivalence_preservesZeroMorphisms`, `hasColimitsOfShape`, `hasLimitsOfShape`, `instHasColimits`, `instHasFiniteColimits`, `instHasFiniteCoproducts`, `instHasFiniteLimits`, `instHasFiniteProducts`, `instHasLimits`, `instPreservesColimitForgetOfHasColimitComp`, `instPreservesColimitsOfShapeForgetOfHasColimitsOfShape`, `instPreservesFiniteColimitsForgetOfHasFiniteColimits`, `instPreservesFiniteLimitsForgetOfHasFiniteLimits`, `instPreservesLimitForgetOfHasLimitComp`, `instPreservesLimitsOfShapeForgetOfHasLimitsOfShape`, `instReflectsColimitForget`, `instReflectsColimitsForget`, `instReflectsColimitsOfShapeForget`, `instReflectsLimitForget`, `instReflectsLimitsForget`, `instReflectsLimitsOfShapeForget`, `neg_hom`, `nsmul_hom`, `preservesColimit_of_preserves`, `preservesColimitsOfShape_of_preserves`, `preservesColimitsOfSize_of_preserves`, `preservesLimit_of_preserves`, `preservesLimitsOfShape_of_preserves`, `preservesLimitsOfSize_of_preserves`, `res_additive`, `res_linear`, `smul_hom`, `sub_hom`, `sum_hom`, `zero_hom`, `zsmul_hom`, `mapAction_linear`, `mapAction_preadditive`	55
Total	66

Action

Definitions

Name	Category	Theorems
`abelianAux` 📖	CompOp	—
`instAbelian` 📖	CompOp	15 math math: `Rep.standardComplex.εToSingle₀_comp_eq`, `Rep.barResolution_complex`, `Rep.Tor_map`, `Rep.standardComplex.quasiIso_forget₂_εToSingle₀`, `inhomogeneousCochains.d_eq`, `Rep.FiniteCyclicGroup.resolution_complex`, `Rep.standardComplex.instQuasiIsoNatεToSingle₀`, `Rep.FiniteCyclicGroup.resolution_quasiIso`, `Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply`, `Rep.Tor_obj`, `Rep.FiniteCyclicGroup.resolution_π`, `Rep.FiniteCyclicGroup.resolution.π_f`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply`
`instAddHom` 📖	CompOp	1 math math: `add_hom`
`instHasZeroMorphisms` 📖	CompOp	32 math math: `groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor`, `Rep.barComplex.d_def`, `groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top`, `groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor`, `Rep.FiniteCyclicGroup.chainComplexFunctor_obj`, `forget₂_preservesZeroMorphisms`, `forget_preservesZeroMorphisms`, `Rep.barResolution_complex`, `Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor`, `Rep.FiniteCyclicGroup.chainComplexFunctor_map_f`, `Rep.coinvariantsShortComplex_g`, `Rep.coinvariantsShortComplex_f`, `FDRep.instHasKernels`, `FDRep.simple_iff_end_is_rank_one`, `groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor`, `Rep.FiniteCyclicGroup.resolution_complex`, `groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor`, `Rep.standardComplex.instQuasiIsoNatεToSingle₀`, `Rep.FiniteCyclicGroup.resolution_quasiIso`, `Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply`, `Rep.coinvariantsShortComplex_X₁`, `Rep.coinvariantsShortComplex_X₂`, `functorCategoryEquivalence_preservesZeroMorphisms`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply`, `Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor`, `Rep.coinvariantsShortComplex_X₃`, `Rep.coinvariantsShortComplex_shortExact`, `Rep.FiniteCyclicGroup.resolution_π`, `Rep.FiniteCyclicGroup.resolution.π_f`, `FDRep.simple_iff_char_is_norm_one`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply`
`instLinear` 📖	CompOp	9 math math: `smul_hom`, `ContinuousCohomology.instLinearActionTopModuleCatInvariants`, `CategoryTheory.Functor.mapAction_linear`, `ContinuousCohomology.instLinearActionTopModuleCatI`, `forget_linear`, `functorCategoryEquivalence_linear`, `res_linear`, `instMonoidalLinear`, `forget₂_linear`
`instNegHom` 📖	CompOp	1 math math: `neg_hom`
`instPreadditive` 📖	CompOp	67 math math: `Rep.resCoindHomEquiv_symm_apply_hom`, `Rep.resCoindHomEquiv_apply_hom`, `Rep.MonoidalClosed.linearHomEquiv_symm_hom`, `sum_hom`, `Rep.diagonalHomEquiv_symm_apply`, `Rep.standardComplex.d_eq`, `Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply`, `smul_hom`, `Rep.instLinearModuleCatObjFunctorCoinvariantsTensor`, `Rep.MonoidalClosed.linearHomEquivComm_hom`, `Rep.standardComplex.εToSingle₀_comp_eq`, `Rep.coindVEquiv_symm_apply_coe`, `ContinuousCohomology.instLinearActionTopModuleCatInvariants`, `Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor`, `Rep.resIndAdjunction_homEquiv_symm_apply`, `ContinuousCohomology.instAdditiveActionTopModuleCatInvariants`, `Rep.instLinearModuleCatCoinvariantsFunctor`, `Rep.coindMap'_hom`, `CategoryTheory.Functor.mapAction_linear`, `res_additive`, `Rep.freeLiftLEquiv_apply`, `ContinuousCohomology.MultiInd.d_comp_d_assoc`, `Rep.resIndAdjunction_homEquiv_apply`, `Rep.coindFunctorIso_inv_app_hom_hom_apply_coe`, `Rep.leftRegularHomEquiv_symm_apply`, `Rep.coindResAdjunction_homEquiv_apply`, `CategoryTheory.Functor.mapAction_preadditive`, `Representation.coind'_apply_apply`, `forget_additive`, `Rep.coindIso_inv_hom_hom`, `Representation.linHom.invariantsEquivRepHom_symm_apply_coe`, `Rep.instLinearModuleCatInvariantsFunctor`, `Rep.standardComplex.quasiIso_forget₂_εToSingle₀`, `Rep.standardComplex.d_comp_ε`, `Rep.coindResAdjunction_homEquiv_symm_apply`, `Rep.coindVEquiv_apply_hom`, `Rep.leftRegularHomEquiv_symm_single`, `inhomogeneousCochains.d_eq`, `Rep.standardComplex.instQuasiIsoNatεToSingle₀`, `Rep.standardComplex.x_projective`, `groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor`, `Rep.MonoidalClosed.linearHomEquiv_hom`, `Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply`, `ContinuousCohomology.instLinearActionTopModuleCatI`, `instMonoidalPreadditive`, `ContinuousCohomology.MultiInd.d_comp_d`, `Rep.leftRegularHomEquiv_apply`, `forget_linear`, `Rep.diagonalHomEquiv_apply`, `functorCategoryEquivalence_linear`, `Rep.freeLiftLEquiv_symm_apply`, `Rep.MonoidalClosed.linearHomEquivComm_symm_hom`, `Rep.indResHomEquiv_apply_hom`, `res_linear`, `ContinuousCohomology.MultiInd.d_succ`, `instMonoidalLinear`, `functorCategoryEquivalence_additive`, `Representation.linHom.invariantsEquivRepHom_apply_hom`, `Rep.instAdditiveModuleCatInvariantsFunctor`, `forget₂_linear`, `Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq`, `Rep.coindIso_hom_hom_hom`, `Rep.instAdditiveModuleCatCoinvariantsFunctor`, `Rep.indResHomEquiv_symm_apply_hom`, `ContinuousCohomology.instAdditiveActionTopModuleCatI`, `forget₂_additive`
`instSMulIntHom` 📖	CompOp	1 math math: `zsmul_hom`
`instSMulNatHom` 📖	CompOp	1 math math: `nsmul_hom`
`instSubHom` 📖	CompOp	15 math math: `Rep.FiniteCyclicGroup.chainComplexFunctor_obj`, `Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff`, `Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff`, `Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff`, `Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff`, `sub_hom`, `Rep.FiniteCyclicGroup.chainComplexFunctor_map_f`, `Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff`, `Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff`, `Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm`, `Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff`, `Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub`, `Rep.FiniteCyclicGroup.resolution.π_f`, `Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination`, `Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff`
`instZeroHom` 📖	CompOp	8 math math: `groupHomology.mapShortComplexH1_zero`, `groupHomology.mapShortComplexH2_zero`, `groupCohomology.cochainsMap_zero`, `groupCohomology.mapShortComplexH2_zero`, `zero_hom`, `Rep.standardComplex.d_comp_ε`, `groupCohomology.mapShortComplexH1_zero`, `groupHomology.chainsMap_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_hom` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instAddHom` `V` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup`	—	—
`forget_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `Action` `instCategory` `instPreadditive` `forget`	—	—
`forget_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `Action` `instCategory` `instPreadditive` `instLinear` `forget`	—	—
`forget_preservesZeroMorphisms` 📖	mathematical	—	`CategoryTheory.Functor.PreservesZeroMorphisms` `Action` `instCategory` `instHasZeroMorphisms` `forget`	—	—
`forget₂_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `Action` `instCategory` `instPreadditive` `CategoryTheory.forget₂` `HomSubtype` `V` `instFunLikeHomSubtypeV` `instConcreteCategoryHomSubtypeV` `hasForgetToV`	—	—
`forget₂_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `Action` `instCategory` `instPreadditive` `instLinear` `CategoryTheory.forget₂` `HomSubtype` `V` `instFunLikeHomSubtypeV` `instConcreteCategoryHomSubtypeV` `hasForgetToV`	—	—
`forget₂_preservesZeroMorphisms` 📖	mathematical	—	`CategoryTheory.Functor.PreservesZeroMorphisms` `Action` `instCategory` `instHasZeroMorphisms` `CategoryTheory.forget₂` `HomSubtype` `V` `instFunLikeHomSubtypeV` `instConcreteCategoryHomSubtypeV` `hasForgetToV`	—	—
`functorCategoryEquivalence_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `Action` `CategoryTheory.Functor` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `instCategory` `CategoryTheory.Functor.category` `instPreadditive` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Equivalence.functor` `functorCategoryEquivalence`	—	—
`functorCategoryEquivalence_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `Action` `CategoryTheory.Functor` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `instCategory` `CategoryTheory.Functor.category` `instPreadditive` `CategoryTheory.functorCategoryPreadditive` `instLinear` `CategoryTheory.functorCategoryLinear` `CategoryTheory.Equivalence.functor` `functorCategoryEquivalence`	—	—
`functorCategoryEquivalence_preservesZeroMorphisms` 📖	mathematical	—	`CategoryTheory.Functor.PreservesZeroMorphisms` `Action` `instCategory` `CategoryTheory.Functor` `CategoryTheory.SingleObj` `CategoryTheory.SingleObj.category` `CategoryTheory.Functor.category` `instHasZeroMorphisms` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Equivalence.functor` `functorCategoryEquivalence`	—	`CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.preservesZeroMorphisms_of_full` `CategoryTheory.Functor.IsEquivalence.full` `instIsEquivalenceFunctorSingleObjFunctor`
`hasColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `Action` `instCategory`	—	`CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasColimitsOfShape`
`hasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.HasLimitsOfShape` `Action` `instCategory`	—	`CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasLimitsOfShape`
`instHasColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasColimits` `Action` `instCategory`	—	`CategoryTheory.Adjunction.has_colimits_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasColimitsOfSize`
`instHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteColimits` `Action` `instCategory`	—	`CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits`
`instHasFiniteCoproducts` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteCoproducts` `Action` `instCategory`	—	`CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.Limits.instHasFiniteCoproductsFunctor` `Finite.of_fintype`
`instHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteLimits` `Action` `instCategory`	—	`CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits`
`instHasFiniteProducts` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteProducts` `Action` `instCategory`	—	`CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.Limits.instHasFiniteProductsFunctor` `Finite.of_fintype`
`instHasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `Action` `instCategory`	—	`CategoryTheory.Adjunction.has_limits_of_equivalence` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasLimitsOfSize`
`instPreservesColimitForgetOfHasColimitComp` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `Action` `instCategory` `forget`	—	`CategoryTheory.Limits.comp_preservesColimit` `CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.evaluation_preservesColimit`
`instPreservesColimitsOfShapeForgetOfHasColimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `Action` `instCategory` `forget`	—	`instPreservesColimitForgetOfHasColimitComp` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape`
`instPreservesFiniteColimitsForgetOfHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `Action` `instCategory` `forget`	—	`CategoryTheory.Limits.evaluation_preservesColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits` `CategoryTheory.Limits.comp_preservesFiniteColimits` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor`
`instPreservesFiniteLimitsForgetOfHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `Action` `instCategory` `forget`	—	`CategoryTheory.Limits.evaluation_preservesLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `CategoryTheory.Limits.comp_preservesFiniteLimits` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor`
`instPreservesLimitForgetOfHasLimitComp` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `Action` `instCategory` `forget`	—	`CategoryTheory.Limits.comp_preservesLimit` `CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit` `CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.evaluation_preservesLimit`
`instPreservesLimitsOfShapeForgetOfHasLimitsOfShape` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `Action` `instCategory` `forget`	—	`instPreservesLimitForgetOfHasLimitComp` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape`
`instReflectsColimitForget` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsColimit` `Action` `instCategory` `forget`	—	`CategoryTheory.CreatesColimit.toReflectsColimit` `CategoryTheory.Equivalence.isEquivalence_functor`
`instReflectsColimitsForget` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsColimits` `Action` `instCategory` `forget`	—	`instReflectsColimitsOfShapeForget`
`instReflectsColimitsOfShapeForget` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsColimitsOfShape` `Action` `instCategory` `forget`	—	`instReflectsColimitForget`
`instReflectsLimitForget` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsLimit` `Action` `instCategory` `forget`	—	`CategoryTheory.CreatesLimit.toReflectsLimit` `CategoryTheory.Equivalence.isEquivalence_functor`
`instReflectsLimitsForget` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsLimits` `Action` `instCategory` `forget`	—	`instReflectsLimitsOfShapeForget`
`instReflectsLimitsOfShapeForget` 📖	mathematical	—	`CategoryTheory.Limits.ReflectsLimitsOfShape` `Action` `instCategory` `forget`	—	`instReflectsLimitForget`
`neg_hom` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instNegHom` `V` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup`	—	—
`nsmul_hom` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulNatHom` `V` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup`	—	—
`preservesColimit_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `Action` `instCategory`	—	`CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves` `CategoryTheory.CreatesColimit.toReflectsColimit` `CategoryTheory.Equivalence.isEquivalence_functor`
`preservesColimitsOfShape_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `Action` `instCategory`	—	`preservesColimit_of_preserves` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit`
`preservesColimitsOfSize_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfSize` `Action` `instCategory`	—	`preservesColimitsOfShape_of_preserves` `CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape`
`preservesLimit_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `Action` `instCategory`	—	`CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves` `CategoryTheory.CreatesLimit.toReflectsLimit` `CategoryTheory.Equivalence.isEquivalence_functor`
`preservesLimitsOfShape_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `Action` `instCategory`	—	`preservesLimit_of_preserves` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit`
`preservesLimitsOfSize_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `Action` `instCategory`	—	`preservesLimitsOfShape_of_preserves` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape`
`res_additive` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `Action` `instCategory` `instPreadditive` `res`	—	—
`res_linear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `Action` `instCategory` `instPreadditive` `instLinear` `res`	—	—
`smul_hom` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `instPreadditive` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Linear.homModule` `instLinear` `V`	—	—
`sub_hom` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSubHom` `V` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup`	—	—
`sum_hom` 📖	mathematical	—	`Hom.hom` `Finset.sum` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `instPreadditive` `V`	—	`CategoryTheory.Functor.map_sum` `forget_additive`
`zero_hom` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instZeroHom` `V` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—
`zsmul_hom` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `Action` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instSMulIntHom` `V` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup`	—	—

Action.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPreservesFiniteColimitsMapActionOfHasFiniteColimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteColimits` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`mapActionPreservesColimitsOfShapeOfPreserves` `CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits` `CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits`
`instPreservesFiniteLimitsMapActionOfHasFiniteLimits` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`mapActionPreservesLimitsOfShapeOfPreserves` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits`
`mapActionPreservesColimit_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`Action.preservesColimit_of_preserves` `CategoryTheory.Limits.comp_preservesColimit` `Action.instPreservesColimitForgetOfHasColimitComp`
`mapActionPreservesColimitsOfShapeOfPreserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfShape` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`mapActionPreservesColimit_of_preserves` `CategoryTheory.Limits.instHasColimitCompOfPreservesColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `Action.hasColimitsOfShape` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `Action.instPreservesColimitsOfShapeForgetOfHasColimitsOfShape`
`mapActionPreservesLimit_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`Action.preservesLimit_of_preserves` `CategoryTheory.Limits.comp_preservesLimit` `Action.instPreservesLimitForgetOfHasLimitComp`
`mapActionPreservesLimitsOfShapeOfPreserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`mapActionPreservesLimit_of_preserves` `CategoryTheory.Limits.instHasLimitCompOfPreservesLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `Action.hasLimitsOfShape` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `Action.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape`
`preservesColimitsOfSize_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimitsOfSize` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`mapActionPreservesColimitsOfShapeOfPreserves` `CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize`
`preservesLimitsOfSize_of_preserves` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfSize` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction`	—	`mapActionPreservesLimitsOfShapeOfPreserves` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits`

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapAction_linear` 📖	mathematical	—	`Linear` `Action` `Action.instCategory` `Action.instPreadditive` `Action.instLinear` `mapAction`	—	`Action.hom_ext` `map_smul`
`mapAction_preadditive` 📖	mathematical	—	`Additive` `Action` `Action.instCategory` `Action.instPreadditive` `mapAction`	—	`Action.hom_ext` `map_add`

---

← Back to Index