English
If the index pair Δ ≠ Δ′ and i is not δ₀, then the map on the summand vanishes: mapMono K i = 0.
Русский
Если Δ ≠ Δ′ и i не δ₀, то отображение на сумманду равно нулю: mapMono K i = 0.
LaTeX
$$mapMono(K,i) = 0, whenever Δ ≠ Δ′ and not Isδ₀(i).$$
Lean4
@[reassoc (attr := simp)]
theorem mapMono_comp (i' : Δ'' ⟶ Δ') (i : Δ' ⟶ Δ) [Mono i'] [Mono i] :
mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i) := by
-- case where i : Δ' ⟶ Δ is the identity
by_cases h₁ : Δ = Δ'
· subst h₁
simp only [SimplexCategory.eq_id_of_mono i, comp_id, id_comp, mapMono_id K]
-- case where i' : Δ'' ⟶ Δ' is the identity
by_cases h₂ : Δ' = Δ''
· subst h₂
simp only [SimplexCategory.eq_id_of_mono i', comp_id, id_comp, mapMono_id K]
-- then the RHS is always zero
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i h₁)
obtain ⟨k', hk'⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i' h₂)
have eq : Δ.len = Δ''.len + (k + k' + 2) := by omega
rw [mapMono_eq_zero K (i' ≫ i) _ _]; rotate_left
· by_contra h
simp only [left_eq_add, h, add_eq_zero, and_false, reduceCtorEq] at eq
· by_contra h
simp only [h.1, add_right_inj] at eq
cutsat
-- in all cases, the LHS is also zero, either by definition, or because d ≫ d = 0
by_cases h₃ : Isδ₀ i
· by_cases h₄ : Isδ₀ i'
· rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
· simp only [mapMono_eq_zero K i' h₂ h₄, comp_zero]
· simp only [mapMono_eq_zero K i h₁ h₃, zero_comp]
