FullyFaithful

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/FullyFaithful.lean

Statistics

Metric	Count
Definitions singleFunctorCompHomologyFunctorIso	1
Theorems instFaithfulSingleFunctor, instFullSingleFunctor	2
Total	3

DerivedCategory

Definitions

Name	Category	Theorems
singleFunctorCompHomologyFunctorIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulSingleFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful DerivedCategory instCategory singleFunctor	—	CategoryTheory.NatIso.naturality_1
instFullSingleFunctor 📖	mathematical	—	CategoryTheory.Functor.Full DerivedCategory instCategory singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject right_fac_of_isStrictlyLE_of_isStrictlyGE CochainComplex.instIsStrictlyGEObjIntSingleFunctor CochainComplex.instIsStrictlyLEObjIntSingleFunctor CochainComplex.exists_iso_single CategoryTheory.Functor.map_surjective CochainComplex.instFullIntSingleFunctor CategoryTheory.Functor.map_comp CategoryTheory.IsIso.comp_isIso instIsIsoMapCochainComplexIntQ quasiIso_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.NatIso.isIso_map_iff CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.of_isIso_comp_left CategoryTheory.Functor.map_inv

---

← Back to Index