galgebra — Mathlib

English

The tensor powers together form a graded algebra over R, i.e., a DirectSum.GAlgebra structure with compatible multiplication and R‑algebra structure.

Русский

Совокупность тензорных степеней образует градуированную алгебру над R, то есть структуру DirectSum.GAlgebra с совместимым умножением и R‑алгеброй.

LaTeX

$$$ DirectSum.GAlgebra\\; R \\; (i \\mapsto ⨂[R]^i M) $$$

Lean4

/-- The tensor powers form a graded algebra.

Note that this instance implies `Algebra R (⨁ n : ℕ, ⨂[R]^n M)` via `DirectSum.Algebra`. -/
instance galgebra : DirectSum.GAlgebra R fun i => ⨂[R]^i M
    where
  toFun := (algebraMap₀ : R ≃ₗ[R] (⨂[R]^0) M).toLinearMap.toAddMonoidHom
  map_one := algebraMap₀_one
  map_mul r
    s :=
    gradedMonoid_eq_of_cast rfl
      (by
        rw [← LinearEquiv.eq_symm_apply]
        have := algebraMap₀_mul_algebraMap₀ (M := M) r s
        exact this.symm)
  commutes r
    x :=
    gradedMonoid_eq_of_cast (add_comm _ _)
      (by
        have := (algebraMap₀_mul r x.snd).trans (mul_algebraMap₀ r x.snd).symm
        rw [← LinearEquiv.eq_symm_apply, cast_symm]
        rw [← LinearEquiv.eq_symm_apply, cast_symm, cast_cast] at this
        exact this)
  smul_def r
    x :=
    gradedMonoid_eq_of_cast (zero_add x.fst).symm
      (by
        rw [← LinearEquiv.eq_symm_apply, cast_symm]
        exact (algebraMap₀_mul r x.snd).symm)

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