action_exchange — Mathlib

English

There is a symmetry between exchanging left and right action morphisms under the action functor.

Русский

Существует симметрия между преобразованиями левого и правого действия при переключении через соответствующий функтор действия.

LaTeX

$$action_exchange$$

Lean4

@[reassoc]
theorem action_exchange {w x : D} {y z : C} (f : w ⟶ x) (g : y ⟶ z) : w ⊴ᵣ g ≫ f ⊵ᵣ z = f ⊵ᵣ y ≫ x ⊴ᵣ g := by
  simp only [← id_actionHom, ← actionHom_id, ← actionHom_comp, id_comp, comp_id]

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