actionHomRight_inv_hom — Mathlib

English

For an isomorphism f: x ⟶ y in C and z in D, composing actionHomLeft f.inv with actionHomLeft f.hom yields the identity on y ⊙ z.

Русский

Для изоморфизма f: x ⟶ y в C и z в D, композиция actionHomLeft f.inv с actionHomLeft f.hom даёт единицу на y ⊙ z.

LaTeX

$$$\\forall f:\\; x \\cong y,\\; z:\\; f.inv ⊵ₗ z ≫ f.hom ⊵ₗ z = 𝟙 (y ⊙ₗ z)$$$

Lean4

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

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