lift_ι_apply — Mathlib

English

Let f: M →ₗ[R] A be linear with cond: ∀ m, f(m)^2 = 0. For any x ∈ M, the lifted map sends ι_R x to f x, i.e., lift R ⟨f, cond⟩ (ι_R x) = f(x).

Русский

Пусть f: M →ₗ[R] A линейно и cond: ∀ m, f(m)^2 = 0. Тогда отображение, получаемое через аппроксимацию под внешнюю алгебру, отправляет ι_R x в f(x) для любого x ∈ M, то есть lift R ⟨f, cond⟩ (ι_R x) = f(x).

LaTeX

$$$\mathrm{lift}_{R}\langle f,\mathrm{cond} \rangle (\iota_R x) = f(x)$$$

Lean4

@[simp]
theorem lift_ι_apply (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = 0) (x) : lift R ⟨f, cond⟩ (ι R x) = f x :=
  CliffordAlgebra.lift_ι_apply f _ x

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