ι_apply — Mathlib

English

For any m in M, the graded injection ι followed by the degree-1 projection yields the standard exterior product map ι_R: M → ∧^1_R M; i.e., the degree-1 component of ι(m) is ι_R(m).

Русский

Для каждого элемента m из M соответствующее включение в градацию ι(m) имеет в компоненте степени 1 элемент ι_R(m).

LaTeX

$$$\pi_1(\iota_R(m)) = ι_R(m) \quad\text{and}\quad \pi_i(\iota_R(m))=0 \text{ for } i\neq 1$$$

Lean4

theorem ι_apply (m : M) :
    GradedAlgebra.ι R M m =
      DirectSum.of (fun i : ℕ => ⋀[R]^i M) 1 ⟨ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ :=
  rfl

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