Graded rings from homogeneous multiplications of modules #

Let M : ι → ModuleCat R be a family of R-modules indexed by an additive monoid, equipped with a unit one : R ⟶ M 0 and homogeneous multiplications mul i j : M i ⊗ M j ⟶ M (i + j) satisfying the graded unit and associativity laws, stated up to the identifications of degrees 0 + n = n, n + 0 = n and i + j + k = i + (j + k). These are the laws of a monoid object in graded R-modules, written degree by degree. This file turns such data into Mathlib's graded ring structure on the family of carriers:

TauCeti.ModuleCat.gRingOfHomogeneous: the DirectSum.GRing structure whose homogeneous product of a : M i and b : M j is mul i j (a ⊗ₜ b) and whose unit is one 1;
TauCeti.ModuleCat.gCommRingOfHomogeneous: the DirectSum.GCommRing structure, when the homogeneous multiplications are moreover graded commutative;
TauCeti.ModuleCat.gAlgebraOfHomogeneous: the DirectSum.GAlgebra R structure whose structure map is one.

Through Mathlib's instances on direct sums these make ⨁ i, M i a (commutative) R-algebra in which DirectSum.of _ i a * DirectSum.of _ j b = DirectSum.of _ (i + j) (mul i j (a ⊗ₜ b)). This is the graded analogue of ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toRing, which makes a monoid object of ModuleCat R a ring. Its main use is to give rings of sections of a graded algebra of sheaves of modules their graded multiplication.

None of these structures is an instance, since the homogeneous multiplication is data that is not determined by the family M.

source

theorem TauCeti.ModuleCat.gradedMonoid_mk_eqToHom_hom {R : Type u} {ι : Type u_1} [Ring R] (M : ι → ModuleCat R) {n m : ι} (h : n = m) (x : ↑(M n)) :

GradedMonoid.mk m ((ModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) x) = GradedMonoid.mk n x

Transporting an element along an identification of degrees does not change the element of the graded monoid.

source

theorem TauCeti.ModuleCat.gradedMonoid_mk_mul_one_hom_tmul {R : Type u} {ι : Type u_1} [CommRing R] [AddZeroClass ι] {M : ι → ModuleCat R} {one : CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R) ⟶ M 0} {mul : (i j : ι) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} (one_mul : ∀ (n : ι), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one (M n)) (mul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (r : R) {n : ι} (a : ↑(M n)) :

GradedMonoid.mk (0 + n) ((ModuleCat.Hom.hom (mul 0 n)) ((ModuleCat.Hom.hom one) r ⊗ₜ[R] a)) = GradedMonoid.mk n (r • a)

The left unit law, applied to r ⊗ₜ a: multiplying by the image of r in degree zero is scalar multiplication by r, as elements of the graded monoid.

source

theorem TauCeti.ModuleCat.gradedMonoid_mk_mul_tmul_one_hom {R : Type u} {ι : Type u_1} [CommRing R] [AddZeroClass ι] {M : ι → ModuleCat R} {one : CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R) ⟶ M 0} {mul : (i j : ι) → CategoryTheory.MonoidalCategoryStruct.tensorObj (M i) (M j) ⟶ M (i + j)} (mul_one : ∀ (n : ι), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M n) one) (mul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M n)).hom (CategoryTheory.eqToHom ⋯)) (r : R) {n : ι} (a : ↑(M n)) :

GradedMonoid.mk (n + 0) ((ModuleCat.Hom.hom (mul n 0)) (a ⊗ₜ[R] (ModuleCat.Hom.hom one) r)) = GradedMonoid.mk n (r • a)

The right unit law, applied to a ⊗ₜ r: multiplying by the image of r in degree zero is scalar multiplication by r, as elements of the graded monoid.

source

@[instance_reducible]

DirectSum.GRing fun (i : ι) => ↑(M i)

The graded ring structure on the carriers of a family of modules M with a unit one : R ⟶ M 0 and homogeneous multiplications mul i j : M i ⊗ M j ⟶ M (i + j) satisfying the graded unit and associativity laws. The product of a : M i and b : M j is mul i j (a ⊗ₜ b) and the unit is one 1.

Instances For

source

@[simp]