The category of graded modules is abelian

This file proves that the category TauCeti.GradedModuleCat 𝒜 of graded 𝒜-modules is abelian. Kernels, cokernels and finite products are formed on underlying modules: the kernel of a morphism f : M ⟶ N is ker f with the grading of M, its cokernel is N ⧸ range f with the grading of N, and the product of finitely many graded modules is their direct sum, graded degreewise. These make sense because a map of degree zero has a homogeneous kernel and a homogeneous image.

The forgetful functor to ModuleCat A therefore preserves kernels and cokernels, and it reflects isomorphisms, because the inverse of a bijective map of degree zero again has degree zero. Since ModuleCat A is abelian, so is GradedModuleCat 𝒜. This transfer argument, which builds the Abelian instance from Abelian.PreservesCoimage.hom_coimageImageComparison, follows Mathlib's proof that FGModuleCat is abelian (Mathlib.Algebra.Category.FGModuleCat.Abelian). Together with the grading shift TauCeti.GradedModuleCat.shift 𝒜, this makes graded modules a graded abelian category, whose canonical exact structure is TauCeti.GradedExactStructure.abelian.

Main definitions

• TauCeti.GradedModuleCat.kernelCone and TauCeti.GradedModuleCat.cokernelCocone: the kernel and cokernel of a morphism of graded modules, formed on underlying modules.
• TauCeti.GradedModuleCat.cokernelGrading: the grading of N ⧸ range f induced from N.
• TauCeti.GradedModuleCat.productFan: the product of finitely many graded modules, formed as their direct sum.

Main results

• TauCeti.GradedModuleCat.kernelIsLimit, TauCeti.GradedModuleCat.cokernelIsColimit and TauCeti.GradedModuleCat.productFanIsLimit: these are limits and colimits.
• TauCeti.GradedModuleCat.mem_kernelCone_pt_piece_iff, TauCeti.GradedModuleCat.mem_cokernelCocone_pt_piece_iff and TauCeti.GradedModuleCat.mem_productFan_pt_piece_iff: the homogeneous elements of kernels, cokernels and finite products.
• The instance Abelian (TauCeti.GradedModuleCat 𝒜).
• TauCeti.GradedModuleCat.epi_iff_surjective and TauCeti.GradedModuleCat.mono_iff_injective: epimorphisms and monomorphisms are precisely the maps whose underlying linear maps are surjective and injective, respectively.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.kernelObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : GradedModuleCat 𝒜

The kernel of a morphism of graded modules: the kernel of the underlying linear map, with the grading of the source.

Equations

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

