lift_comp_ι — Mathlib

English

The composition of lift with ι returns the original g after applying the inverse lift; i.e., lift R (g ∘ ι) = g.

Русский

Составление lift с ι возвращает исходный g после применения обратного лифта; т.е. lift R (g ∘ ι) = g.

LaTeX

$$lift R (g.toLinearMap.comp (ι R)) = g$$

Lean4

@[simp]
theorem lift_comp_ι {A : Type*} [Semiring A] [Algebra R A] (g : TensorAlgebra R M →ₐ[R] A) :
    lift R (g.toLinearMap.comp (ι R)) = g := by
  rw [← lift_symm_apply]
  exact (lift R).apply_symm_apply g

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