Internal gradings and graded objects

This file compares the two presentations of a graded module used by the DGAInfinity roadmap. An InternalGrading R M presents all degrees inside one total module M, while a CategoryTheory.GradedObject ℤ (ModuleCat R) presents the homogeneous modules separately.

The categorical total of the graded-object presentation of an internal grading is canonically isomorphic to the original module. Conversely, a graded object has a canonical internal grading on the external direct sum of its components, and recovering its graded-object presentation gives the original object degreewise.

Main definitions

• InternalGrading.toGradedObject: the family of homogeneous pieces as a Mathlib graded object.
• InternalGrading.totalIso: the canonical isomorphism from its categorical total to the original module.
• InternalGrading.ofGradedObject: the canonical internal grading on the external direct sum of a graded object.
• InternalGrading.ofGradedObjectToGradedObjectIso: the degreewise comparison with the original graded object.

@[reducible, inline]

abbrev TauCeti.InternalGrading.toGradedObject {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : CategoryTheory.GradedObject ℤ (ModuleCat R)

The homogeneous pieces of an internal grading, regarded as a Mathlib graded object.

Equations

• G.toGradedObject p = ↧↥(G.piece p)

noncomputable def TauCeti.InternalGrading.totalIso {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : ∐ G.toGradedObject ≅ ↧M

The categorical total of the graded-object presentation is the original total module.

Equations

• G.totalIso = ModuleCat.coprodIsoDirectSum G.toGradedObject ≪≫ (DirectSum.decomposeLinearEquiv G.piece).symm.toModuleIso

@[simp]

theorem TauCeti.InternalGrading.ι_totalIso_hom {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (p : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι G.toGradedObject p) G.totalIso.hom = ModuleCat.ofHom (G.piece p).subtype

On a homogeneous piece, the total comparison is the inclusion into the original module.

@[simp]

theorem TauCeti.InternalGrading.ι_totalIso_hom_assoc {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (p : ℤ) {Z : ModuleCat R} (h : ↧M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι G.toGradedObject p) (CategoryTheory.CategoryStruct.comp G.totalIso.hom h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.piece p).subtype) h

On a homogeneous piece, the total comparison is the inclusion into the original module.

@[reducible, inline]

abbrev TauCeti.InternalGrading.gradedObjectPiece (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) (p : ℤ) : Submodule R (DirectSum ℤ fun (q : ℤ) => ↑(X q))

The copy of the degree-p component inside the external direct sum of a graded object.

Equations

• TauCeti.InternalGrading.gradedObjectPiece R X p = (DirectSum.lof R ℤ (fun (q : ℤ) => ↑(X q)) p).range

noncomputable def TauCeti.InternalGrading.gradedObjectPieceEquiv (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) (p : ℤ) : ↑(X p) ≃ₗ[R] ↥(gradedObjectPiece R X p)

A component of a graded object is linearly equivalent to its copy in the external direct sum.

Equations

• TauCeti.InternalGrading.gradedObjectPieceEquiv R X p = LinearEquiv.ofInjective (DirectSum.lof R ℤ (fun (q : ℤ) => ↑(X q)) p) ⋯

@[simp]

theorem TauCeti.InternalGrading.gradedObjectPieceEquiv_apply (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) (p : ℤ) (x : ↑(X p)) : ↑((gradedObjectPieceEquiv R X p) x) = (DirectSum.lof R ℤ (fun (q : ℤ) => ↑(X q)) p) x

The canonical component equivalence agrees with the direct-sum inclusion.

noncomputable def TauCeti.InternalGrading.ofGradedObject (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) : InternalGrading R (DirectSum ℤ fun (p : ℤ) => ↑(X p))

The external direct sum of a graded object carries the internal grading by its canonical component copies.

Equations

• TauCeti.InternalGrading.ofGradedObject R X = { piece := TauCeti.InternalGrading.gradedObjectPiece R X, isInternal := ⋯ }

@[simp]

theorem TauCeti.InternalGrading.ofGradedObject_piece (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) (p : ℤ) : (ofGradedObject R X).piece p = gradedObjectPiece R X p

noncomputable def TauCeti.InternalGrading.ofGradedObjectToGradedObjectIso (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) : (ofGradedObject R X).toGradedObject ≅ X

Recovering the graded-object presentation of the canonical internal grading returns the original graded object degreewise.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.InternalGrading.ofGradedObjectToGradedObjectIso_inv_apply (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) (p : ℤ) (x : ↑(X p)) : ↑((CategoryTheory.ConcreteCategory.hom ((ofGradedObjectToGradedObjectIso R X).inv p)) x) = (DirectSum.lof R ℤ (fun (q : ℤ) => ↑(X q)) p) x

The underlying element of the inverse comparison is the canonical direct-sum inclusion.

@[simp]

theorem TauCeti.InternalGrading.ofGradedObjectToGradedObjectIso_hom_apply (R : Type u) [Ring R] (X : CategoryTheory.GradedObject ℤ (ModuleCat R)) (p : ℤ) (x : ↑((ofGradedObject R X).toGradedObject p)) : (DirectSum.lof R ℤ (fun (q : ℤ) => ↑(X q)) p) ((CategoryTheory.ConcreteCategory.hom ((ofGradedObjectToGradedObjectIso R X).hom p)) x) = ↑x

Applying the forward comparison and then including its component recovers the original element of the external direct sum.