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) [DecidableEq M] [CommSemiring R] (f : Mι) (i : ι) :

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

Instances For
    @[inline, reducible]
    abbrev AddMonoidAlgebra.grade {M : Type u_1} (R : Type u_3) [DecidableEq M] [CommSemiring R] (m : M) :

    The submodule corresponding to each grade.

    Instances For
      theorem AddMonoidAlgebra.mem_gradeBy_iff {M : Type u_1} {ι : Type u_2} (R : Type u_3) [DecidableEq M] [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) [DecidableEq M] [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} [DecidableEq M] {R : Type u_4} [CommSemiring R] (f : Mι) (m : M) (r : R) :
      (fun₀ | m => r) AddMonoidAlgebra.gradeBy R f (f m)
      theorem AddMonoidAlgebra.single_mem_grade {M : Type u_1} [DecidableEq M] {R : Type u_4} [CommSemiring R] (i : M) (r : R) :
      (fun₀ | i => r) AddMonoidAlgebra.grade R i
      def AddMonoidAlgebra.decomposeAux {M : Type u_1} {ι : Type u_2} {R : Type u_3} [DecidableEq M] [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) :
      AddMonoidAlgebra R M →ₐ[R] ⨁ (i : ι), { x // x AddMonoidAlgebra.gradeBy R (f) i }

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

      Instances For
        theorem AddMonoidAlgebra.decomposeAux_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [DecidableEq M] [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) (m : M) (r : R) :
        (↑(AddMonoidAlgebra.decomposeAux f) fun₀ | m => r) = ↑(DirectSum.of (fun i => { x // x AddMonoidAlgebra.gradeBy R (f) i }) (f m)) { val := fun₀ | m => r, property := (_ : (fun₀ | m => r) AddMonoidAlgebra.gradeBy R (f) (f m)) }
        theorem AddMonoidAlgebra.decomposeAux_coe {M : Type u_1} {ι : Type u_2} {R : Type u_3} [DecidableEq M] [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) {i : ι} (x : { x // x AddMonoidAlgebra.gradeBy R (f) i }) :
        ↑(AddMonoidAlgebra.decomposeAux f) x = ↑(DirectSum.of (fun i => { x // x AddMonoidAlgebra.gradeBy R (f) i }) i) x
        @[simp]
        theorem AddMonoidAlgebra.GradesBy.decompose_single {M : Type u_1} {ι : Type u_2} {R : Type u_3} [DecidableEq M] [AddMonoid M] [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) (m : M) (r : R) :
        (↑(DirectSum.decompose (AddMonoidAlgebra.gradeBy R f)) fun₀ | m => r) = ↑(DirectSum.of (fun i => { x // x AddMonoidAlgebra.gradeBy R (f) i }) (f m)) { val := fun₀ | m => r, property := (_ : (fun₀ | m => r) AddMonoidAlgebra.gradeBy R (f) (f m)) }
        @[simp]
        theorem AddMonoidAlgebra.grade.decompose_single {ι : Type u_2} {R : Type u_3} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] (i : ι) (r : R) :
        (↑(DirectSum.decompose (AddMonoidAlgebra.grade R)) fun₀ | i => r) = ↑(DirectSum.of (fun i => { x // x AddMonoidAlgebra.grade R i }) i) { val := fun₀ | i => r, property := (_ : (fun₀ | i => r) AddMonoidAlgebra.grade R i) }

        AddMonoidAlgebra.gradeBy describe an internally graded algebra.