homEquiv_naturality_left_square_iff

English

Equivalence between left-square naturality and composition equality.

Русский

Эквивалентность между натуральностью левого квадрата и равенством композиции.

LaTeX

$$$(f \!\gg g = h \!\gg k) \iff (F.map f \gg g = h \gg k)$$$

Lean4

theorem homEquiv_naturality_left_square_iff (f : X' ⟶ X) (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') :
    (f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k) ↔ (F.map f ≫ g = h ≫ k) :=
  ⟨fun w ↦ by simpa only [Equiv.symm_apply_apply] using homEquiv_naturality_right_square adj _ _ _ _ w,
    homEquiv_naturality_left_square adj f g h k⟩

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