gradedAlgebra — Mathlib

English

There exists a graded algebra structure on gradeBy R f, i.e., gradeBy(R, f) is equipped with a grading by ι compatible with algebra multiplication: the product of elements from grades i and j lies in grade i+j.

Русский

Существует градуированная по ι структура алгебры на gradeBy R f; операция умножения совместима с градацией: произведение элементов из компонент i и j принадлежит grade i+j.

LaTeX

$$$\text{GradedAlgebra}(\mathrm{gradeBy}\;R\;f)$$$

Lean4

instance gradedAlgebra : GradedAlgebra (gradeBy R f) :=
  GradedAlgebra.ofAlgHom _ (decomposeAux f)
    (by
      ext : 4
      dsimp
      rw [decomposeAux_single, DirectSum.coeAlgHom_of, Subtype.coe_mk])
    fun i x => by
    rw [decomposeAux_coe f x]
      -- Lean can't find this later without us repeating it

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