homEquiv_naturality_right_symm — Mathlib

English

For f: X → G(Y) and g: Y → Y', the symmetric right naturality of the core hom-equivalence gives (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g.

Русский

Для f: X → G(Y) и g: Y → Y' симметричная правая натуральность CoreHomEquiv даёт (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g.

LaTeX

$$$ (\operatorname{adj.homEquiv} X Y')^{-1} (f \circ G.map g) = (\operatorname{adj.homEquiv} X Y)^{-1} f \circ g $$$

Lean4

theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
    (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g := by rw [Equiv.symm_apply_eq]; simp

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