lift_comp_ι — Mathlib

English

For any algebra homomorphism g: ExteriorAlgebra R M →ₐ[R] A, the lift of the map g restricted to M via ι gives back g: lift R ⟨g ∘ ι, comp_ι_sq_zero⟩ = g.

Русский

Для любого гомоморфизма алгебр g: ExteriorAlgebra R M →ₐ[R] A, продолжение по отображению g ограниченное на M через ι восстанавливает g: lift R ⟨g ∘ ι, comp_ι_sq_zero⟩ = g.

LaTeX

$$$\mathrm{lift}_{R} \langle g \circ \iota_R, \mathrm{comp\_ι\_sq\_zero} \rangle = g$$$

Lean4

@[simp]
theorem lift_comp_ι (g : ExteriorAlgebra R M →ₐ[R] A) : lift R ⟨g.toLinearMap.comp (ι R), comp_ι_sq_zero _⟩ = g :=
  CliffordAlgebra.lift_comp_ι g

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