English
The unit isomorphism of the two-variable equivalence equals the corresponding unit iso constructed from the same data.
Русский
Единичная изоморфия пары эквивалентностей равна соответствующей единичной изоморфии, построенной по тем же данным.
LaTeX
$$$ (\\text{equivalence₂} \\, eB \\, hF).\\text{unitIso} = \\text{equivalence₂UnitIso} \\, eB \\, hF $$$
Lean4
/-- In each positive degree, this lemma decomposes the idempotent endomorphism
`Q q` as a sum of morphisms which are postcompositions with suitable degeneracies.
As `Q q` is the complement projection to `P q`, this implies that in the case of
simplicial abelian groups, any $(n+1)$-simplex $x$ can be decomposed as
$x = x' + \sum (i=0}^{q-1} σ_{n-i}(y_i)$ where $x'$ is in the image of `P q` and
the $y_i$ are in degree $n$. -/
theorem decomposition_Q (n q : ℕ) :
((Q q).f (n + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) =
∑ i : Fin (n + 1) with i.val < q, (P i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ (Fin.rev i) :=
by
induction q with
| zero => simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero, Finset.filter_false, Finset.sum_empty]
| succ q hq =>
by_cases hqn : q + 1 ≤ n + 1
swap
· rw [Q_is_eventually_constant (show n + 1 ≤ q by cutsat), hq]
congr 1
ext ⟨x, hx⟩
simp_rw [Finset.mem_filter_univ]
cutsat
· obtain ⟨a, ha⟩ := Nat.le.dest (Nat.succ_le_succ_iff.mp hqn)
rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]
symm
conv_rhs => rw [sub_eq_add_neg, add_comm]
let q' : Fin (n + 1) := ⟨q, Nat.succ_le_iff.mp hqn⟩
rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp [q'])]
congr
· have hnaq' : n = a + q := by omega
simp only [(HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq', q'.rev_eq hnaq', neg_neg]
rfl
· ext ⟨i, hi⟩
simp_rw [Finset.mem_erase, Finset.mem_filter_univ, q', ne_eq, Fin.mk.injEq]
cutsat
