homEquiv_symm_naturality_one — Mathlib

English

Let adj2 be as above. For f1: X1 → Y1 and g: X2 → (G.obj (op Y1)).obj X3, the naturality of the inverse bijection holds: adj2.homEquiv.symm (g ≫ (G.map f1.op).app X3) = (F.map f1).app X2 ≫ adj2.homEquiv.symm g.

Русский

Пусть adj2 — как выше. Для f1: X1 → Y1 и g: X2 → (G.obj (op Y1)).obj X3 верна естественность обратной биекции: adj2.homEquiv.symm (g ≫ (G.map f1.op).app X3) = (F.map f1).app X2 ≫ adj2.homEquiv.symm g.

LaTeX

$$$adj_2.homEquiv.symm \,(g \;\circ\; (G.map f_1.op).\mathrm{app}\; X_3) = (F.map f_1).\mathrm{app}\; X_2 \;\circ\; adj_2.homEquiv.symm(g)$$$

Lean4

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

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