hom_inv_whiskerRight_whiskerRight

English

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

Русский

Пусть η: f ≅ g – изоморфизм и h: b → c. Тогда (η.hom ▷ h) ⋅ (η.inv ▷ h) = id_{(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_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) (k : c ⟶ d) :
    η.hom ▷ h ▷ k ≫ η.inv ▷ h ▷ k = 𝟙 ((f ≫ h) ≫ k) := by simp [← comp_whiskerRight]

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