The graded Cartan equivalence

Let A be a graded algebra. The graded Cartan map from finite graded projectives to finite graded modules factors through the full subcategory of modules admitting a finite graded projective resolution. The graded resolution theorem identifies the first two Laurent Grothendieck groups.

Consequently, if every finite graded module admits such a resolution, the graded Cartan map is an isomorphism of ℤ[q,q⁻¹]-modules. Its inverse sends the class of a module to the alternating class of any finite graded projective resolution. This is the graded analogue of TauCeti.cartanEquiv.

Main definitions

• TauCeti.gradedFiniteProjectiveResolutionExactStructure: the induced graded exact structure on graded modules admitting finite resolutions by finite graded projectives.
• TauCeti.gradedModuleResolutionEquiv: the graded resolution equivalence onto that subcategory.
• TauCeti.gradedCartanEquiv: the graded Cartan map as a Laurent-linear equivalence when every finite graded module has a finite graded-projective resolution.

References

• Charles A. Weibel, The K-book, Chapter II, Theorem 7.6.
• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3.

@[reducible, inline]

noncomputable abbrev TauCeti.gradedModuleCanonicalExactStructure {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : GradedExactStructure (GradedModuleCat 𝒜)

The canonical exact structure on graded modules, graded by the internal shift.

Equations

• TauCeti.gradedModuleCanonicalExactStructure 𝒜 = TauCeti.GradedExactStructure.abelian (TauCeti.GradedModuleCat 𝒜) (TauCeti.GradedModuleCat.shift 𝒜)

theorem TauCeti.gradedAdmitsFiniteProjectiveResolution_le_finiteModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜) ≤ gradedFiniteModules 𝒜

A graded module admitting a finite resolution by finite graded projectives is itself finite. Each resolution step presents its target as a quotient of a finite graded module.

instance TauCeti.instEssentiallySmallGradedModuleCatAdmitsFiniteResolutionGradedModuleCanonicalExactStructureGradedFiniteProjectiveModules {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) : CategoryTheory.ObjectProperty.EssentiallySmall.{uA, uA, max (uA + 1) uk} ((gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜))

noncomputable def TauCeti.gradedFiniteProjectiveResolutionExactStructure {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] : GradedExactStructure ((gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)).FullSubcategory

The induced graded exact structure on graded modules admitting finite resolutions by finite graded projectives.

Equations

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

noncomputable def TauCeti.gradedModuleResolutionEquiv {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜) ≃ₗ[LaurentPolynomial ℤ] LaurentK0 (gradedFiniteProjectiveResolutionExactStructure 𝒜)

The graded resolution theorem for modules admitting finite resolutions by finite graded projectives.

Equations

• TauCeti.gradedModuleResolutionEquiv 𝒜 = (TauCeti.LaurentK0.mapEquiv (TauCeti.finiteProjectiveExactEquiv✝ 𝒜)).trans ((TauCeti.gradedModuleCanonicalExactStructure 𝒜).laurentResolutionEquiv ⋯ ⋯)

@[simp]

theorem TauCeti.gradedModuleResolutionEquiv_of {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (M : (gradedFiniteProjectiveModules 𝒜).FullSubcategory) : (gradedModuleResolutionEquiv 𝒜) (LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) M) = LaurentK0.of (gradedFiniteProjectiveResolutionExactStructure 𝒜) { obj := M.obj, property := ⋯ }

The graded resolution equivalence sends the class of a finite graded projective to its class among modules admitting finite graded-projective resolutions.

noncomputable def TauCeti.fromGradedFiniteProjectiveResolution {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] : LaurentK0 (gradedFiniteProjectiveResolutionExactStructure 𝒜) →ₗ[LaurentPolynomial ℤ] LaurentK0 (gradedFiniteModulesExactStructure 𝒜)

The comparison from modules admitting finite graded-projective resolutions to all finite graded modules.

Equations

• TauCeti.fromGradedFiniteProjectiveResolution 𝒜 = ↑(TauCeti.LaurentK0.mapEquiv (TauCeti.finiteModulesExactEquiv✝ 𝒜)).symm ∘ₗ TauCeti.LaurentK0.map (TauCeti.finiteResolutionToFiniteFunctor✝ 𝒜)

@[simp]

theorem TauCeti.fromGradedFiniteProjectiveResolution_of {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (M : GradedModuleCat 𝒜) (hM : (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜) M) : (fromGradedFiniteProjectiveResolution 𝒜) (LaurentK0.of (gradedFiniteProjectiveResolutionExactStructure 𝒜) { obj := M, property := hM }) = LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) { obj := M, property := ⋯ }

The comparison map sends an object class to the class of the same finite graded module.

theorem TauCeti.gradedCartanMap_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (x : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)) : (gradedCartanMap 𝒜) x = (fromGradedFiniteProjectiveResolution 𝒜) ((gradedModuleResolutionEquiv 𝒜) x)

