hom_inv_whiskerRight — Mathlib

English

Let η be an isomorphism η: f ≅ g between 1-morphisms a → b, and h: b → c. Then whiskering η on the right by h yields an isomorphism η.hom ▷ h with inverse η.inv ▷ h, and their composition is the identity on f ≫ h.

Русский

Пусть η: f ≅ g – изоморфизм между 1-морфизмами a → b и h: b → c. Тогда правое взвешивание η по h дает изоморфизм η.hom ▷ h с обратным η.inv ▷ h, чей состав равен тождеству на f ≫ h.

LaTeX

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

Lean4

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

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