whiskerLeft_whiskerLeft_hom_inv — Mathlib

English

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

Русский

Для f: A→B и g: B→C и изоморфизма η: h ≅ k, композиция f ◁ g ◁ η.hom ≫ f ◁ g ◁ η.inv равна тождеству на f ≫ g ≫ k.

LaTeX

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

Lean4

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

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