[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) → i = 0
[PROOFSTEP]
rintro ⟨_, h₂⟩
[GOAL]
case mp.intro
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
⊢ i = 0
[PROOFSTEP]
by_contra h
[GOAL]
case mp.intro
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
h : ¬i = 0
⊢ False
[PROOFSTEP]
exact h₂ (Fin.succAbove_ne_zero_zero h)
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)
[PROOFSTEP]
exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ ↑(Hom.toOrderHom (SimplexCategory.δ 0)) 0 ≠ 0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.1159, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ ¬↑(Hom.toOrderHom (SimplexCategory.δ 0)) 0 = 0
[PROOFSTEP]
exact Fin.succ_ne_zero (0 : Fin (j + 1))
[GOAL]
C : Type u_1
inst✝² : Category.{?u.2609, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
i : [n] ⟶ [n + 1]
inst✝ : Mono i
hi : Isδ₀ i
⊢ i = SimplexCategory.δ 0
[PROOFSTEP]
obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono i
[GOAL]
case intro
C : Type u_1
inst✝² : Category.{?u.2609, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : Isδ₀ (SimplexCategory.δ j)
⊢ SimplexCategory.δ j = SimplexCategory.δ 0
[PROOFSTEP]
rw [iff] at hi 
[GOAL]
case intro
C : Type u_1
inst✝² : Category.{?u.2609, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0
[PROOFSTEP]
rw [hi]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Δ = Δ'
[GOAL]
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Δ = Δ'
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
exact eqToHom (by congr)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ')
[PROOFSTEP]
congr
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : ¬Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Isδ₀ i
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h : ¬Δ = Δ'
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
by_cases Isδ₀ i
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
h : Isδ₀ i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
exact K.d Δ.len Δ'.len
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.36495, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
h : ¬Isδ₀ i
⊢ HomologicalComplex.X K (len Δ) ⟶ HomologicalComplex.X K (len Δ')
[PROOFSTEP]
exact 0
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
⊢ mapMono K (𝟙 Δ) = 𝟙 (HomologicalComplex.X K (len Δ))
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
⊢ (if h : Δ = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ))
    else if h : Isδ₀ (𝟙 Δ) then HomologicalComplex.d K (len Δ) (len Δ) else 0) =
    𝟙 (HomologicalComplex.X K (len Δ))
[PROOFSTEP]
simp only [eq_self_iff_true, eqToHom_refl, dite_eq_ite, if_true]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ mapMono K i = HomologicalComplex.d K (len Δ) (len Δ')
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    HomologicalComplex.d K (len Δ) (len Δ')
[PROOFSTEP]
suffices Δ ≠ Δ' by simp only [dif_neg this, dif_pos hi]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
this : Δ ≠ Δ'
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    HomologicalComplex.d K (len Δ) (len Δ')
[PROOFSTEP]
simp only [dif_neg this, dif_pos hi]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ Δ ≠ Δ'
[PROOFSTEP]
rintro rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i : Δ ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ False
[PROOFSTEP]
simpa only [self_eq_add_right, Nat.one_ne_zero] using hi.1
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
n : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)
[PROOFSTEP]
rw [Isδ₀.iff]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ mapMono K i = 0
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    0
[PROOFSTEP]
rw [Ne.def] at h₁ 
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ'))
    else if h : Isδ₀ i then HomologicalComplex.d K (len Δ) (len Δ') else 0) =
    0
[PROOFSTEP]
split_ifs
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ mapMono K i ≫ HomologicalComplex.Hom.f f (len Δ) = HomologicalComplex.Hom.f f (len Δ') ≫ mapMono K' i
[PROOFSTEP]
unfold mapMono
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ (if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K (len Δ') (len Δ) else 0) ≫
      HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K' (len Δ') (len Δ) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ)) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ')) ≫
      HomologicalComplex.Hom.f f (len Δ') =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ'))
[PROOFSTEP]
simp only [id_comp, eqToHom_refl, comp_id]
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ HomologicalComplex.d K (len Δ') (len Δ) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫ HomologicalComplex.d K' (len Δ') (len Δ)
[PROOFSTEP]
rw [HomologicalComplex.Hom.comm]
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ HomologicalComplex.Hom.f f (len Δ) = HomologicalComplex.Hom.f f (len Δ') ≫ 0
[PROOFSTEP]
rw [zero_comp, comp_zero]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
by_cases h₁ : Δ = Δ'
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
subst h₁
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ
i : Δ ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
simp only [SimplexCategory.eq_id_of_mono i, comp_id, id_comp, mapMono_id K, eqToHom_refl]
  -- case where i' : Δ'' ⟶ Δ' is the identity
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
by_cases h₂ : Δ' = Δ''
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
subst h₂
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝¹ : Mono i
h₁ : ¬Δ = Δ'
i' : Δ' ⟶ Δ'
inst✝ : Mono i'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
simp only [SimplexCategory.eq_id_of_mono i', comp_id, id_comp, mapMono_id K, eqToHom_refl]
  -- then the RHS is always zero
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i h₁)
[GOAL]
case neg.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
obtain ⟨k', hk'⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i' h₂)
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
have eq : Δ.len = Δ''.len + (k + k' + 2) := by linarith
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
⊢ len Δ = len Δ'' + (k + k' + 2)
[PROOFSTEP]
linarith
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
[PROOFSTEP]
rw [mapMono_eq_zero K (i' ≫ i) _ _]
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)
[PROOFSTEP]
rotate_left
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Δ = Δ''
⊢ False
[PROOFSTEP]
simp only [self_eq_add_right, h, add_eq_zero_iff, and_false] at eq 
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Isδ₀ (i' ≫ i)
⊢ False
[PROOFSTEP]
simp only [h.1, add_right_inj] at eq 
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
h : Isδ₀ (i' ≫ i)
eq : 1 = k + k' + 2
⊢ False
[PROOFSTEP]
linarith
  -- in all cases, the LHS is also zero, either by definition, or because d ≫ d = 0
[GOAL]
case neg.intro.intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
by_cases h₃ : Isδ₀ i
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
by_cases h₄ : Isδ₀ i'
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : ¬Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
simp only [mapMono_eq_zero K i' h₂ h₄, comp_zero]
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : ¬Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
[PROOFSTEP]
simp only [mapMono_eq_zero K i h₁ h₃, zero_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
simp only [map, colimit.ι_desc, Cofan.mk_ι_app]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
have h := SimplexCategory.image_eq fac
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
h : image (θ.unop ≫ Splitting.IndexSet.e A) = Δ''
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (summand K Δ') (Splitting.IndexSet.pull A θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_i
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ image.ι (θ.unop ≫ Splitting.IndexSet.e A) = i
[PROOFSTEP]
exact SimplexCategory.image_ι_eq fac
[GOAL]
case e_a.h.e_6.h
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.pull A θ = Splitting.IndexSet.mk e
[PROOFSTEP]
dsimp only [SimplicialObject.Splitting.IndexSet.pull]
[GOAL]
case e_a.h.e_6.h
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ Splitting.IndexSet.e A)) = Splitting.IndexSet.mk e
[PROOFSTEP]
congr
[GOAL]
case e_a.h.e_6.h.e_f
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : Δ'.unop ⟶ image (θ.unop ≫ Splitting.IndexSet.e A)
i : image (θ.unop ≫ Splitting.IndexSet.e A) ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ factorThruImage (θ.unop ≫ Splitting.IndexSet.e A) = e
[PROOFSTEP]
exact SimplexCategory.factorThruImage_eq fac
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫
      𝟙 ({ obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.obj Δ)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
[PROOFSTEP]
have fac : A.e ≫ 𝟙 A.1.unop = (𝟙 Δ).unop ≫ A.e := by rw [unop_id, comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (𝟙 Δ).unop ≫ Splitting.IndexSet.e A
[PROOFSTEP]
rw [unop_id, comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (𝟙 Δ).unop ≫ Splitting.IndexSet.e A
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A } ≫ 𝟙 (Obj.obj₂ K Δ)
[PROOFSTEP]
erw [Obj.map_on_summand₀ K A fac, Obj.Termwise.mapMono_id, id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac : Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (𝟙 Δ).unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk (Splitting.IndexSet.e A)) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ A) { as := A }
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫
        { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
[PROOFSTEP]
have fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e := by rw [unop_comp, assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ θ.unop ≫ θ'.unop ≫ Splitting.IndexSet.e A = (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
[PROOFSTEP]
rw [unop_comp, assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : θ.unop ≫ θ'.unop ≫ Splitting.IndexSet.e A = (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫
        { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
[PROOFSTEP]
rw [← image.fac (θ'.unop ≫ A.e), ← assoc, ← image.fac (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)), assoc] at fac 
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
        image.ι (θ'.unop ≫ Splitting.IndexSet.e A) =
    (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
⊢ colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map (θ' ≫ θ) =
    colimit.ι (Discrete.functor fun A => Obj.summand K Δ'' A) { as := A } ≫
      { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ' ≫
        { obj := fun Δ => Obj.obj₂ K Δ, map := fun {X Y} θ => Obj.map K θ }.map θ
[PROOFSTEP]
simp only [Obj.map_on_summand₀'_assoc K A θ', Obj.map_on_summand₀' K _ θ, Obj.Termwise.mapMono_comp_assoc,
  Obj.map_on_summand₀ K A fac]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.105445, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x✝ : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
        image.ι (θ'.unop ≫ Splitting.IndexSet.e A) =
    (θ' ≫ θ).unop ≫ Splitting.IndexSet.e A
⊢ Obj.Termwise.mapMono K
        (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
          image.ι (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (Obj.summand K Δ)
        (Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ Splitting.IndexSet.e A)))) =
    Obj.Termwise.mapMono K
        (image.ι (θ.unop ≫ Splitting.IndexSet.e (Splitting.IndexSet.pull A θ')) ≫
          image.ι (θ'.unop ≫ Splitting.IndexSet.e A)) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.pull (Splitting.IndexSet.pull A θ') θ)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) Δ =
    colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ)
[PROOFSTEP]
induction' Δ using Opposite.rec' with Δ
[GOAL]
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝¹ : Discrete (Splitting.IndexSet Δ✝)
A✝ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝ : Discrete (Splitting.IndexSet (op Δ))
A : Splitting.IndexSet (op Δ)
⊢ colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op Δ)))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) (op Δ) =
    colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op Δ)))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op Δ))
[PROOFSTEP]
induction' Δ using SimplexCategory.rec with n
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ colimit.ι
        (Discrete.functor
          (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n])))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) (op [n]) =
    colimit.ι
        (Discrete.functor
          (Splitting.summand (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n])))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n]))
[PROOFSTEP]
dsimp [Splitting.map]
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ (colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      Sigma.desc fun A =>
        Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n]))
[PROOFSTEP]
simp only [colimit.ι_desc, Cofan.mk_ι_app, Γ₀.obj_map]
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) (op [n]))
[PROOFSTEP]
erw [Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1) (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl),
  Γ₀.Obj.Termwise.mapMono_id, A.ext', id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (Splitting.IndexSet.e A).op.unop ≫ 𝟙 (op A.fst.unop).unop
[PROOFSTEP]
rfl
[GOAL]
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet (op Δ))
A✝ : Splitting.IndexSet (op Δ)
n : ℕ
x✝ : Discrete (Splitting.IndexSet (op [n]))
A : Splitting.IndexSet (op [n])
⊢ Sigma.ι (Obj.summand K (op [n]))
      (Splitting.IndexSet.mk
        (Splitting.IndexSet.e
          { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } })) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst))
      { as := { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } } }
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{?u.135855, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
⊢ IsIso (Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K (op [n])) (Splitting.IndexSet.id (op [n]))) Δ)
[PROOFSTEP]
rw [Γ₀.splitting_map_eq_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.135855, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
Δ : SimplexCategoryᵒᵖ
⊢ IsIso (𝟙 (Splitting.coprod (fun n => Obj.summand K (op [n]) (Splitting.IndexSet.id (op [n]))) Δ))
[PROOFSTEP]
apply IsIso.id
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.ιSummand (splitting K) A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ Splitting.ιSummand (splitting K) (Splitting.IndexSet.mk e)
[PROOFSTEP]
dsimp only [SimplicialObject.Splitting.ιSummand, SimplicialObject.Splitting.ιCoprod]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ (Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (Splitting.iso (splitting K) Δ).hom) ≫ (obj K).map θ =
    Termwise.mapMono K i ≫
      Sigma.ι (Splitting.summand (splitting K).N (op Δ'.unop)) (Splitting.IndexSet.mk e) ≫
        (Splitting.iso (splitting K) (op Δ'.unop)).hom
[PROOFSTEP]
simp only [assoc, Γ₀.splitting_iso_hom_eq_id, id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ Sigma.ι (Splitting.summand (splitting K).N (op Δ'.unop)) (Splitting.IndexSet.mk e)
[PROOFSTEP]
exact Γ₀.Obj.map_on_summand₀ K A fac
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ Splitting.ιSummand (splitting K) A ≫ (obj K).map θ =
    Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      Splitting.ιSummand (splitting K) (Splitting.IndexSet.pull A θ)
[PROOFSTEP]
apply Obj.map_on_summand
[GOAL]
case fac
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ factorThruImage (θ.unop ≫ Splitting.IndexSet.e A) ≫ image.ι (θ.unop ≫ Splitting.IndexSet.e A) =
    θ.unop ≫ Splitting.IndexSet.e A
[PROOFSTEP]
apply image.fac
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝¹ : HasFiniteCoproducts C
Δ Δ' : SimplexCategory
e : Δ' ⟶ Δ
inst✝ : Epi e
⊢ Splitting.ιSummand (splitting K) (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map e.op =
    Splitting.ιSummand (splitting K) (Splitting.IndexSet.mk e)
[PROOFSTEP]
simpa only [Γ₀.Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) e.op (rfl : e ≫ 𝟙 Δ = e ≫ 𝟙 Δ),
  Γ₀.Obj.Termwise.mapMono_id] using id_comp _
[GOAL]
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
⊢ (obj K).map θ ≫
      (fun Δ =>
          Splitting.desc (splitting K) Δ fun A =>
            HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
        Δ =
    (fun Δ =>
          Splitting.desc (splitting K) Δ fun A =>
            HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
        Δ' ≫
      (obj K').map θ
[PROOFSTEP]
apply (Γ₀.splitting K).hom_ext'
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
⊢ ∀ (A : Splitting.IndexSet Δ'),
    Splitting.ιSummand (splitting K) A ≫
        (obj K).map θ ≫
          (fun Δ =>
              Splitting.desc (splitting K) Δ fun A =>
                HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
            Δ =
      Splitting.ιSummand (splitting K) A ≫
        (fun Δ =>
              Splitting.desc (splitting K) Δ fun A =>
                HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
            Δ' ≫
          (obj K').map θ
[PROOFSTEP]
intro A
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ Splitting.ιSummand (splitting K) A ≫
      (obj K).map θ ≫
        (fun Δ =>
            Splitting.desc (splitting K) Δ fun A =>
              HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
          Δ =
    Splitting.ιSummand (splitting K) A ≫
      (fun Δ =>
            Splitting.desc (splitting K) Δ fun A =>
              HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (splitting K') A)
          Δ' ≫
        (obj K').map θ
[PROOFSTEP]
simp only [(splitting K).ι_desc_assoc, Obj.map_on_summand'_assoc K _ θ, (splitting K).ι_desc, assoc,
  Obj.map_on_summand' K' _ θ]
[GOAL]
case h
C : Type u_1
inst✝² : Category.{?u.164164, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ Obj.Termwise.mapMono K (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
      HomologicalComplex.Hom.f f (len (Splitting.IndexSet.pull A θ).fst.unop) ≫
        Splitting.ιSummand (splitting K') (Splitting.IndexSet.pull A θ) =
    HomologicalComplex.Hom.f f (len A.fst.unop) ≫
      Obj.Termwise.mapMono K' (image.ι (θ.unop ≫ Splitting.IndexSet.e A)) ≫
        Splitting.ιSummand (splitting K') (Splitting.IndexSet.pull A θ)
[PROOFSTEP]
apply Obj.Termwise.mapMono_naturality_assoc
[GOAL]
C : Type u_1
inst✝² : Category.{?u.167032, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ Splitting.ι ((fun K => Split.mk' (Γ₀.splitting K)) K).s n ≫ NatTrans.app (Γ₀.map f) (op [n]) =
    HomologicalComplex.Hom.f f n ≫ Splitting.ι ((fun K => Split.mk' (Γ₀.splitting K)) K').s n
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.167032, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ (Splitting.ι (Γ₀.splitting K) n ≫
      Splitting.desc (Γ₀.splitting K) (op [n]) fun A =>
        HomologicalComplex.Hom.f f (len A.fst.unop) ≫ Splitting.ιSummand (Γ₀.splitting K') A) =
    HomologicalComplex.Hom.f f n ≫ Splitting.ι (Γ₀.splitting K') n
[PROOFSTEP]
simp only [← Splitting.ιSummand_id, (Γ₀.splitting K).ι_desc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.167032, u_1} C
inst✝¹ : Preadditive C
K✝ K'✝ : ChainComplex C ℕ
f✝ : K✝ ⟶ K'✝
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K K' : ChainComplex C ℕ
f : K ⟶ K'
n : ℕ
⊢ HomologicalComplex.Hom.f f (len (Splitting.IndexSet.id (op [n])).fst.unop) ≫
      Splitting.ιSummand (Γ₀.splitting K') (Splitting.IndexSet.id (op [n])) =
    HomologicalComplex.Hom.f f n ≫ Splitting.ιSummand (Γ₀.splitting K') (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HigherFacesVanish (n + 1) (Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])))
[PROOFSTEP]
intro j _
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
[PROOFSTEP]
have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
[PROOFSTEP]
rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq 
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ [n + 1] ≠ [n]
case h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))
[PROOFSTEP]
rotate_left
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ [n + 1] ≠ [n]
[PROOFSTEP]
intro h
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
h : [n + 1] = [n]
⊢ False
[PROOFSTEP]
exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)
[GOAL]
case h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
⊢ ¬Isδ₀ (SimplexCategory.δ (Fin.succ j))
[PROOFSTEP]
exact fun h => Fin.succ_ne_zero j (by simpa only [Isδ₀.iff] using h)
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ (Fin.succ j)) ≫
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
h : Isδ₀ (SimplexCategory.δ (Fin.succ j))
⊢ Fin.succ j = 0
[PROOFSTEP]
simpa only [Isδ₀.iff] using h
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      (Γ₀.obj K).map (SimplexCategory.δ (Fin.succ j)).op =
    0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      SimplicialObject.δ (Γ₀.obj K) (Fin.succ j) =
    0
[PROOFSTEP]
exact eq
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) ≫ HomologicalComplex.Hom.f PInfty n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rw [PInfty_f]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) ≫ HomologicalComplex.Hom.f (P n) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.zero])) ≫
      HomologicalComplex.Hom.f (P Nat.zero) Nat.zero =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.zero]))
[PROOFSTEP]
simpa only [P_f_0_eq] using comp_id _
[GOAL]
case succ
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.succ n])) ≫
      HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [Nat.succ n]))
[PROOFSTEP]
exact (HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self
