LeftExact

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

Statistics

Metric	Count
Definitions isColimitMapCoconeBinaryCofanOfPreservesCokernels, isLimitMapConeBinaryFanOfPreservesKernels	2
Theorems preservesBinaryCoproducts_of_preservesCokernels, preservesBinaryProduct_of_preservesKernels, preservesBinaryProducts_of_preservesKernels, preservesCoequalizer_of_preservesCokernels, preservesCoequalizers_of_preservesCokernels, preservesCoproduct_of_preservesCokernels, preservesEqualizer_of_preservesKernels, preservesEqualizers_of_preservesKernels, preservesFiniteColimits_of_preservesCokernels, preservesFiniteLimits_of_preservesKernels	10
Total	12

CategoryTheory.Functor

Definitions

Name	Category	Theorems
isColimitMapCoconeBinaryCofanOfPreservesCokernels 📖	CompOp	—
isLimitMapConeBinaryFanOfPreservesKernels 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesBinaryCoproducts_of_preservesCokernels 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory	—	CategoryTheory.Limits.preservesColimit_of_iso_diagram preservesCoproduct_of_preservesCokernels
preservesBinaryProduct_of_preservesKernels 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	—
preservesBinaryProducts_of_preservesKernels 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory	—	CategoryTheory.Limits.preservesLimit_of_iso_diagram preservesBinaryProduct_of_preservesKernels
preservesCoequalizer_of_preservesCokernels 📖	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—	CategoryTheory.Limits.Cofork.condition map_sub additive_of_preservesBinaryBiproducts CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts preservesBinaryCoproducts_of_preservesCokernels CategoryTheory.Category.comp_id CategoryTheory.Preadditive.comp_sub CategoryTheory.Category.id_comp CategoryTheory.Limits.comp_zero
preservesCoequalizers_of_preservesCokernels 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Limits.PreservesColimitsOfShape	—	CategoryTheory.Limits.preservesColimit_of_iso_diagram preservesCoequalizer_of_preservesCokernels
preservesCoproduct_of_preservesCokernels 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	—
preservesEqualizer_of_preservesKernels 📖	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—	CategoryTheory.Limits.Fork.condition map_sub additive_of_preservesBinaryBiproducts CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts preservesBinaryProducts_of_preservesKernels CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
preservesEqualizers_of_preservesKernels 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Limits.PreservesLimitsOfShape	—	CategoryTheory.Limits.preservesLimit_of_iso_diagram preservesEqualizer_of_preservesKernels
preservesFiniteColimits_of_preservesCokernels 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Limits.PreservesFiniteColimits	—	CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts preservesCoequalizers_of_preservesCokernels CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial preservesBinaryCoproducts_of_preservesCokernels CategoryTheory.Limits.preservesColimitsOfShape_pempty_of_preservesInitial preservesInitialObject_of_preservesZeroMorphisms Finite.of_fintype
preservesFiniteLimits_of_preservesKernels 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	CategoryTheory.Limits.PreservesFiniteLimits	—	preservesEqualizers_of_preservesKernels preservesTerminalObject_of_preservesZeroMorphisms CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal preservesBinaryProducts_of_preservesKernels CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts

---

← Back to Index