lift_single — Mathlib

English

Let F: G →* A be a monoid homomorphism. Then for every a ∈ G and b ∈ k, the image of the basis element single a b under lift equals b times F(a): lift k G A F (single a b) = b • F(a).

Русский

Пусть F: G →* A – гомоморфизм моноидов. Тогда при любом a ∈ G и любом b ∈ k образ базисного элемента single a b под lift равен b умножить на F(a): lift k G A F (single a b) = b • F(a).

LaTeX

$$$\\mathrm{lift}_{k,G,A}(F)(\\mathrm{single}(a,b)) = b\\,F(a).$$$

Lean4

@[simp]
theorem lift_single (F : G →* A) (a b) : lift k G A F (single a b) = b • F a := by
  rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]

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