div_faithful — Mathlib

English

The divided faithful functor is faithful if F is faithful and G is faithful with appropriate data.

Русский

Разделённый верный функтор верен, если F и G верны и данные соответствуют условиям.

LaTeX

$$$\text{Faithful.div } F G obj h_obj map h_map\text{ is faithful}$$$

Lean4

theorem div_faithful (F : C ⥤ E) [F.Faithful] (G : D ⥤ E) [G.Faithful] (obj : C → D)
    (h_obj : ∀ X, G.obj (obj X) = F.obj X) (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y} {f : X ⟶ Y}, G.map (map f) ≍ F.map f) :
    Functor.Faithful (Faithful.div F G obj @h_obj @map @h_map) :=
  (Faithful.div_comp F G _ h_obj _ @h_map).faithful_of_comp

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