lift_unique' — Mathlib

English

If F is a k-algebra homomorphism from MonoidAlgebra k G to A, then F is completely determined by its composition with of k G and the lift construction: F = lift k G A ((F : MonoidAlgebra k G →* A) ∘ of k G).

Русский

Если F — алгебра-гомоморфизм из MonoidAlgebra k G в A, то F полностью определяется через отображение из MonoidAlgebra k G в A, полученное как lift скомпонованный с of k G: F = lift k G A (F ∘ of k G).

LaTeX

$$$F = \\mathrm{lift}_{k,G,A}\\big(F \\circ \\mathrm{of}_{k,G}\\big).$$$

Lean4

theorem lift_unique' (F : MonoidAlgebra k G →ₐ[k] A) : F = lift k G A ((F : MonoidAlgebra k G →* A).comp (of k G)) :=
  ((lift k G A).apply_symm_apply F).symm

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