Complementary embeddings

Given two embeddings e₁ : c₁.Embedding c and e₂ : c₂.Embedding c of complex shapes, we introduce a property e₁.AreComplementary e₂ saying that the image subsets of the indices of c₁ and c₂ form a partition of the indices of c.

If e₁.IsTruncLE and e₂.IsTruncGE, and K : HomologicalComplex C c, we construct a quasi-isomorphism shortComplexTruncLEX₃ToTruncGE between the cokernel of K.ιTruncLE e₁ : K.truncLE e₁ ⟶ K and K.truncGE e₂.

structure ComplexShape.Embedding.AreComplementary {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} (e₁ : c₁.Embedding c) (e₂ : c₂.Embedding c) : Prop

Two embedding e₁ and e₂ into a complex shape c : ComplexShape ι are complementary when the range of e₁.f and e₂.f form a partition of ι.

• disjoint (i₁ : ι₁) (i₂ : ι₂) : e₁.f i₁ ≠ e₂.f i₂
• union (i : ι) : (∃ (i₁ : ι₁), e₁.f i₁ = i) ∨ ∃ (i₂ : ι₂), e₂.f i₂ = i

theorem ComplexShape.Embedding.AreComplementary.symm {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) : e₂.AreComplementary e₁

theorem ComplexShape.Embedding.AreComplementary.exists_i₁ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (i : ι) (hi : ∀ (i₂ : ι₂), e₂.f i₂ ≠ i) : ∃ (i₁ : ι₁), i = e₁.f i₁

theorem ComplexShape.Embedding.AreComplementary.exists_i₂ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (i : ι) (hi : ∀ (i₁ : ι₁), e₁.f i₁ ≠ i) : ∃ (i₂ : ι₂), i = e₂.f i₂

def ComplexShape.Embedding.AreComplementary.fromSum {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} (e₁ : c₁.Embedding c) (e₂ : c₂.Embedding c) : ι₁ ⊕ ι₂ → ι

Given complementary embeddings of complex shapes e₁ : Embedding c₁ c and e₂ : Embedding c₂ c, this is the obvious map ι₁ ⊕ ι₂ → ι from the sum of the index types of c₁ and c₂ to the index type of c.

Equations

• ComplexShape.Embedding.AreComplementary.fromSum e₁ e₂ (Sum.inl i₁) = e₁.f i₁
• ComplexShape.Embedding.AreComplementary.fromSum e₁ e₂ (Sum.inr i₂) = e₂.f i₂

theorem ComplexShape.Embedding.AreComplementary.fromSum_bijective {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) : Function.Bijective (fromSum e₁ e₂)

noncomputable def ComplexShape.Embedding.AreComplementary.equiv {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) : ι₁ ⊕ ι₂ ≃ ι

Given complementary embeddings of complex shapes e₁ : Embedding c₁ c and e₂ : Embedding c₂ c, this is the obvious bijection ι₁ ⊕ ι₂ ≃ ι from the sum of the index types of c₁ and c₂ to the index type of c.

Equations

• ac.equiv = Equiv.ofBijective (ComplexShape.Embedding.AreComplementary.fromSum e₁ e₂) ⋯

@[simp]

