HomologicalComplexAbelian

📁 Source: Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean

Statistics

Metric	Count
Definitions instAbelian	1
Theorems exact_iff_degreewise_exact, exact_of_degreewise_exact, instIsNormalEpiCategory, instIsNormalMonoCategory, shortExact_iff_degreewise_shortExact, shortExact_of_degreewise_shortExact	6
Total	7

HomologicalComplex

Definitions

Name	Category	Theorems
instAbelian 📖	CompOp	1 math math: isGrothendieckAbelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exact_iff_degreewise_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms CategoryTheory.ShortComplex.map eval instPreservesZeroMorphismsEval	—	instPreservesZeroMorphismsEval CategoryTheory.ShortComplex.Exact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsEvalOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits instPreservesFiniteColimitsEvalOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf exact_of_degreewise_exact
exact_of_degreewise_exact 📖	—	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map HomologicalComplex instCategory instHasZeroMorphisms eval instPreservesZeroMorphismsEval	—	—	instPreservesZeroMorphismsEval CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.IsZero.iff_id_eq_zero hom_ext CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.IsZero.of_iso CategoryTheory.ShortComplex.hasHomology_of_preserves CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsEvalOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits instPreservesFiniteColimitsEvalOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf
instIsNormalEpiCategory 📖	mathematical	—	CategoryTheory.IsNormalEpiCategory HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms	—	instHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Abelian.hasEqualizers CategoryTheory.Limits.kernel.condition instPreservesZeroMorphismsEval CategoryTheory.Functor.map_epi CategoryTheory.Functor.instPreservesEpimorphisms instHasZeroObject CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsEvalOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits instPreservesFiniteColimitsEvalOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits instPreservesLimitEval CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.hasKernels_of_hasEqualizers instHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit instPreservesLimitsOfShapeEvalOfHasLimitsOfShape
instIsNormalMonoCategory 📖	mathematical	—	CategoryTheory.IsNormalMonoCategory HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms	—	instHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Abelian.hasCoequalizers CategoryTheory.Limits.cokernel.condition instPreservesZeroMorphismsEval CategoryTheory.Functor.map_mono CategoryTheory.Functor.instPreservesMonomorphisms instHasZeroObject CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsEvalOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits instPreservesFiniteColimitsEvalOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits instPreservesColimitEval CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.hasCokernels_of_hasCoequalizers instHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeEvalOfHasColimitsOfShape
shortExact_iff_degreewise_shortExact 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms CategoryTheory.ShortComplex.map eval instPreservesZeroMorphismsEval	—	instPreservesZeroMorphismsEval CategoryTheory.ShortComplex.ShortExact.mono_f CategoryTheory.ShortComplex.ShortExact.epi_g CategoryTheory.ShortComplex.ShortExact.map CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact instPreservesFiniteLimitsEvalOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits instPreservesFiniteColimitsEvalOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.Functor.map_mono CategoryTheory.Functor.instPreservesMonomorphisms instHasZeroObject CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.map_epi CategoryTheory.Functor.instPreservesEpimorphisms shortExact_of_degreewise_shortExact
shortExact_of_degreewise_shortExact 📖	—	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.map HomologicalComplex instCategory instHasZeroMorphisms eval instPreservesZeroMorphismsEval	—	—	instPreservesZeroMorphismsEval exact_of_degreewise_exact CategoryTheory.ShortComplex.ShortExact.exact mono_of_mono_f CategoryTheory.ShortComplex.ShortExact.mono_f epi_of_epi_f CategoryTheory.ShortComplex.ShortExact.epi_g

---

← Back to Index