sum_obj_inr — Mathlib

English

The objects of the sum of functors F.sum G on inl and inr are preserved to the corresponding left and right injections respectively.

Русский

Объекты суммы функторов F.sum G на inl и inr сохраняются в соответствующие левый и правый инъекции.

LaTeX

$$$$ (F.sum G).obj (\mathrm{inl} a) = \mathrm{inl}(F.obj a), \quad (F.sum G).obj (\mathrm{inr} c) = \mathrm{inr}(G.obj c). $$$$

Lean4

@[simp]
theorem sum_obj_inr (F : A ⥤ B) (G : C ⥤ D) (c : C) : (F.sum G).obj (inr c) = inr (G.obj c) :=
  rfl

Похожие утверждения