homEquiv_naturality_two — Mathlib

English

Let adj2 be a parametrized adjunction between F and G. For morphisms f2 and g of the indicated types, the bijection adj2.homEquiv is natural in the second and third arguments; explicitly, adj2.homEquiv ((F.obj X1).map f2 ≫ g) equals f2 ≫ adj2.homEquiv g.

Русский

Пусть adj2 — параметризованная адъюнкция между F и G. Для отображений f2 и g соответствующих типов биекция adj2.homEquiv сохраняет структуру линейности по второму и третьему аргументам; то есть adj2.homEquiv ((F.obj X1).map f2 ≫ g) = f2 ≫ adj2.homEquiv g.

LaTeX

$$$\operatorname{homEquiv} \;((F\,\obj X_1).map\; f_2 \;\circ\; g) \,=\, f_2 \circ \operatorname{homEquiv}(g)$$$

Lean4

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

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