actionHom_def' — Mathlib

English

The actionHom f g can be defined as the exchange of the two ways of viewing a left and right action together with the left/right morphisms.

Русский

Гомоморфизм действия можно определить через обмен двух представлений левого и правого действия вместе с морфизмами слева и справа.

LaTeX

$$actionHom_def'$$

Lean4

@[reassoc]
theorem actionHom_def' {x₁ y₁ : D} {x₂ y₂ : C} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂) : f ⊙ᵣₘ g = x₁ ⊴ᵣ g ≫ f ⊵ᵣ y₂ :=
  action_exchange f g ▸ actionHom_def f g

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