English
The χ-relations express coherence between the σ signs and the ε₂,ε₁ maps under permutations and preimages of π.
Русский
Отношения χ выражают когерентность знаков σ и отображений ε₂, ε₁ при перестановках и предобразах π.
LaTeX
$$$\\text{σ-ε coherence: } σ\\_ε₁ = σ ε_1 \\text{ and } σ\\_ε₂ = ε_1 σ$$$
Lean4
theorem δ_apply (x₃ : (forget₂ C Ab).obj (S.X₃.X i)) (hx₃ : (forget₂ C Ab).map (S.X₃.d i j) x₃ = 0)
(x₂ : (forget₂ C Ab).obj (S.X₂.X i)) (hx₂ : (forget₂ C Ab).map (S.g.f i) x₂ = x₃)
(x₁ : (forget₂ C Ab).obj (S.X₁.X j)) (hx₁ : (forget₂ C Ab).map (S.f.f j) x₁ = (forget₂ C Ab).map (S.X₂.d i j) x₂)
(k : ι) (hk : c.next j = k) :
(forget₂ C Ab).map (hS.δ i j hij)
((forget₂ C Ab).map (S.X₃.homologyπ i) (S.X₃.cyclesMk x₃ j (c.next_eq' hij) hx₃)) =
(forget₂ C Ab).map (S.X₁.homologyπ j) (S.X₁.cyclesMk x₁ k hk (d_eq_zero_of_f_eq_d_apply hS _ _ x₂ x₁ hx₁ _)) :=
by
refine hS.δ_apply' i j hij _ ((forget₂ C Ab).map (S.X₂.pOpcycles i) x₂) _ ?_ ?_
·
rw [← ConcreteCategory.forget₂_comp_apply, ← ConcreteCategory.forget₂_comp_apply, HomologicalComplex.p_opcyclesMap,
Functor.map_comp, ConcreteCategory.comp_apply, HomologicalComplex.homology_π_ι,
ConcreteCategory.forget₂_comp_apply, hx₂, HomologicalComplex.i_cyclesMk]
· apply (Preadditive.mono_iff_injective (S.X₂.iCycles j)).1 inferInstance
conv_lhs =>
rw [← ConcreteCategory.forget₂_comp_apply, HomologicalComplex.cyclesMap_i, ConcreteCategory.forget₂_comp_apply,
HomologicalComplex.i_cyclesMk, hx₁]
conv_rhs =>
rw [← ConcreteCategory.forget₂_comp_apply, ← ConcreteCategory.forget₂_comp_apply,
HomologicalComplex.pOpcycles_opcyclesToCycles_assoc, HomologicalComplex.toCycles_i]
