additive_of_comp_faithful — Mathlib

English

Let F: C → D and G: D → E be functors between preadditive categories. If G is additive and the composite F ∘ G is additive, and G is faithful, then F is additive.

Русский

Пусть F: C → D и G: D → E — функторы между предаддитивными категориями. Если G аддитивен и композиция F ∘ G аддитивна, а также G верен, то F аддитивен.

LaTeX

$$$ (F \circ G)\text{ additive} \land G\text{ additive} \land \text{Faithful}(G) \Rightarrow F\text{ additive}$$$

Lean4

theorem additive_of_comp_faithful (F : C ⥤ D) (G : D ⥤ E) [G.Additive] [(F ⋙ G).Additive] [Faithful G] : F.Additive
    where
  map_add
    {_ _ f₁
      f₂} :=
    G.map_injective (by rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map])

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