English
The extension maps compose in the expected way: mapping from i1 to i3 is the composite of the maps from i1 to i2 and i2 to i3, whenever indices are in increasing order and below j.
Русский
Расширение отображений композиционно складывается: отображение от i1 к i3 есть как композиция отображений i1→i2 и i2→i3 при i1 ≤ i2 ≤ i3 < j.
LaTeX
$$$\\text{For } i_1 \\le i_2 \\le i_3 \\le j,\\; f_{i_1,i_3}=f_{i_2,i_3}\\circ f_{i_1,i_2}.$$$
Lean4
theorem map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (hi₃ : i₃ ≤ j) :
map c i₁ i₃ (hi.trans hi') hi₃ = map c i₁ i₂ hi (hi'.trans hi₃) ≫ map c i₂ i₃ hi' hi₃ :=
by
obtain hi₁₂ | rfl := hi.lt_or_eq
· obtain hi₂₃ | rfl := hi'.lt_or_eq
· dsimp [map]
obtain hi₃' | rfl := hi₃.lt_or_eq
·
rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc, Iso.inv_hom_id_assoc, ←
Functor.map_comp_assoc, homOfLE_comp]
·
rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp), dif_pos hi₂₃, eqToHom_refl,
comp_id, assoc, assoc, Iso.inv_hom_id_assoc, Cocone.w_assoc]
· rw [map_id, comp_id]
· rw [map_id, id_comp]
