hext — Mathlib

English

Two functors F and G are equal if they are equal on objects and their action on morphisms is HEq-preserving.

Русский

Два функторы F и G равны, если их значения на объектах совпадают и их действие на морфизмы сохраняет HEq.

LaTeX

$$$ F = G \\ \\\\text{ if } F.obj X = G.obj X \\text{ for all } X \\text{ and } F.map f \\mathrel{≍} G.map f \\text{ for all } f$$$

Lean4

/-- Proving equality between functors using heterogeneous equality. -/
theorem hext {F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X) (h_map : ∀ (X Y) (f : X ⟶ Y), F.map f ≍ G.map f) : F = G :=
  Functor.ext h_obj fun _ _ f => (conj_eqToHom_iff_heq _ _ (h_obj _) (h_obj _)).2 <| h_map _ _ f

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