lift_ι_apply — Mathlib

English

For given f and cond, applying the lift to iota_Q(x) yields f(x); the lift respects the embedding of M into the tensor algebra.

Русский

Для данных f и cond применение подъема к ι_Q(x) даёт f(x); подъем сохраняет вложение M в тензорную алгебру.

LaTeX

$$$\\mathrm{lift}\\ Q ⟨f, cond⟩ (\\iota_Q(x)) = f(x)$ for all x ∈ M.$$

Lean4

@[simp]
theorem lift_ι_apply (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) (x) :
    lift Q ⟨f, cond⟩ (ι Q x) = f x :=
  (LinearMap.ext_iff.mp <| ι_comp_lift f cond) x

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