whiskerLeft_inv_hom — Mathlib

English

For a left whiskering by f of an isomorphism η: g ≅ h, the composite f ◁ η.inv ≫ f ◁ η.hom equals the identity on f ≫ h.

Русский

Для левого взвешивания f изоморфизма η: g ≅ h, композиция f ◁ η.inv с f ◁ η.hom равна тождественному отображению на f ≫ h.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_inv_hom (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h) := by
  rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

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