sum_map_inr — Mathlib

English

Let F : A ⥤ B and G : C ⥤ D be functors. Then for any f : c ⟶ c' in C, (F ⊔ G).map (Sum.inr f) = Sum.inr (G.map f).

Русский

Пусть F : A ⥤ B и G : C ⥤ D — функторы. Тогда для любого f : c ⟶ c' в C выполняется (F ⊔ G).map (Sum.inr f) = Sum.inr (G.map f).

LaTeX

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

Lean4

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

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