homEquiv_naturality_left_symm — Mathlib

English

Naturality of the left side of the hom-equivalence: precompose on X corresponds to applying F on the morphism and then composing with the inverse homEquiv.

Русский

Естественность слева для гом-эквивалентности: предварительное композирование в X соответствует применению F к гомоморфизму и последующему композированию с обратной homEquiv.

LaTeX

$$$(adj.homEquiv X' Y).symm (f \circ g) = F.map f \circ (adj.homEquiv X Y).symm g$$$

Lean4

theorem homEquiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
    (adj.homEquiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.homEquiv X Y).symm g := by simp

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