Documentation

Mathlib.Algebra.MonoidAlgebra.Grading

Internal grading of an AddMonoidAlgebra #

In this file, we show that an AddMonoidAlgebra has an internal direct sum structure.

Main results #

@[inline, reducible]
abbrev AddMonoidAlgebra.gradeBy {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : Mι) (i : ι) :

The submodule corresponding to each grade given by the degree function f.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[inline, reducible]
    abbrev AddMonoidAlgebra.grade {M : Type u_1} (R : Type u_3) [CommSemiring R] (m : M) :

    The submodule corresponding to each grade.

    Equations
    Instances For
      theorem AddMonoidAlgebra.mem_gradeBy_iff {M : Type u_1} {ι : Type u_2} (R : Type u_3) [CommSemiring R] (f : Mι) (i : ι) (a : AddMonoidAlgebra R M) :
      a AddMonoidAlgebra.gradeBy R f i a.support f ⁻¹' {i}
      theorem AddMonoidAlgebra.mem_grade_iff {M : Type u_1} (R : Type u_3) [CommSemiring R] (m : M) (a : AddMonoidAlgebra R M) :
      a AddMonoidAlgebra.grade R m a.support {m}
      theorem AddMonoidAlgebra.single_mem_gradeBy {M : Type u_1} {ι : Type u_2} {R : Type u_4} [CommSemiring R] (f : Mι) (m : M) (r : R) :
      def AddMonoidAlgebra.decomposeAux {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) :
      AddMonoidAlgebra R M →ₐ[R] DirectSum ι fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)

      Auxiliary definition; the canonical grade decomposition, used to provide DirectSum.decompose.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem AddMonoidAlgebra.decomposeAux_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) (m : M) (r : R) :
        (AddMonoidAlgebra.decomposeAux f) (Finsupp.single m r) = (DirectSum.of (fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)) (f m)) { val := Finsupp.single m r, property := (_ : Finsupp.single m r AddMonoidAlgebra.gradeBy R (f) (f m)) }
        theorem AddMonoidAlgebra.decomposeAux_coe {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) {i : ι} (x : (AddMonoidAlgebra.gradeBy R (f) i)) :
        (AddMonoidAlgebra.decomposeAux f) x = (DirectSum.of (fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)) i) x
        instance AddMonoidAlgebra.gradeBy.gradedAlgebra {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) :
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem AddMonoidAlgebra.GradesBy.decompose_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) (m : M) (r : R) :
        (DirectSum.decompose (AddMonoidAlgebra.gradeBy R f)) (Finsupp.single m r) = (DirectSum.of (fun (i : ι) => (AddMonoidAlgebra.gradeBy R (f) i)) (f m)) { val := Finsupp.single m r, property := (_ : Finsupp.single m r AddMonoidAlgebra.gradeBy R (f) (f m)) }
        Equations
        • AddMonoidAlgebra.grade.decomposition = inferInstance
        @[simp]
        theorem AddMonoidAlgebra.grade.decompose_single {ι : Type u_2} {R : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (i : ι) (r : R) :

        AddMonoidAlgebra.gradeBy describe an internally graded algebra.