Theorems · Theorem · category theory
CategoryTheory.Abelian.Ext.comp_assoc
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
[inst_2 : CategoryTheory.HasExt C] {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ} (α : CategoryTheory.Abelian.Ext X Y a₁)
(β : CategoryTheory.Abelian.Ext Y Z a₂) (γ : CategoryTheory.Abelian.Ext Z T a₃) (h₁₂ : a₁ + a₂ = a₁₂)
(h₂₃ : a₂ + a₃ = a₂₃) (h : a₁ + a₂ + a₃ = a), (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯- Cited by
- 5 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- CategoryTheory.Abelianstatement and proof · cited by 1,753
- ComplexShape.upproof · cited by 1,123
- CategoryTheory.HasExtstatement and proof · cited by 218
- CategoryTheory.Abelian.Extstatement and proof · cited by 191
- CategoryTheory.Abelian.Ext.compstatement · cited by 80
- HomologicalComplex.quasiIsoproof · cited by 42
- CategoryTheory.Localization.SmallShiftedHom.comp_assocproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assocproof · cited by 3
- CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zeroproof · cited by 3
- CategoryTheory.Abelian.Ext.comp_assoc_of_third_deg_zeroproof · cited by 0
- CategoryTheory.ShortComplex.ShortExact.extClass_comp_assocproof · cited by 0
- CategoryTheory.ShortComplex.ShortExact.comp_extClass_assocproof · cited by 0