English
Auxiliary construction giving the action on arrows induced by f on objects for thickened categories; maps an arrow i ⟶ j to the corresponding arrow in the K-thickened setting via image under f.
Русский
Вспомогательная конструкция, задающая отображение на стрелки, индуцированное отображением f на объекты; перевод стрелки i ⟶ j в соответствующую стрелку в K-усеченной конфигурации через образ под f.
LaTeX
$$$$ \mathrm{functorMap}(f,i,j) : (i \to j) \to (\mathrm{orderHom} f i \to \mathrm{orderHom} f j) $$$$
Lean4
/-- Auxiliary definition for `SimplicialThickening.functor` -/
noncomputable abbrev functorMap {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K)
(i j : SimplicialThickening J) : (i ⟶ j) ⥤ ((orderHom f i) ⟶ (orderHom f j))
where
obj
I :=
⟨f '' I.I, Set.mem_image_of_mem f I.left, Set.mem_image_of_mem f I.right, by rintro _ ⟨k, hk, rfl⟩;
exact f.monotone (I.left_le k hk), by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.le_right k hk)⟩
map f := ⟨⟨Set.image_mono f.1.1⟩⟩
