homEquiv_naturality_right_square_iff

English

Dual statement to the left-square-iff, relating right-square naturality to composition equality.

Русский

Дуальное утверждение к left-square-iff, связывающее правую квадратную натуральность с равенством композиций.

LaTeX

$$$(f \to g) \iff (f \to g)$$$

Lean4

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

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