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	—
`instAddHom` 📖	CompOp	1 math math: `add_hom`
`instHasZeroMorphisms` 📖	CompOp	6 math math: `forget₂_preservesZeroMorphisms`, `forget_preservesZeroMorphisms`, `FDRep.instHasKernels`, `FDRep.simple_iff_end_is_rank_one`, `functorCategoryEquivalence_preservesZeroMorphisms`, `FDRep.simple_iff_char_is_norm_one`
`instLinear` 📖	CompOp	13 math math: `smul_hom`, `FDRep.instFiniteDimensionalHom`, `ContinuousCohomology.instLinearActionTopModuleCatInvariants`, `CategoryTheory.Functor.mapAction_linear`, `FDRep.simple_iff_end_is_rank_one`, `ContinuousCohomology.instLinearActionTopModuleCatI`, `forget_linear`, `functorCategoryEquivalence_linear`, `res_linear`, `FDRep.scalar_product_char_eq_finrank_equivariant`, `instMonoidalLinear`, `forget₂_linear`, `FDRep.finrank_hom_simple_simple`
`instNegHom` 📖	CompOp	1 math math: `neg_hom`
`instPreadditive` 📖	CompOp	25 math math: `sum_hom`, `smul_hom`, `FDRep.instFiniteDimensionalHom`, `ContinuousCohomology.instLinearActionTopModuleCatInvariants`, `ContinuousCohomology.instAdditiveActionTopModuleCatInvariants`, `CategoryTheory.Functor.mapAction_linear`, `res_additive`, `ContinuousCohomology.MultiInd.d_comp_d_assoc`, `CategoryTheory.Functor.mapAction_preadditive`, `forget_additive`, `FDRep.simple_iff_end_is_rank_one`, `ContinuousCohomology.instLinearActionTopModuleCatI`, `instMonoidalPreadditive`, `ContinuousCohomology.MultiInd.d_comp_d`, `forget_linear`, `functorCategoryEquivalence_linear`, `res_linear`, `ContinuousCohomology.MultiInd.d_succ`, `FDRep.scalar_product_char_eq_finrank_equivariant`, `instMonoidalLinear`, `functorCategoryEquivalence_additive`, `forget₂_linear`, `ContinuousCohomology.instAdditiveActionTopModuleCatI`, `forget₂_additive`, `FDRep.finrank_hom_simple_simple`
`instSMulIntHom` 📖	CompOp	1 math math: `zsmul_hom`
`instSMulNatHom` 📖	CompOp	1 math math: `nsmul_hom`
`instSubHom` 📖	CompOp	1 math math: `sub_hom`
`instZeroHom` 📖	CompOp	1 math math: `zero_hom`

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.toNSMul` `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`
`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`
`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