homEquiv_naturality_three — Mathlib

English

Let adj2 be a parametrized adjunction as above. For f3: X3 → Y3 and g: (F.obj X1).obj X2 → X3, the naturality in the third variable holds: adj2.homEquiv (g ≫ f3) = adj2.homEquiv g ≫ (G.obj (op X1)).map f3.

Русский

Пусть adj2 — параметризованная адъюнкция. Для f3: X3 → Y3 и g: (F.obj X1).obj X2 → X3 верна естественность по третьему аргументу: adj2.homEquiv (g ≫ f3) = adj2.homEquiv g ≫ (G.obj (op X1)).map f3.

LaTeX

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

Lean4

@[reassoc]
theorem homEquiv_naturality_three (f₃ : X₃ ⟶ Y₃) (g : (F.obj X₁).obj X₂ ⟶ X₃) :
    adj₂.homEquiv (g ≫ f₃) = adj₂.homEquiv g ≫ (G.obj (op X₁)).map f₃ :=
  (adj₂.adj X₁).homEquiv_naturality_right _ _

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