hom_ext — Mathlib

English

If two algebra homomorphisms f and g from ExteriorAlgebra R M to A agree on ι_R(M), then f = g; the map is determined by its values on generators.

Русский

Если два гомоморфизма алгебр f и g из ExteriorAlgebra R M в A совпадают на ι_R(M), то f = g; отображение определяется по значениям на генераторы.

LaTeX

$$$\mathrm{hom}_{ext} : (f,g) \,|\, f\circ\iota_R = g\circ\iota_R \Rightarrow f = g$$$

Lean4

/-- See note [partially-applied ext lemmas]. -/
@[ext]
theorem hom_ext {f g : ExteriorAlgebra R M →ₐ[R] A} (h : f.toLinearMap.comp (ι R) = g.toLinearMap.comp (ι R)) : f = g :=
  CliffordAlgebra.hom_ext h

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