homEquiv_naturality_left_square — Mathlib

English

A square identity expressing compatibility of left naturality with composition.

Русский

Квадратная идентичность совместимости левой натуральности со взятием композиции.

LaTeX

$$$(f : X' \to X)(g) = (F.map f) (g) \;\Rightarrow\; \text{(compatibility relation)}$$$

Lean4

@[reassoc]
theorem homEquiv_naturality_left_square (f : X' ⟶ X) (g : F.obj X ⟶ Y') (h : F.obj X' ⟶ Y) (k : Y ⟶ Y')
    (w : F.map f ≫ g = h ≫ k) : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k := by
  rw [← homEquiv_naturality_left, ← homEquiv_naturality_right, w]

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