congr_hom — Mathlib

English

If F = G as functors, then for any morphism f: X → Y, F.map f equals eqToHom (congr_obj h X) ≫ G.map f ≫ eqToHom (congr_obj h Y).symm.

Русский

Если F = G как функторы, то для любого морфизма f: X → Y имеем F.map f = eqToHom (congr_obj h X) ≫ G.map f ≫ eqToHom (congr_obj h Y).symm.

LaTeX

$$$ F.map f = eqToHom (congr\_obj(h) X) \\;\\circ\\; G.map f \\;\\circ\\; eqToHom (congr\_obj(h) Y)^{\\mathrm{symm}} $$$

Lean4

@[reassoc]
theorem congr_hom {F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) :
    F.map f = eqToHom (congr_obj h X) ≫ G.map f ≫ eqToHom (congr_obj h Y).symm := by subst h; simp

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