instAlgebraOfSMulCommClass — Mathlib

English

An ext lemma for non-unital algebra homs via h on of k G; ext via congruence on of k G.

Русский

Лемма экстенсивности негомоморфизмов через сопоставление по of k G; экст через конгруэнтность по of k G.

LaTeX

$$$\forall h,\ (φ_1.toMulHom) \circ (of k G) = (φ_2.toMulHom) \circ (of k G) \Rightarrow φ_1 = φ_2$$$

Lean4

/-- The instance `Algebra k (SkewMonoidAlgebra A G)` whenever we have `Algebra k A`.
  In particular this provides the instance `Algebra k (SkewMonoidAlgebra k G)`. -/
instance [MulSemiringAction G A] [SMulCommClass G k A] : Algebra k (SkewMonoidAlgebra A G)
    where
  algebraMap := singleOneRingHom.comp (algebraMap k A)
  smul_def' r
    a := by
    ext
    simp only [RingHom.coe_comp, comp_apply, coeff_smul, Algebra.smul_def, singleOneRingHom, singleAddHom,
      ZeroHom.toFun_eq_coe, ZeroHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, coeff_single_one_mul]
  commutes' r
    f := by
    ext
    simp only [singleOneRingHom, singleAddHom, ZeroHom.toFun_eq_coe, ZeroHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk,
      OneHom.coe_mk, coeff_single_one_mul, Algebra.commutes, coeff_mul_single_one, smul_algebraMap, RingHom.coe_comp,
      comp_apply]

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