hom_inv_actionHomLeft — Mathlib

English

Inverse of the left-action homomorphism composed with the inverse morphism equals identity after action.

Русский

Обратное левого отображения действия, составленное с обратным морфизмом, даёт тождество через действие.

LaTeX

$$inv_hom_actionHomLeft'$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_actionHomLeft {x y : D} (f : x ≅ y) (z : C) : f.hom ⊵ᵣ z ≫ f.inv ⊵ᵣ z = 𝟙 (x ⊙ᵣ z) := by
  rw [← comp_actionHomLeft, Iso.hom_inv_id, id_actionHomLeft]

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