functoriality_faithful — Mathlib

English

Let F: J → C and G: C → D be functors. If G is faithful, then the induced functor Cones.functoriality(F, G) is faithful.

Русский

Пусть F: J → C и G: C → D — функторы. Если G является верным функтором, то индуцированный переходник Cones.functoriality(F, G) верен (то есть верен по отношению к морфизмам конусов).

LaTeX

$$$\mathrm{Faithful}(G) \Rightarrow \mathrm{Faithful}(\mathrm{Cones.functoriality}(F,G))$$$

Lean4

instance functoriality_faithful [G.Faithful] : (Cones.functoriality F G).Faithful where
  map_injective {_X} {_Y} f g h := ConeMorphism.ext f g <| G.map_injective <| congr_arg ConeMorphism.hom h

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