instIsScalarTowerMonoidAlgebraAsModule

English

The module ρ.asModule carries a compatible action of k and of MonoidAlgebra k G, making it a module over the scalar ring k and the monoid-algebra in a coherent way: (t • a) • v = t • (a • v).

Русский

Модуль ρ.asModule имеет совместное действие скаляров из k и моноидальной алгебры kG, удовлетворяющее тождесту (t • a) • v = t • (a • v).

LaTeX

$$$\\forall t \\in k, \\forall a \\in \\mathrm{MonoidAlgebra}(k,G), \\forall v \\in ρ.asModule:\\ (t \\cdot a) \\cdot v = t \\cdot (a \\cdot v).$$$

Lean4

instance : IsScalarTower k (MonoidAlgebra k G) ρ.asModule where
  smul_assoc t x
    v := by
    revert t
    apply x.induction_on
    · simp
    · intro y z hy hz
      simp [add_smul, hy, hz]
    · intro s y hy t
      rw [← smul_assoc, smul_eq_mul, hy (t * s), ← smul_eq_mul, smul_assoc]
      aesop

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