homEquiv_symm_naturality_two — Mathlib

English

In the setting above, for f2: X2 → Y2 and g: Y2 → (G.obj (op X1)).obj X3, the inverse naturality is adj2.homEquiv.symm (f2 ≫ g) = (F.obj X1).map f2 ≫ adj2.homEquiv.symm g.

Русский

В той же установке: для f2: X2 → Y2 и g: Y2 → (G.obj (op X1)).obj X3, обратная естественность: adj2.homEquiv.symm (f2 ≫ g) = (F.obj X1).map f2 ≫ adj2.homEquiv.symm g.

LaTeX

$$$adj_2.homEquiv.symm (f_2 \;\circ\; g) = (F.obj X_1).map f_2 \;\circ\; adj_2.homEquiv.symm(g)$$$

Lean4

@[reassoc]
theorem homEquiv_symm_naturality_two (f₂ : X₂ ⟶ Y₂) (g : Y₂ ⟶ (G.obj (op X₁)).obj X₃) :
    adj₂.homEquiv.symm (f₂ ≫ g) = (F.obj X₁).map f₂ ≫ adj₂.homEquiv.symm g :=
  adj₂.homEquiv.injective (by simp [homEquiv_naturality_two])

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