sndHom — Mathlib

English

There is a canonical R-linear projection p: Unitization(R, A) → A defined by taking the A-component; equivalently p(inl r) = 0 and p(inr a) = a.

Русский

Существует канонический R-линейный проективный отображение p: Unitization(R, A) → A, которое возвращает компоненту A; p(inl r) = 0, p(inr a) = a.

LaTeX

$$$\exists p: Unitization(R,A) \to_{R} A,\ p(\mathrm{inl}(r)) = 0,\ p(\mathrm{inr}(a)) = a.$$$

Lean4

/-- The canonical `R`-linear projection `Unitization R A → A`. -/
@[simps apply]
def sndHom [Semiring R] [AddCommMonoid A] [Module R A] : Unitization R A →ₗ[R] A :=
  { LinearMap.snd _ _ _ with toFun := snd }

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