objEquiv — Mathlib

English

An object of the action category corresponding to M acting on X is naturally in bijection with an element of X. This yields an equivalence of categories X ≃ ActionCategory M X.

Русский

Объект категории действия, заданный действием M на X, естественно эквивалентен элементу X; существует эквиваленция X ≃ ActionCategory M X.

LaTeX

$$$X \simeq \text{ActionCategory } M X$ with $\text{objEquiv}$ mapping $x \mapsto x$ and inverse mapping via the back operation.$$

Lean4

/-- An object of the action category given by M ↻ X corresponds to an element of X. -/
def objEquiv : X ≃ ActionCategory M X where
  toFun x := x
  invFun x := x.back
  left_inv := coe_back
  right_inv := back_coe

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