Theorems · Definition · category theory
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.Preadditive C] →
{ι : Type u_2} →
{c : ComplexShape ι} →
CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) ≅
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.comp
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverseThe unit isomorphism of the equivalence
Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Functor.compstatement · cited by 6,529
- CategoryTheory.Isostatement · cited by 3,963
- CategoryTheory.Functor.idstatement · cited by 3,333
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- HomologicalComplexstatement and proof · cited by 1,691
- ComplexShapestatement and proof · cited by 1,684
- HomologicalComplex.Hom.fproof · cited by 845
- ComplexShape.Relproof · cited by 518
- CategoryTheory.Idempotents.Karoubistatement and proof · cited by 233
Cited by4
Results whose statement or proof uses this declaration.
- CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalenceproof · cited by 4
- CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_fstatement and proof · cited by 0
- CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIsostatement · cited by 0
- CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_fstatement and proof · cited by 0