lift_comp_ι — Mathlib

English

For any algebra hom g from Clifford(Q) to A, lifting the composite with ι_Q recovers g.

Русский

Для любого алгебра-гомоморфизма g: Clifford(Q) → A восстанавливается g через подъем: lift Q ⟨g⋅cos, comp_ι_sq_scalar⟩ = g.

LaTeX

$$$\\mathrm{lift}\\ Q ⟨g.toLinearMap \\circ (ι_Q), comp_ι_sq_scalar\\,\\rangle = g$$$

Lean4

@[simp]
theorem lift_comp_ι (g : CliffordAlgebra Q →ₐ[R] A) : lift Q ⟨g.toLinearMap.comp (ι Q), comp_ι_sq_scalar _⟩ = g := by
  exact (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g

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