English
Let Φ be a SuccStruct on a category C with shape J, and let iter₁, iter₂, iter₃ be iterations corresponding to indices j₁, j₂, j₃. Then the composition of the two short maps obtained by first combining iter₁→iter₂ and iter₂→iter₃ equals the single map obtained by directly combining iter₁→iter₃; i.e. the two-step map equals the one-step map with the composed index.
Русский
Пусть Φ — структура Succ на категорию C, имеющая форму J, и пусть iter₁, iter₂, iter₃ — итерации, соответствующие индексам j₁, j₂, j₃. Тогда композиция двух коротких отображений, полученных из последовательного объединения iter₁→iter₂ и iter₂→iter₃, равна одному отображению, полученному напрямую из объединения iter₁→iter₃; т.е. двухшаговое отображение равно одном шагу с композицией индексов.
LaTeX
$$$ mapObj\\ iter_1\\ iter_2\\ h_{12}\\ h_1\\ h_2\\ h'_{12} \\\\;≫\\; mapObj\\ iter_2\\ iter_3\\ h_{23}\\ h_2\\ h_3\\ h'_{23} \\\\;=\\; mapObj\\ iter_1\\ iter_3\\ (h_{12}.trans h_{23})\\ h_1\\ h_3\\ (h'_{12}.trans h'_{23}) $$$
Lean4
@[reassoc (attr := simp)]
theorem mapObj_trans {j₁ j₂ j₃ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (iter₃ : Φ.Iteration j₃)
{k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂) (h₂₃ : k₂ ≤ k₃) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂)
(h₂₃' : j₂ ≤ j₃) :
mapObj iter₁ iter₂ h₁₂ h₁ h₂ h₁₂' ≫ mapObj iter₂ iter₃ h₂₃ h₂ h₃ h₂₃' =
mapObj iter₁ iter₃ (h₁₂.trans h₂₃) h₁ h₃ (h₁₂'.trans h₂₃') :=
by simp [mapObj, congr_map iter₂ iter₃ h₁₂ h₂ (h₂.trans h₂₃'), ← Functor.map_comp]
