Zero

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

Statistics

Metric	Count
Definitions `PreservesZeroMorphisms`, `mapZeroObject`	2
Theorems `map_zero`, `instPreservesZeroMorphismsFlipOfObj`, `instPreservesZeroMorphismsObjFlip`, `mapZeroObject_hom`, `mapZeroObject_inv`, `map_eq_zero_iff`, `map_isZero`, `map_zero`, `preservesColimitsOfShape_of_isZero`, `preservesColimitsOfSize_of_isZero`, `preservesInitialObject_of_preservesZeroMorphisms`, `preservesLimitsOfShape_of_isZero`, `preservesLimitsOfSize_of_isZero`, `preservesTerminalObject_of_preservesZeroMorphisms`, `preservesZeroMorphisms_comp`, `preservesZeroMorphisms_evaluation_obj`, `preservesZeroMorphisms_of_full`, `preservesZeroMorphisms_of_isLeftAdjoint`, `preservesZeroMorphisms_of_isRightAdjoint`, `preservesZeroMorphisms_of_iso`, `preservesZeroMorphisms_of_map_zero_object`, `preservesZeroMorphisms_of_preserves_initial_object`, `preservesZeroMorphisms_of_preserves_terminal_object`, `whiskerRight_zero`, `zero_of_map_zero`	25
Total	27

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`PreservesZeroMorphisms` 📖	CompData	38 math math: `groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor`, `groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor`, `Action.forget₂_preservesZeroMorphisms`, `Action.forget_preservesZeroMorphisms`, `preservesZeroMorphisms_of_isRightAdjoint`, `IsHomological.toPreservesZeroMorphisms`, `preservesZeroMorphisms_evaluation_obj`, `preservesZeroMorphisms_comp`, `CategoryTheory.ShortComplex.preservesZeroMorphisms_π₃`, `CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF`, `preservesZeroMorphisms_of_map_zero_object`, `IsTriangulated.instPreservesZeroMorphisms`, `HomologicalComplex.instPreservesZeroMorphismsEval`, `Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor`, `preservesZeroMorphisms_of_isLeftAdjoint`, `HomologicalComplex.instPreservesZeroMorphismsHomologyFunctor`, `preservesZeroMorphisms_of_full`, `CategoryTheory.ShortComplex.preservesZeroMorphisms_π₁`, `preservesZeroMorphisms_of_additive`, `ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexExtendFunctor`, `preservesZeroMorphisms_of_iso`, `CategoryTheory.plusPlusSheaf_preservesZeroMorphisms`, `groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor`, `preservesZeroMorphisms_of_preserves_initial_object`, `instPreservesZeroMorphismsObjFlip`, `CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsFReduced`, `groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor`, `CategoryTheory.GrothendieckTopology.plusFunctor_preservesZeroMorphisms`, `CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi`, `Action.functorCategoryEquivalence_preservesZeroMorphisms`, `HomologicalComplex.instPreservesZeroMorphismsCyclesFunctor`, `preservesZeroMorphisms_of_preserves_terminal_object`, `HomologicalComplex.instPreservesZeroMorphismsSingle`, `Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor`, `CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex`, `HomologicalComplex.instPreservesZeroMorphismsOpcyclesFunctor`, `CategoryTheory.ShortComplex.preservesZeroMorphisms_π₂`, `ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor`
`mapZeroObject` 📖	CompOp	2 math math: `mapZeroObject_inv`, `mapZeroObject_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPreservesZeroMorphismsFlipOfObj` 📖	mathematical	`PreservesZeroMorphisms` `obj` `CategoryTheory.Functor` `category`	`CategoryTheory.Limits.instHasZeroMorphismsFunctor` `flip`	—	`CategoryTheory.NatTrans.ext'` `map_zero`
`instPreservesZeroMorphismsObjFlip` 📖	mathematical	—	`PreservesZeroMorphisms` `obj` `CategoryTheory.Functor` `category` `flip`	—	`map_zero`
`mapZeroObject_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `obj` `CategoryTheory.Limits.HasZeroObject.zero'` `mapZeroObject` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—
`mapZeroObject_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `obj` `CategoryTheory.Limits.HasZeroObject.zero'` `mapZeroObject` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—
`map_eq_zero_iff` 📖	mathematical	—	`map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`zero_of_map_zero` `map_zero`
`map_isZero` 📖	mathematical	`CategoryTheory.Limits.IsZero`	`obj`	—	`map_id` `map_zero`
`map_zero` 📖	mathematical	—	`map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `obj`	—	`PreservesZeroMorphisms.map_zero`
`preservesColimitsOfShape_of_isZero` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor` `category`	`CategoryTheory.Limits.PreservesColimitsOfShape`	—	`isZero` `isZero_iff`
`preservesColimitsOfSize_of_isZero` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor` `category`	`CategoryTheory.Limits.PreservesColimitsOfSize`	—	`preservesColimitsOfShape_of_isZero`
`preservesInitialObject_of_preservesZeroMorphisms` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `empty`	—	`CategoryTheory.Limits.preservesInitial_of_iso` `CategoryTheory.Limits.HasZeroObject.hasInitial`
`preservesLimitsOfShape_of_isZero` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor` `category`	`CategoryTheory.Limits.PreservesLimitsOfShape`	—	`isZero` `isZero_iff`
`preservesLimitsOfSize_of_isZero` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.Functor` `category`	`CategoryTheory.Limits.PreservesLimitsOfSize`	—	`preservesLimitsOfShape_of_isZero`
`preservesTerminalObject_of_preservesZeroMorphisms` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `empty`	—	`CategoryTheory.Limits.preservesTerminal_of_iso` `CategoryTheory.Limits.HasZeroObject.hasTerminal`
`preservesZeroMorphisms_comp` 📖	mathematical	—	`PreservesZeroMorphisms` `comp`	—	`map_zero`
`preservesZeroMorphisms_evaluation_obj` 📖	mathematical	—	`PreservesZeroMorphisms` `CategoryTheory.Functor` `category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `obj` `CategoryTheory.evaluation`	—	—
`preservesZeroMorphisms_of_full` 📖	mathematical	—	`PreservesZeroMorphisms`	—	`CategoryTheory.Limits.zero_comp` `map_comp` `map_preimage` `CategoryTheory.Limits.comp_zero`
`preservesZeroMorphisms_of_isLeftAdjoint` 📖	mathematical	—	`PreservesZeroMorphisms`	—	`CategoryTheory.Adjunction.left_triangle_components` `CategoryTheory.Category.comp_id` `map_comp` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Adjunction.counit_naturality` `CategoryTheory.Limits.comp_zero`
`preservesZeroMorphisms_of_isRightAdjoint` 📖	mathematical	—	`PreservesZeroMorphisms`	—	`CategoryTheory.Adjunction.right_triangle_components_assoc` `map_comp` `CategoryTheory.Limits.comp_zero` `CategoryTheory.Adjunction.unit_naturality_assoc` `CategoryTheory.Limits.zero_comp`
`preservesZeroMorphisms_of_iso` 📖	mathematical	—	`PreservesZeroMorphisms`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.NatTrans.naturality` `map_zero` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`
`preservesZeroMorphisms_of_map_zero_object` 📖	mathematical	—	`PreservesZeroMorphisms`	—	`map_comp` `CategoryTheory.Limits.comp_zero` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.zero_of_to_zero` `CategoryTheory.Limits.zero_comp`
`preservesZeroMorphisms_of_preserves_initial_object` 📖	mathematical	—	`PreservesZeroMorphisms`	—	`preservesZeroMorphisms_of_map_zero_object` `CategoryTheory.Limits.HasZeroObject.hasInitial`
`preservesZeroMorphisms_of_preserves_terminal_object` 📖	mathematical	—	`PreservesZeroMorphisms`	—	`preservesZeroMorphisms_of_map_zero_object` `CategoryTheory.Limits.HasZeroObject.hasTerminal`
`whiskerRight_zero` 📖	mathematical	—	`whiskerRight` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `category` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `comp`	—	`CategoryTheory.NatTrans.ext'` `map_zero`
`zero_of_map_zero` 📖	—	`map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	—	`map_injective` `map_zero`

CategoryTheory.Functor.PreservesZeroMorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_zero` 📖	mathematical	—	`CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index