homEquiv_naturality_left — Mathlib

English

Given f: X' → X and g: F(X) → Y, the left naturality of the hom-equivalence says (adj.homEquiv X' Y)(F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g.

Русский

Для f: X' → X и g: F(X) → Y левоe натуральности гом-эквивалентности: (adj.homEquiv X' Y)(F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g.

LaTeX

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

Lean4

theorem homEquiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
    (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g := by rw [← Equiv.eq_symm_apply]; simp

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