hom_ext — Mathlib

English

If two Clifford algebra algebra homomorphisms agree on the canonical embedding ι_Q, they are equal.

Русский

Если два гомоморфизма Clifford алгебры согласны на отображении ι_Q, то они совпадают.

LaTeX

$$$f = g$ if $f \\circ ι_Q = g \\circ ι_Q$ for $f,g: Clifford(Q) → A$.$$

Lean4

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem hom_ext {A : Type*} [Semiring A] [Algebra R A] {f g : CliffordAlgebra Q →ₐ[R] A} :
    f.toLinearMap.comp (ι Q) = g.toLinearMap.comp (ι Q) → f = g :=
  by
  intro h
  apply (lift Q).symm.injective
  rw [lift_symm_apply, lift_symm_apply]
  simp only [h]
    -- This proof closely follows `TensorAlgebra.induction`

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