Lean4
/-- The functor `Arrow C ⥤ Arrow C` that is constructed in order to apply the small
object argument to a family of morphisms `f i : A i ⟶ B i`, see the introduction
of the file `Mathlib/CategoryTheory/SmallObject/Construction.lean` -/
@[simps! obj map]
noncomputable def functor : Arrow C ⥤ Arrow C
where
obj π := Arrow.mk (πFunctorObj f π.hom)
map {π₁ π₂} τ := Arrow.homMk (functorMap f τ) τ.right
map_id
g := by
ext
· apply functorMap_id
· dsimp
map_comp {π₁ π₂ π₃} τ
τ' := by
ext
· dsimp
simp only [functorMap, Arrow.comp_left, Arrow.mk_left]
ext ⟨i, t, b, w⟩
· simp
·
simp [ι_functorMapTgt_assoc f τ i t b w _ rfl _ rfl, ι_functorMapTgt_assoc f (τ ≫ τ') i t b w _ rfl _ rfl,
ι_functorMapTgt_assoc f τ' i (t ≫ τ.left) (b ≫ τ.right) (by simp [reassoc_of% w]) (b ≫ τ.right ≫ τ'.right)
(by simp) (t ≫ (τ ≫ τ').left) (by simp)]
· dsimp
