HomologicalComplexLimitsEventuallyConstant

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

Statistics

Metric	Count
Definitions	0
Theorems isIso_π_f_of_isLimit_of_isEventuallyConstantTo, quasiIsoAt_π_of_isLimit_of_isEventuallyConstantTo	2
Total	2

HomologicalComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_π_f_of_isLimit_of_isEventuallyConstantTo 📖	mathematical	CategoryTheory.Limits.HasLimit CategoryTheory.Functor.comp HomologicalComplex instCategory eval CategoryTheory.Functor.IsEventuallyConstantTo	CategoryTheory.IsIso X CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt Hom.f CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit instPreservesLimitEval
quasiIsoAt_π_of_isLimit_of_isEventuallyConstantTo 📖	mathematical	CategoryTheory.Limits.HasLimit CategoryTheory.Functor.comp HomologicalComplex instCategory eval ComplexShape.prev ComplexShape.next CategoryTheory.Functor.IsEventuallyConstantTo	QuasiIsoAt CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.CategoryWithHomology.hasHomology sc	—	CategoryTheory.CategoryWithHomology.hasHomology quasiIsoAt_iff' isIso_π_f_of_isLimit_of_isEventuallyConstantTo CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso

---

← Back to Index