theorem ComplexShape.Embedding.AreComplementary.equiv_inl {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (i₁ : ι₁) : ac.equiv (Sum.inl i₁) = e₁.f i₁

@[simp]

theorem ComplexShape.Embedding.AreComplementary.equiv_inr {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (i₂ : ι₂) : ac.equiv (Sum.inr i₂) = e₂.f i₂

def ComplexShape.Embedding.AreComplementary.desc.aux {ι : Type u_1} (X : ι → Type u_5) (i j : ι) (hij : i = j) : X i ≃ X j

Auxiliary definition for desc.

Equations

• ComplexShape.Embedding.AreComplementary.desc.aux X i j hij = hij ▸ Equiv.refl (X i)

@[simp]

theorem ComplexShape.Embedding.AreComplementary.desc.aux_trans {ι : Type u_1} {X : ι → Type u_5} {i j k : ι} (hij : i = j) (hjk : j = k) (x : X i) : (aux X j k hjk) ((aux X i j hij) x) = (aux X i k ⋯) x

def ComplexShape.Embedding.AreComplementary.desc' {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5} (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i : ι₁ ⊕ ι₂) : X (ac.equiv i)

Auxiliary definition for desc.

Equations

• ac.desc' x₁ x₂ (Sum.inl i₁) = x₁ i₁
• ac.desc' x₁ x₂ (Sum.inr i₂) = x₂ i₂

theorem ComplexShape.Embedding.AreComplementary.desc'_inl {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5} (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i : ι₁ ⊕ ι₂) (i₁ : ι₁) (h : Sum.inl i₁ = i) : ac.desc' x₁ x₂ i = (desc.aux X (e₁.f i₁) (ac.equiv i) ⋯) (x₁ i₁)

theorem ComplexShape.Embedding.AreComplementary.desc'_inr {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5} (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i : ι₁ ⊕ ι₂) (i₂ : ι₂) (h : Sum.inr i₂ = i) : ac.desc' x₁ x₂ i = (desc.aux X (e₂.f i₂) (ac.equiv i) ⋯) (x₂ i₂)

noncomputable def ComplexShape.Embedding.AreComplementary.desc {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5} (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i : ι) : X i

If ι₁ and ι₂ are the index types of complementary embeddings into a complex shape of index type ι, this is a constructor for (dependent) maps from ι, which takes as inputs the "restrictions" to ι₁ and ι₂.

Equations

• ac.desc x₁ x₂ i = (ComplexShape.Embedding.AreComplementary.desc.aux X (ac.equiv (ac.equiv.symm i)) i ⋯) (ac.desc' x₁ x₂ (ac.equiv.symm i))

theorem ComplexShape.Embedding.AreComplementary.desc_inl {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5} (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i₁ : ι₁) : ac.desc x₁ x₂ (e₁.f i₁) = x₁ i₁

theorem ComplexShape.Embedding.AreComplementary.desc_inr {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5} (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i₂ : ι₂) : ac.desc x₁ x₂ (e₂.f i₂) = x₂ i₂

theorem ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₁_iff {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (K : HomologicalComplex C c) : K.IsStrictlySupportedOutside e₁ ↔ K.IsStrictlySupported e₂

theorem ComplexShape.Embedding.AreComplementary.isStrictlySupportedOutside₂_iff {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (K : HomologicalComplex C c) : K.IsStrictlySupportedOutside e₂ ↔ K.IsStrictlySupported e₁

theorem ComplexShape.Embedding.AreComplementary.isSupportedOutside₁_iff {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (K : HomologicalComplex C c) : K.IsSupportedOutside e₁ ↔ K.IsSupported e₂

theorem ComplexShape.Embedding.AreComplementary.isSupportedOutside₂_iff {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) (K : HomologicalComplex C c) : K.IsSupportedOutside e₂ ↔ K.IsSupported e₁

theorem ComplexShape.Embedding.AreComplementary.hom_ext' {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {K L : HomologicalComplex C c} (φ : K ⟶ L) (hK : K.IsStrictlySupportedOutside e₂) (hL : L.IsStrictlySupportedOutside e₁) : φ = 0

Variant of hom_ext.

theorem ComplexShape.Embedding.AreComplementary.hom_ext {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Limits.HasZeroMorphisms C] {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {K L : HomologicalComplex C c} [K.IsStrictlySupported e₁] [L.IsStrictlySupported e₂] (φ : K ⟶ L) : φ = 0

def ComplexShape.Embedding.AreComplementary.Boundary {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} : e₁.AreComplementary e₂ → (i₁ : ι₁) → (i₂ : ι₂) → Prop

If e₁ and e₂ are complementary embeddings into a complex shape c, indices i₁ and i₂ are at the boundary if c.Rel (e₁.f i₁) (e₂.f i₂).

Equations

• x✝.Boundary i₁ i₂ = c.Rel (e₁.f i₁) (e₂.f i₂)

theorem ComplexShape.Embedding.AreComplementary.Boundary.fst {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ : ι₁} {i₂ : ι₂} (h : ac.Boundary i₁ i₂) : e₁.BoundaryLE i₁

theorem ComplexShape.Embedding.AreComplementary.Boundary.snd {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ : ι₁} {i₂ : ι₂} (h : ac.Boundary i₁ i₂) : e₂.BoundaryGE i₂

theorem ComplexShape.Embedding.AreComplementary.Boundary.fst_inj {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ i₁' : ι₁} {i₂ : ι₂} (h : ac.Boundary i₁ i₂) (h' : ac.Boundary i₁' i₂) : i₁ = i₁'

theorem ComplexShape.Embedding.AreComplementary.Boundary.snd_inj {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ : ι₁} {i₂ i₂' : ι₂} (h : ac.Boundary i₁ i₂) (h' : ac.Boundary i₁ i₂') : i₂ = i₂'

theorem ComplexShape.Embedding.AreComplementary.Boundary.exists₁ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₁ : ι₁} (h : e₁.BoundaryLE i₁) : ∃ (i₂ : ι₂), ac.Boundary i₁ i₂

theorem ComplexShape.Embedding.AreComplementary.Boundary.exists₂ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₂ : ι₂} (h : e₂.BoundaryGE i₂) : ∃ (i₁ : ι₁), ac.Boundary i₁ i₂

noncomputable def ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLE {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₁ : ι₁} (h : e₁.BoundaryLE i₁) : ι₂

If ac : AreComplementary e₁ e₂ (with e₁ : ComplexShape.Embedding c₁ c and e₂ : ComplexShape.Embedding c₂ c), and i₁ belongs to e₁.BoundaryLE, then this is the (unique) index i₂ of c₂ such that ac.Boundary i₁ i₂.

Equations

• ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLE ac h = ⋯.choose

theorem ComplexShape.Embedding.AreComplementary.Boundary.of_boundaryLE {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₁ : ι₁} (h : e₁.BoundaryLE i₁) : ac.Boundary i₁ (indexOfBoundaryLE ac h)

noncomputable def ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGE {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₂ : ι₂} (h : e₂.BoundaryGE i₂) : ι₁

If ac : AreComplementary e₁ e₂ (with e₁ : ComplexShape.Embedding c₁ c and e₂ : ComplexShape.Embedding c₂ c), and i₂ belongs to e₂.BoundaryGE, then this is the (unique) index i₁ of c₁ such that ac.Boundary i₁ i₂.

Equations

• ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGE ac h = ⋯.choose

theorem ComplexShape.Embedding.AreComplementary.Boundary.of_boundaryGE {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₂ : ι₂} (h : e₂.BoundaryGE i₂) : ac.Boundary (indexOfBoundaryGE ac h) i₂

noncomputable def ComplexShape.Embedding.AreComplementary.Boundary.equiv {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) : Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE

The bijection Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE when e₁ and e₂ are complementary embeddings of complex shapes.

Equations

• One or more equations did not get rendered due to their size.

theorem ComplexShape.Embedding.embeddingUpInt_areComplementary (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (embeddingUpIntLE n₀).AreComplementary (embeddingUpIntGE n₁)

noncomputable def HomologicalComplex.shortComplexTruncLEX₃ToTruncGE {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [e₁.IsTruncLE] [e₂.IsTruncGE] (ac : e₁.AreComplementary e₂) : (K.shortComplexTruncLE e₁).X₃ ⟶ K.truncGE e₂

When e₁ and e₂ are complementary embeddings of complex shapes, with e₁.IsTruncLE and e₂.IsTruncGE, then this is the canonical quasi-isomorphism (K.shortComplexTruncLE e₁).X₃ ⟶ K.truncGE e₂ where (K.shortComplexTruncLE e₁).X₃ is the cokernel of K.ιTruncLE e₁ : K.truncLE e₁ ⟶ K.

Equations

• K.shortComplexTruncLEX₃ToTruncGE ac = CategoryTheory.Limits.cokernel.desc (K.ιTruncLE e₁) (K.πTruncGE e₂) ⋯

@[simp]

theorem HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [e₁.IsTruncLE] [e₂.IsTruncGE] (ac : e₁.AreComplementary e₂) : CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE e₁).g (K.shortComplexTruncLEX₃ToTruncGE ac) = K.πTruncGE e₂

@[simp]

theorem HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [e₁.IsTruncLE] [e₂.IsTruncGE] (ac : e₁.AreComplementary e₂) {Z : HomologicalComplex C c} (h : K.truncGE e₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE e₁).g (CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLEX₃ToTruncGE ac) h) = CategoryTheory.CategoryStruct.comp (K.πTruncGE e₂) h

instance HomologicalComplex.instQuasiIsoShortComplexTruncLEX₃ToTruncGE {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {C : Type u_4} [CategoryTheory.Category.{u_5, u_4} C] [CategoryTheory.Abelian C] (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [e₁.IsTruncLE] [e₂.IsTruncGE] (ac : e₁.AreComplementary e₂) : QuasiIso (K.shortComplexTruncLEX₃ToTruncGE ac)