actionHomRight_inv_hom' — Mathlib

English

For F and objects c,d, the inverse of μᵣ equals δᵣ; i.e., inv(μᵣ F d c) = δᵣ F d c.

Русский

Для F и объектов c,d обратный к μᵣ равен δᵣ; то есть inv(μᵣ F d c) = δᵣ F d c.

LaTeX

$$$\mathrm{inv}(\mu^{\mathrm{r}} F d c) = \delta^{\mathrm{r}} F d c$$$

Lean4

@[reassoc (attr := simp)]
theorem actionHomRight_inv_hom' (x : D) {y z : C} (f : y ⟶ z) [IsIso f] : x ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (x ⊙ᵣ z) := by
  rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]

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