English
The morphism map in extendToSucc is defined by cases depending on i₁,i₂ with hi and hi₂, matching the corresponding maps in F and the isomorphisms.
Русский
Гомоморфизм map в extendToSucc задаётся по случаям в зависимости от i₁,i₂ с hi и hi₂, согласуясь с отображениями F и изоморфизмами.
LaTeX
$$$\\text{map}\\; \\; i_1\\ i_2\\ hi\\ hi_2 = \\cdots$ (case distinction expressed in definitional form)$$
Lean4
/-- `extendToSucc`, on morphisms. -/
def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ Order.succ j) : obj F X ⟨i₁, hi.trans hi₂⟩ ⟶ obj F X ⟨i₂, hi₂⟩ :=
if h₁ : i₂ ≤ j then (objIso F X ⟨i₁, hi.trans h₁⟩).hom ≫ F.map (homOfLE hi) ≫ (objIso F X ⟨i₂, h₁⟩).inv
else
if h₂ : i₁ ≤ j then
(objIso F X ⟨i₁, h₂⟩).hom ≫
F.map (homOfLE h₂) ≫
τ ≫
(objSuccIso hj F X).inv ≫
eqToHom
(by
congr
exact le_antisymm (Order.succ_le_of_lt (not_le.1 h₁)) hi₂)
else
eqToHom
(by
congr
rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))])
