English
There is a canonical symmetry equivalence between the j-fiber of π in the swapped order and the original order, given by flipping the indices.
Русский
Существует каноническое соответствие симметрии между волоками j-слоя функций π в порядке swapped и в исходном порядке, задаваемое обменом индексов.
LaTeX
$$$\\text{symmetryEquiv}(j):\\ (π_{c_2,c_1,c_{12}}^{-1}\\{j\\}) \\simeq (π_{c_1,c_2,c_{12}}^{-1}\\{j\\}).$$$
Lean4
theorem δ_apply' (x₃ : (forget₂ C Ab).obj (S.X₃.homology i)) (x₂ : (forget₂ C Ab).obj (S.X₂.opcycles i))
(x₁ : (forget₂ C Ab).obj (S.X₁.cycles j))
(h₂ : (forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i) x₂ = (forget₂ C Ab).map (S.X₃.homologyι i) x₃)
(h₁ :
(forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j) x₁ = (forget₂ C Ab).map (S.X₂.opcyclesToCycles i j) x₂) :
(forget₂ C Ab).map (hS.δ i j hij) x₃ = (forget₂ C Ab).map (S.X₁.homologyπ j) x₁ :=
(HomologicalComplex.HomologySequence.snakeInput hS i j hij).δ_apply' x₃ x₂ x₁ h₂ h₁
