sum_map_inl — Mathlib

English

Let F : A ⥤ B and G : C ⥤ D be functors. The sum functor F ⊔ G : A ⊕ C ⥤ B ⊕ D satisfies that for any f : a ⟶ a' in A, (F ⊔ G).map (Sum.inl f) = Sum.inl (F.map f).

Русский

Пусть F : A ⥤ B и G : C ⥤ D — функторы. Функтор суммы F ⊔ G : A ⊕ C ⥤ B ⊕ D удовлетворяет, что для любого f : a ⟶ a' в A выполняется (F ⊔ G).map (Sum.inl f) = Sum.inl (F.map f).

LaTeX

$$$ (F \\oplus G).map\\big(\\mathrm{Sum.inl}(f)\\big) = \\mathrm{Sum.inl}\\big( F.map(f) \\big) $$$

Lean4

@[simp]
theorem sum_map_inl (F : A ⥤ B) (G : C ⥤ D) {a a' : A} (f : a ⟶ a') :
    (F.sum G).map ((Sum.inl_ _ _).map f) = (Sum.inl_ _ _).map (F.map f) := by simp [sum]

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