lsum_symm_apply — Mathlib

English

A rearrangement of lsum gives the bijection underlying the free-forgetful adjunction for R-modules.

Русский

Перестановка lsum даёт биекцию, лежащую в основе свободно- forgetful адъюнкции для R-модулей.

LaTeX

$$$$ \text{lift} : (X \to M) \simeq_+ ((X \to_0 R) \to_\ell[R] M) $$$$

Lean4

theorem lsum_symm_apply (f : (α →₀ M) →ₛₗ[σ] N) (x : α) : (lsum S).symm f x = f.comp (lsingle x) :=
  rfl

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