id_comm — Mathlib

English

The monoid of natural endomorphisms of the identity functor is commutative: for any α,β : 1_C ⟶ 1_C, α ≫ β = β ≫ α.

Русский

Моноид натуральных самопреобразований тождества коммутативен: для любых α,β : 1_C ⟶ 1_C выполняется α ≫ β = β ≫ α.

LaTeX

$$$ \forall \alpha,\beta : (\mathsf{Id}_\mathcal{C}) \Rightarrow \alpha \circ \beta = \beta \circ \alpha. $$$

Lean4

/-- The monoid of natural transformations of the identity is commutative. -/
theorem id_comm (α β : (𝟭 C) ⟶ (𝟭 C)) : α ≫ β = β ≫ α := by
  ext X
  exact (α.naturality (β.app X)).symm

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