lift_unique' — Mathlib

English

A k-algebra homomorphism F is determined by its values on of: F = lift k G A (F ∘ of k G).

Русский

Единственность: гомоморфизм F: k[G] →ₐ[k] A определяется значениями на of: F = lift(k,G,A)(F ∘ of k G).

LaTeX

$$$F = \\mathrm{lift}_{k,G,A}\\big( (F : k[G] \\to_* A) \\circ (\\mathrm{of}_{k,G}) \\big).$$$

Lean4

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

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