whiskerLeft_hom_inv — Mathlib

English

In a bicategory, given a morphism f: a → b and an isomorphism η: g ≅ h with g,h: b → c, the left whiskering of η by f yields a pair of 2-cells whose composition is the identity on f ≫ g; equivalently, f ◁ η.hom followed by f ◁ η.inv equals the identity on f ≫ g.

Русский

В бикатегории, пусть f: A → B и η: g ≅ h с g,h: B → C. Левое взвешивание η по f дает пару 2-ячей, чья композиция равна тождественному отображению на f ≫ g; то есть f ◁ η.hom после f ◁ η.inv равно тождеству на f ≫ g.

LaTeX

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

Lean4

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

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