The graded Cartan map factors through the modules admitting finite graded-projective resolutions.

noncomputable def TauCeti.toGradedFiniteProjectiveResolution {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) : LaurentK0 (gradedFiniteModulesExactStructure 𝒜) →ₗ[LaurentPolynomial ℤ] LaurentK0 (gradedFiniteProjectiveResolutionExactStructure 𝒜)

Under finite graded-projective dimension, compare all finite graded modules with the subcategory of modules admitting finite graded-projective resolutions.

Equations

• TauCeti.toGradedFiniteProjectiveResolution 𝒜 h = TauCeti.LaurentK0.map (TauCeti.finiteToFiniteResolutionFunctor✝ 𝒜 h) ∘ₗ ↑(TauCeti.LaurentK0.mapEquiv (TauCeti.finiteModulesExactEquiv✝ 𝒜))

@[simp]

theorem TauCeti.toGradedFiniteProjectiveResolution_of {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) (M : (gradedFiniteModules 𝒜).FullSubcategory) : (toGradedFiniteProjectiveResolution 𝒜 h) (LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) M) = LaurentK0.of (gradedFiniteProjectiveResolutionExactStructure 𝒜) { obj := M.obj, property := ⋯ }

@[simp]

theorem TauCeti.fromGradedFiniteProjectiveResolution_toGradedFiniteProjectiveResolution {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) (x : LaurentK0 (gradedFiniteModulesExactStructure 𝒜)) : (fromGradedFiniteProjectiveResolution 𝒜) ((toGradedFiniteProjectiveResolution 𝒜 h) x) = x

The map from finite-resolution modules is inverse to the map into that subcategory.

@[simp]

theorem TauCeti.toGradedFiniteProjectiveResolution_fromGradedFiniteProjectiveResolution {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) (x : LaurentK0 (gradedFiniteProjectiveResolutionExactStructure 𝒜)) : (toGradedFiniteProjectiveResolution 𝒜 h) ((fromGradedFiniteProjectiveResolution 𝒜) x) = x

The map into finite-resolution modules is inverse to their inclusion.

noncomputable def TauCeti.gradedCartanInverse {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) : LaurentK0 (gradedFiniteModulesExactStructure 𝒜) →ₗ[LaurentPolynomial ℤ] LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)

The inverse of the graded Cartan map under finite graded-projective dimension.

Equations

• TauCeti.gradedCartanInverse 𝒜 h = ↑(TauCeti.gradedModuleResolutionEquiv 𝒜).symm ∘ₗ TauCeti.toGradedFiniteProjectiveResolution 𝒜 h

theorem TauCeti.gradedCartanInverse_of_eq_foldAlternating {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) (M : GradedModuleCat 𝒜) (hM : gradedFiniteModules 𝒜 M) (r : (gradedModuleCanonicalExactStructure 𝒜).FiniteResolution (gradedFiniteProjectiveModules 𝒜) M) : (gradedCartanInverse 𝒜 h) (LaurentK0.of (gradedFiniteModulesExactStructure 𝒜) { obj := M, property := hM }) = ExactStructure.FiniteResolution.foldAlternating (fun (Z : GradedModuleCat 𝒜) (hZ : gradedFiniteProjectiveModules 𝒜 Z) => LaurentK0.of (gradedFiniteProjectiveModulesExactStructure 𝒜) { obj := Z, property := hZ }) r

The inverse Cartan map sends the class of a finite graded module to the alternating class of any finite graded-projective resolution. In particular, the result is independent of the chosen resolution.

noncomputable def TauCeti.gradedCartanEquiv {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜) ≃ₗ[LaurentPolynomial ℤ] LaurentK0 (gradedFiniteModulesExactStructure 𝒜)

If every finite graded module admits a finite graded-projective resolution, the graded Cartan map is an isomorphism of ℤ[q,q⁻¹]-modules.

Equations

• TauCeti.gradedCartanEquiv 𝒜 h = { toFun := ⇑(TauCeti.gradedCartanMap 𝒜), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(TauCeti.gradedCartanInverse 𝒜 h), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.gradedCartanEquiv_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) (x : LaurentK0 (gradedFiniteProjectiveModulesExactStructure 𝒜)) : (gradedCartanEquiv 𝒜 h) x = (gradedCartanMap 𝒜) x

@[simp]

theorem TauCeti.gradedCartanEquiv_symm_apply {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) (x : LaurentK0 (gradedFiniteModulesExactStructure 𝒜)) : (gradedCartanEquiv 𝒜 h).symm x = (gradedCartanInverse 𝒜 h) x

theorem TauCeti.gradedCartanMap_bijective {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] (𝒜 : ℤ → Submodule k A) [DirectSum.Decomposition 𝒜] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) : Function.Bijective ⇑(gradedCartanMap 𝒜)

The graded Cartan map is bijective whenever every finite graded module has a finite graded-projective resolution.