Forgetting grading in the Cartan map

Forgetting the internal grading sends finite graded modules to finite modules, and finite graded projectives to finite projectives. These functors preserve the induced conflations and identify an internal shift with the original underlying module. Consequently their maps on Grothendieck groups factor through specialization at q = 1.

The resulting square with the graded and ungraded Cartan maps commutes. This is a comparison of maps, not an assertion that either forgetful map is an isomorphism: an underlying module need not admit a grading. No decomposition hypothesis on the algebra grading is needed, since the graded projective subcategory is defined by projectivity of the underlying module.

The construction uses LaurentK0.forgetGrading and the graded Cartan map. See Z. Dancso and A. Licata, "Koszul algebras and flow lattices", Section 2.2, for the specialization convention.

def TauCeti.gradedFiniteModulesForget {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : CategoryTheory.Functor (gradedFiniteModules 𝒜).FullSubcategory (FGModuleCat A)

Forget the grading of a finitely generated graded module.

Equations

• TauCeti.gradedFiniteModulesForget 𝒜 = (ModuleCat.isFG A).lift ((TauCeti.gradedFiniteModules 𝒜).ι.comp TauCeti.GradedModuleCat.toModuleCat) ⋯

def TauCeti.gradedFiniteProjectiveModulesForget {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : CategoryTheory.Functor (gradedFiniteProjectiveModules 𝒜).FullSubcategory (finiteProjectiveModules A).FullSubcategory

Forget the grading of a finitely generated graded module with projective underlying module.

Equations

• TauCeti.gradedFiniteProjectiveModulesForget 𝒜 = (TauCeti.finiteProjectiveModules A).lift ((TauCeti.gradedFiniteProjectiveModules 𝒜).ι.comp TauCeti.GradedModuleCat.toModuleCat) ⋯

@[simp]

theorem TauCeti.gradedFiniteModulesForget_obj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (M : (gradedFiniteModules 𝒜).FullSubcategory) : (gradedFiniteModulesForget 𝒜).obj M = { obj := ↧M.obj.carrier, property := ⋯ }

@[simp]

theorem TauCeti.gradedFiniteProjectiveModulesForget_obj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (M : (gradedFiniteProjectiveModules 𝒜).FullSubcategory) : (gradedFiniteProjectiveModulesForget 𝒜).obj M = { obj := ↧M.obj.carrier, property := ⋯ }

@[simp]

theorem TauCeti.gradedFiniteModulesForget_map_hom {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {M N : (gradedFiniteModules 𝒜).FullSubcategory} (f : M ⟶ N) : ((gradedFiniteModulesForget 𝒜).map f).hom = ModuleCat.ofHom f.hom.hom

@[simp]

theorem TauCeti.gradedFiniteProjectiveModulesForget_map_hom {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) {M N : (gradedFiniteProjectiveModules 𝒜).FullSubcategory} (f : M ⟶ N) : ((gradedFiniteProjectiveModulesForget 𝒜).map f).hom = ModuleCat.ofHom f.hom.hom

instance TauCeti.instAdditiveFullSubcategoryGradedModuleCatGradedFiniteModulesFGModuleCatGradedFiniteModulesForget {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : (gradedFiniteModulesForget 𝒜).Additive

instance TauCeti.instAdditiveFullSubcategoryGradedModuleCatGradedFiniteProjectiveModulesModuleCatFiniteProjectiveModulesGradedFiniteProjectiveModulesForget {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : (gradedFiniteProjectiveModulesForget 𝒜).Additive

theorem TauCeti.instPreservesFiniteLimitsGradedModuleCatModuleCatToModuleCat {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : CategoryTheory.Limits.PreservesFiniteLimits GradedModuleCat.toModuleCat

theorem TauCeti.instPreservesFiniteColimitsGradedModuleCatModuleCatToModuleCat {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : CategoryTheory.Limits.PreservesFiniteColimits GradedModuleCat.toModuleCat

theorem TauCeti.isConflationExact_gradedFiniteModulesForget {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : (gradedFiniteModulesExactStructure 𝒜).IsConflationExact (finiteModulesExactStructure A) (gradedFiniteModulesForget 𝒜)

Forgetting grading preserves the conflations of finite modules.

theorem TauCeti.isConflationExact_gradedFiniteProjectiveModulesForget {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : (gradedFiniteProjectiveModulesExactStructure 𝒜).IsConflationExact (finiteProjectiveModulesExactStructure A) (gradedFiniteProjectiveModulesForget 𝒜)

Forgetting grading preserves the conflations of finite projectives.

noncomputable def TauCeti.gradedFiniteModulesForgetShiftIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : (gradedFiniteModulesExactStructure 𝒜).shift.functor.comp (gradedFiniteModulesForget 𝒜) ≅ gradedFiniteModulesForget 𝒜

Forgetting the shift of a finite graded module gives the same underlying module.

Equations

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

noncomputable def TauCeti.gradedFiniteProjectiveModulesForgetShiftIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : (gradedFiniteProjectiveModulesExactStructure 𝒜).shift.functor.comp (gradedFiniteProjectiveModulesForget 𝒜) ≅ gradedFiniteProjectiveModulesForget 𝒜

Forgetting the shift of a finite graded projective gives the same underlying projective.

Equations

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

noncomputable def TauCeti.gradedFiniteModulesForgetK0 {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : LaurentSpecialization 1 (LaurentK0 (gradedFiniteModulesExactStructure 𝒜)) →ₗ[ℤ] ExactK0 (finiteModulesExactStructure A)

The map from specialized graded G₀ to ungraded G₀, induced by forgetting grading.

Equations

• TauCeti.gradedFiniteModulesForgetK0 𝒜 = TauCeti.LaurentK0.forgetGrading ⋯ (TauCeti.gradedFiniteModulesForgetShiftIso 𝒜)

noncomputable def TauCeti.gradedFiniteProjectiveModulesForgetK0 {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : LaurentSpecialization 1 (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)) →ₗ[ℤ] ExactK0 (finiteProjectiveModulesExactStructure A)

The map from specialized graded projective K₀ to ungraded projective K₀.

Equations

• TauCeti.gradedFiniteProjectiveModulesForgetK0 𝒜 = TauCeti.LaurentK0.forgetGrading ⋯ (TauCeti.gradedFiniteProjectiveModulesForgetShiftIso 𝒜)

@[simp]

theorem TauCeti.gradedFiniteModulesForgetK0_mk_of {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (M : (gradedFiniteModules 𝒜).FullSubcategory) : (gradedFiniteModulesForgetK0 𝒜) ((LaurentSpecialization.mk 1) (LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) M)) = ExactK0.of ((gradedFiniteModulesForget 𝒜).obj M)

Forgetting grading on a specialized module class gives its underlying module class.

@[simp]

theorem TauCeti.gradedFiniteProjectiveModulesForgetK0_mk_of {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (M : (gradedFiniteProjectiveModules 𝒜).FullSubcategory) : (gradedFiniteProjectiveModulesForgetK0 𝒜) ((LaurentSpecialization.mk 1) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) M)) = ExactK0.of ((gradedFiniteProjectiveModulesForget 𝒜).obj M)

Forgetting grading on a specialized projective class gives its underlying projective class.

noncomputable def TauCeti.gradedCartanMapSpecialized {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (ε : ℤˣ) : LaurentSpecialization ε (LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)) →ₗ[ℤ] LaurentSpecialization ε (LaurentK0 (gradedFiniteModulesExactStructure 𝒜))

The Cartan map specialized at a unit of ℤ. In particular it is defined at q = ±1.

Equations

• TauCeti.gradedCartanMapSpecialized 𝒜 ε = TauCeti.LaurentSpecialization.map ε (TauCeti.gradedCartanMap 𝒜)

@[simp]

theorem TauCeti.gradedCartanMapSpecialized_mk {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) (ε : ℤˣ) (x : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)) : (gradedCartanMapSpecialized 𝒜 ε) ((LaurentSpecialization.mk ε) x) = (LaurentSpecialization.mk ε) ((gradedCartanMap 𝒜) x)

Specializing the Cartan map commutes with the quotient class map.

theorem TauCeti.gradedFiniteModulesForgetK0_comp_gradedCartanMapSpecialized {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : gradedFiniteModulesForgetK0 𝒜 ∘ₗ gradedCartanMapSpecialized 𝒜 1 = (cartanMap A).toIntLinearMap ∘ₗ gradedFiniteProjectiveModulesForgetK0 𝒜

Forgetting grading recovers the ungraded Cartan map. The square from graded projective K₀ and graded module G₀, specialized at q = 1, to their ungraded counterparts commutes.