noncomputable def TauCeti.GradedModuleCat.kernelι {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : kernelObj f ⟶ M

The inclusion of the kernel of a morphism of graded modules.

Equations

• TauCeti.GradedModuleCat.kernelι f = TauCeti.GradedModuleCat.ofHom f.hom.ker.subtype ⋯

@[simp]

theorem TauCeti.GradedModuleCat.hom_kernelι {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : (kernelι f).hom = f.hom.ker.subtype

The underlying linear map of the kernel inclusion is the submodule inclusion.

@[simp]

theorem TauCeti.GradedModuleCat.kernelι_comp {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (kernelι f) f = 0

@[simp]

theorem TauCeti.GradedModuleCat.kernelι_comp_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) {Z : GradedModuleCat 𝒜} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelι f) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def TauCeti.GradedModuleCat.kernelCone {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Limits.KernelFork f

The kernel fork of a morphism of graded modules.

Equations

• TauCeti.GradedModuleCat.kernelCone f = CategoryTheory.Limits.KernelFork.ofι (TauCeti.GradedModuleCat.kernelι f) ⋯

@[simp]

theorem TauCeti.GradedModuleCat.hom_kernelCone_ι {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : (CategoryTheory.Limits.Fork.ι (kernelCone f)).hom = f.hom.ker.subtype

@[simp]

theorem TauCeti.GradedModuleCat.mem_kernelCone_pt_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) {p : ℤ} {z : (kernelCone f).pt.carrier} : z ∈ (kernelCone f).pt.grading.piece p ↔ (CategoryTheory.Limits.Fork.ι (kernelCone f)).hom z ∈ M.grading.piece p

An element of the kernel of f has degree p exactly when it has degree p in the source.

noncomputable def TauCeti.GradedModuleCat.kernelIsLimit {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Limits.IsLimit (kernelCone f)

The kernel of a morphism of graded modules is a limit.

Equations

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

instance TauCeti.GradedModuleCat.instHasKernels {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Limits.HasKernels (GradedModuleCat 𝒜)

instance TauCeti.GradedModuleCat.instPreservesLimitModuleCatWalkingParallelPairParallelPairOfNatHomToModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) toModuleCat

noncomputable def TauCeti.GradedModuleCat.cokernelGrading {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : InternalGrading k (N.carrier ⧸ f.hom.range)

The grading of the quotient of N by the image of f, whose degree-p piece is the image of Nₚ.

Equations

• TauCeti.GradedModuleCat.cokernelGrading f = (N.grading.quotient (Submodule.restrictScalars k f.hom.range) ⋯).map (Submodule.Quotient.restrictScalarsEquiv k f.hom.range)

@[simp]

theorem TauCeti.GradedModuleCat.mem_cokernelGrading_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) {p : ℤ} {y : N.carrier ⧸ f.hom.range} : y ∈ (cokernelGrading f).piece p ↔ ∃ x ∈ N.grading.piece p, Submodule.Quotient.mk x = y

An element of the quotient of N by the image of f has degree p exactly when it is the class of an element of degree p.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.cokernelObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : GradedModuleCat 𝒜

The cokernel of a morphism of graded modules: the quotient of the target by the image, with the grading induced from the target.

Equations

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

noncomputable def TauCeti.GradedModuleCat.cokernelπ {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : N ⟶ cokernelObj f

The projection onto the cokernel of a morphism of graded modules.

Equations

• TauCeti.GradedModuleCat.cokernelπ f = TauCeti.GradedModuleCat.ofHom f.hom.range.mkQ ⋯

@[simp]

theorem TauCeti.GradedModuleCat.comp_cokernelπ {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp f (cokernelπ f) = 0

@[simp]

theorem TauCeti.GradedModuleCat.comp_cokernelπ_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) {Z : GradedModuleCat 𝒜} (h : cokernelObj f ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (cokernelπ f) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def TauCeti.GradedModuleCat.cokernelCocone {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Limits.CokernelCofork f

The cokernel cofork of a morphism of graded modules.

Equations

• TauCeti.GradedModuleCat.cokernelCocone f = CategoryTheory.Limits.CokernelCofork.ofπ (TauCeti.GradedModuleCat.cokernelπ f) ⋯

@[simp]

theorem TauCeti.GradedModuleCat.hom_cokernelCocone_π {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : (CategoryTheory.Limits.Cofork.π (cokernelCocone f)).hom = f.hom.range.mkQ

@[simp]

theorem TauCeti.GradedModuleCat.mem_cokernelCocone_pt_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) {p : ℤ} {y : (cokernelCocone f).pt.carrier} : y ∈ (cokernelCocone f).pt.grading.piece p ↔ ∃ x ∈ N.grading.piece p, (CategoryTheory.Limits.Cofork.π (cokernelCocone f)).hom x = y

An element of the cokernel of f has degree p exactly when it is the class of an element of degree p.

noncomputable def TauCeti.GradedModuleCat.cokernelIsColimit {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Limits.IsColimit (cokernelCocone f)

The cokernel of a morphism of graded modules is a colimit.

Equations

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

instance TauCeti.GradedModuleCat.instHasCokernels {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Limits.HasCokernels (GradedModuleCat 𝒜)

instance TauCeti.GradedModuleCat.instPreservesColimitModuleCatWalkingParallelPairParallelPairOfNatHomToModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) toModuleCat

@[reducible, inline]

abbrev TauCeti.GradedModuleCat.directSumObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) : GradedModuleCat 𝒜

The direct sum of a family of graded modules, graded degreewise.

Equations

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

def TauCeti.GradedModuleCat.productFan {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type} (M : J → GradedModuleCat 𝒜) : CategoryTheory.Limits.Fan M

The fan exhibiting the direct sum of a family of graded modules as their product, which it is when the family is finite.

Equations

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

@[simp]

theorem TauCeti.GradedModuleCat.hom_productFan_proj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type} (M : J → GradedModuleCat 𝒜) (j : J) (x : (directSumObj M).carrier) : ((productFan M).proj j).hom x = x j

@[simp]

theorem TauCeti.GradedModuleCat.mem_productFan_pt_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type} (M : J → GradedModuleCat 𝒜) {p : ℤ} {x : (productFan M).pt.carrier} : x ∈ (productFan M).pt.grading.piece p ↔ ∀ (j : J), ((productFan M).proj j).hom x ∈ (M j).grading.piece p

An element of the direct sum has degree p exactly when each of its components does.

noncomputable def TauCeti.GradedModuleCat.productFanIsLimit {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type} (M : J → GradedModuleCat 𝒜) [Finite J] : CategoryTheory.Limits.IsLimit (productFan M)

The direct sum of finitely many graded modules is their product.

Equations

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

instance TauCeti.GradedModuleCat.instHasProduct {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type} (M : J → GradedModuleCat 𝒜) [Finite J] : CategoryTheory.Limits.HasProduct M

instance TauCeti.GradedModuleCat.instHasFiniteProducts {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Limits.HasFiniteProducts (GradedModuleCat 𝒜)

instance TauCeti.GradedModuleCat.instReflectsIsomorphismsModuleCatToModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : toModuleCat.ReflectsIsomorphisms

instance TauCeti.GradedModuleCat.instIsIsoCoimageImageComparison {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)

@[instance_reducible]

instance TauCeti.GradedModuleCat.instAbelian {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Abelian (GradedModuleCat 𝒜)

Equations

• TauCeti.GradedModuleCat.instAbelian = CategoryTheory.Abelian.ofCoimageImageComparisonIsIso

theorem TauCeti.GradedModuleCat.epi_iff_surjective {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f.hom

A morphism of graded modules is an epimorphism exactly when its underlying map is surjective.

theorem TauCeti.GradedModuleCat.mono_iff_injective {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {M N : GradedModuleCat 𝒜} (f : M ⟶ N) : CategoryTheory.Mono f ↔ Function.Injective ⇑f.hom

A morphism of graded modules is a monomorphism exactly when its underlying map is injective.

instance TauCeti.GradedModuleCat.instPreservesHomologyModuleCatToModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : toModuleCat.PreservesHomology

The forgetful functor preserves homology because kernels and cokernels are formed on underlying modules.

theorem TauCeti.GradedModuleCat.exact_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {S : CategoryTheory.ShortComplex (GradedModuleCat 𝒜)} : S.Exact ↔ Function.Exact ⇑S.f.hom ⇑S.g.hom

A short complex of graded modules is exact exactly when its underlying linear maps are exact. No additional condition on the internal degrees is needed.