lift_unique — Mathlib

English

Let f: M →ₗ[R] A be linear with cond: ∀ m, f(m)^2 = 0, and g: ExteriorAlgebra R M →ₐ[R] A be an algebra homomorphism. Then g is determined by its restriction to M; namely, g ∘ ι_R = f if and only if g = lift R ⟨f, cond⟩.

Русский

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

LaTeX

$$$g \circ \iota_R = f \iff g = \mathrm{lift}_{R} \langle f,\mathrm{cond} \rangle$$$

Lean4

theorem lift_unique (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = 0) (g : ExteriorAlgebra R M →ₐ[R] A) :
    g.toLinearMap.comp (ι R) = f ↔ g = lift R ⟨f, cond⟩ :=
  CliffordAlgebra.lift_unique f _ _

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