ι_apply — Mathlib

English

For m ∈ M, the graded embedding ι_R M m equals the corresponding degree-1 component in DirectSum via ι_R.

Русский

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

LaTeX

$$$ GradedAlgebra.ι R M m = DirectSum.of (fun i => ⨂[R]^i M) 1 ⟨TensorAlgebra.ι R m, _⟩ $$$

Lean4

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

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