English
A constructed equivalence of a divisor-type functor preserves compositional equality with a given functor G; the displayed two sides are equal after applying G and then composing.
Русский
Сконструированное разделение типа дивидента сохраняет равенство композиции с данным функтором G; две стороны совпадают после применения G и затем композиции.
LaTeX
$$$\text{Divisor compatibility: } (Faithful.div F G obj h_obj map h_map).comp G = F$$$
Lean4
theorem div_comp (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) :
Faithful.div F G obj @h_obj @map @h_map ⋙ G = F :=
by
obtain ⟨F_obj, _, _, _⟩ := F; obtain ⟨G_obj, _, _, _⟩ := G
unfold Faithful.div Functor.comp
have : F_obj = G_obj ∘ obj := (funext h_obj).symm
subst this
congr
simp only [Function.comp_apply, heq_eq_eq] at h_map
ext
exact h_map
