inv_hom_whiskerRight — Mathlib

English

Take an isomorphism η: f ≅ g and a morphism h: b → c. Then η.inv ▷ h ≫ η.hom ▷ h = id_{(g ≫ h)}.

Русский

Возьмем изоморфизм η: f ≅ g и морфизм h: b → c. Тогда η.inv ▷ h ⋅ η.hom ▷ h = id_{(g ≫ h)}}.

LaTeX

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

Lean4

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

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