whiskerLeft_hom_inv_whiskerRight — Mathlib

English

For f: a → b and g: b → c and η: h ≅ k, the composite f ◁ g ◁ η.inv ≫ f ◁ g ◁ η.hom equals id on f ≫ g ≫ k.

Русский

Пусть f: A→B, g: B→C и η: h ≅ k. Тогда f ◁ g ◁ η.inv ≫ f ◁ g ◁ η.hom = id_{f ≫ g ≫ k}.

LaTeX

$$$ f \triangleleft g \triangleleft \eta^{\mathrm{inv}} \circ f \triangleleft g \triangleleft \eta^{\mathrm{hom}} = \mathrm{id}_{f \circ g \circ k} $$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_hom_inv_whiskerRight (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) (k : c ⟶ d) :
    f ◁ η.hom ▷ k ≫ f ◁ η.inv ▷ k = 𝟙 (f ≫ g ≫ k) := by simp [← whiskerLeft_comp]

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