English
A product of categories indexed by Option J identifies with the binary product of the none-indexed part and the J-indexed part.
Русский
Произведение категорий, индексируемых по Option J, идентифицируется с двоичным произведением: часть без индекса none и часть с индексами some j.
LaTeX
$$$(\\forall i, C'(i)) \\simeq C'(\\mathrm{none}) \\times (\\forall j: J, C'(\\mathrm{some}(j)))$$$
Lean4
/-- A natural transformation between `F G : Paths V ⥤ C` is defined by its components and
its unary naturality squares. -/
@[simps]
def liftNatTrans {F G : Paths V ⥤ C} (α_app : (v : V) → (F.obj v ⟶ G.obj v))
(α_nat : {X Y : V} → (f : X ⟶ Y) → F.map (Quiver.Hom.toPath f) ≫ α_app Y = α_app X ≫ G.map (Quiver.Hom.toPath f)) :
F ⟶ G where
app := α_app
naturality :=
by
apply MorphismProperty.of_eq_top (P := MorphismProperty.naturalityProperty (F₁ := F) α_app)
exact morphismProperty_eq_top_of_isMultiplicative _ _ α_nat
