English
ExtendToSucc defines an extension functor from Set.Iic j to C, extending F below j by a fixed X and τ.
Русский
ExtendToSucc задаёт расширение функторa от Set.Iic j к C, продолжая F ниже j до фиксированного X и τ.
LaTeX
$$$\\text{extendToSucc} : Set.Iic (Order.succ j) ⥤ C$$$
Lean4
theorem map_comp (i₁ i₂ i₃ : J) (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) (h : i₃ ≤ Order.succ j) :
map hj F τ i₁ i₃ (h₁₂.trans h₂₃) h = map hj F τ i₁ i₂ h₁₂ (h₂₃.trans h) ≫ map hj F τ i₂ i₃ h₂₃ h :=
by
by_cases h₁ : i₃ ≤ j
·
rw [map_eq hj F τ i₁ i₂ _ (h₂₃.trans h₁), map_eq hj F τ i₂ i₃ _ h₁, map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc,
Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
· obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))
obtain h₂ | rfl := h₂₃.lt_or_eq
· rw [Order.lt_succ_iff_of_not_isMax hj] at h₂
rw [map_eq hj F τ i₁ i₂ _ h₂]
dsimp [map]
rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂, assoc, assoc, Iso.inv_hom_id_assoc, comp_id, ←
Functor.map_comp_assoc, homOfLE_comp]
· rw [map_id, comp_id]
