homEquiv_symm_naturality_three — Mathlib

English

For f3: X3 → Y3 and g: X2 → (G.obj (op X1)).obj X3, the symmetric naturality holds: adj2.homEquiv.symm (g ≫ (G.obj (op X1)).map f3) = adj2.homEquiv.symm g ≫ f3.

Русский

Для f3: X3 → Y3 и g: X2 → (G.obj (op X1)).obj X3 справедлива симметричная естественность: adj2.homEquiv.symm (g ≫ (G.obj (op X1)).map f3) = adj2.homEquiv.symm g ≫ f3.

LaTeX

$$$adj_2.homEquiv.symm (g \;\circ\; (G.obj (op X_1)).map f_3) = adj_2.homEquiv.symm(g) \circ f_3$$$

Lean4

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

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