The Cartan map of a ring

For a ring R, the finitely generated R-modules and the finitely generated projective R-modules are two full subcategories of ModuleCat R, each extension closed for the canonical exact structure of the abelian category ModuleCat R. This file equips them with the induced exact structures and constructs the homomorphism of exact Grothendieck groups

c_R : K₀(proj R) ⟶ G₀(mod R)

induced by the inclusion of the finitely generated projectives into the finitely generated modules. Here K₀(proj R) is the exact K₀ of the finitely generated projectives and G₀(mod R) is the exact K₀ of the finitely generated modules. Over a noetherian ring the latter is the usual G₀ (Weibel, The K-book, Definition II.6.2); over a general ring the usual G₀ is defined through pseudo-coherent modules instead (Example II.7.1.4 and Exercise II.7.3 there). The first structure is the split one, by TauCeti.finiteProjectiveModulesExactStructure_eq_split, because a short exact sequence of modules with projective quotient splits.

The two subcategories are essentially small — every finitely generated module is a quotient of some Rⁿ — which is what makes their Grothendieck groups small types, and the Cartan map lives in the same universe as R.

The main theorem is the module form of the resolution theorem: if every finitely generated R-module admits a finite resolution by finitely generated projectives, then c_R is an isomorphism, with inverse the alternating class of any such resolution. This is deduced from the categorical resolution theorem TauCeti.ExactStructure.resolutionEquiv by factoring the Cartan map through the modules admitting finite resolutions by finitely generated projectives. Over a semisimple ring the hypothesis holds for the trivial reason that every module is projective, which is recorded as TauCeti.cartanEquivOfIsSemisimpleRing.

Nothing here computes a Cartan matrix; TauCeti.cartanMatrix is the matrix of cartanMap over an Artinian ring, in the indecomposable-projective and simple bases.

Main definitions

• ModuleCat.isFG and TauCeti.finiteProjectiveModules: the two object properties.
• TauCeti.finiteModulesExactStructure, TauCeti.finiteProjectiveModulesExactStructure and TauCeti.finiteProjectiveResolutionExactStructure: the exact structures induced on them, and on the modules admitting finite resolutions by finitely generated projectives, by the canonical exact structure of ModuleCat R.
• TauCeti.cartanMap: the Cartan map K₀(proj R) ⟶ G₀(mod R).
• TauCeti.moduleResolutionEquiv: the resolution theorem in ModuleCat R, comparing K₀(proj R) with the Grothendieck group of the modules admitting finite resolutions by finitely generated projectives.
• TauCeti.fromFiniteProjectiveResolution and TauCeti.toFiniteProjectiveResolution: the two comparison maps between that group and G₀(mod R).
• TauCeti.moduleEulerClassOf and TauCeti.moduleEulerClass: the alternating class in K₀(proj R) determined by any finite resolution by finitely generated projectives, and the value at a particular resolution, evaluated by TauCeti.moduleEulerClass_base and TauCeti.moduleEulerClass_step.
• TauCeti.cartanInverse and TauCeti.cartanEquiv: the inverse of the Cartan map and the resulting isomorphism, under the hypothesis that every finitely generated module has a finite resolution by finitely generated projectives.

Main results

• TauCeti.finiteModulesExactStructure_conflation_iff and TauCeti.finiteProjectiveModulesExactStructure_conflation_iff, and TauCeti.finiteProjectiveResolutionExactStructure_conflation_iff: the conflations of the three structures are the short exact sequences of modules with terms in the subcategory.
• TauCeti.finiteProjectiveModulesExactStructure_eq_split: the exact structure of the finitely generated projectives is the split one.
• TauCeti.finiteModulesExactStructure_eq_abelian: over a noetherian ring, the exact structure of the finitely generated modules is the canonical one of the abelian category FGModuleCat R.
• TauCeti.finiteModulesExactK0Equiv: the explicit comparison between the named finite-module exact structure and the structure induced directly from all modules.
• TauCeti.exactK0_fgModuleCat_prod: in G₀(mod R), the class of a product of two finitely generated modules is the sum of their classes.
• TauCeti.exactK0_of_eq_range_add_range: in G₀(mod R), the class of the middle term of an exact pair is the sum of the classes of the two images.
• TauCeti.exactK0_add_add_eq_add_add_of_exact: along a six-term exact sequence of finitely generated modules, the odd-indexed and even-indexed classes have the same sum.
• CategoryTheory.Equivalence.isConflationExact_finiteModules_congrFullSubcategory_functor and its finiteProjectiveModules and _inverse companions: an exact equivalence of module categories respecting the two object properties restricts to exact equivalences of the two subcategories. These are dot notation on the equivalence.
• TauCeti.cartanMap_apply: the Cartan map factors through the Grothendieck group of the modules admitting finite resolutions by finitely generated projectives, by the resolution theorem.
• TauCeti.moduleEulerClassOf_eq: every finite projective resolution computes the module Euler class.
• TauCeti.cartanMap_bijective: the module form of the resolution theorem, and TauCeti.cartanMap_bijective_of_isSemisimpleRing for the semisimple-ring instance of its hypothesis.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Sections 6 and 7, for K₀(proj R), G₀(mod R) and the resolution theorem; Definition II.6.2 for G₀ of a noetherian ring, and Example II.7.1.4 and Exercise II.7.3 for G₀ of a general ring.
• Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3, for the Cartan map of a finite-dimensional algebra.

The finitely generated projectives

def TauCeti.finiteProjectiveModules (R : Type u) [Ring R] : CategoryTheory.ObjectProperty (ModuleCat R)

The object property of being a finitely generated projective module.

Equations

• TauCeti.finiteProjectiveModules R M = (Module.Finite R ↑M ∧ Module.Projective R ↑M)

@[simp]

theorem TauCeti.finiteProjectiveModules_iff {R : Type u} [Ring R] {M : ModuleCat R} : finiteProjectiveModules R M ↔ Module.Finite R ↑M ∧ Module.Projective R ↑M

instance TauCeti.instFiniteCarrierObjModuleCatFiniteProjectiveModules {R : Type u} [Ring R] (X : (finiteProjectiveModules R).FullSubcategory) : Module.Finite R ↑X.obj

The underlying module of an object of the subcategory of finitely generated projectives is finitely generated.

instance TauCeti.instProjectiveCarrierObjModuleCatFiniteProjectiveModules {R : Type u} [Ring R] (X : (finiteProjectiveModules R).FullSubcategory) : Module.Projective R ↑X.obj

The underlying module of an object of the subcategory of finitely generated projectives is projective.

theorem TauCeti.finiteProjectiveModules_le_finiteModules (R : Type u) [Ring R] : finiteProjectiveModules R ≤ ModuleCat.isFG R

instance TauCeti.instIsClosedUnderIsomorphismsModuleCatIsFG_tauCeti (R : Type u) [Ring R] : (ModuleCat.isFG R).IsClosedUnderIsomorphisms

instance TauCeti.instIsClosedUnderIsomorphismsModuleCatFiniteProjectiveModules (R : Type u) [Ring R] : (finiteProjectiveModules R).IsClosedUnderIsomorphisms

instance TauCeti.instContainsZeroModuleCatIsFG_tauCeti (R : Type u) [Ring R] : (ModuleCat.isFG R).ContainsZero

instance TauCeti.instContainsZeroModuleCatFiniteProjectiveModules (R : Type u) [Ring R] : (finiteProjectiveModules R).ContainsZero

Essential smallness

instance TauCeti.instEssentiallySmallModuleCatIsFG_tauCeti (R : Type u) [Ring R] : CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} (ModuleCat.isFG R)

instance TauCeti.instEssentiallySmallModuleCatFiniteProjectiveModules (R : Type u) [Ring R] : CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} (finiteProjectiveModules R)

The two exact structures

theorem TauCeti.isExtensionClosed_finiteModules (R : Type u) [Ring R] : (ExactStructure.abelian (ModuleCat R)).IsExtensionClosed (ModuleCat.isFG R)

The finitely generated modules are extension closed: the middle term of a short exact sequence with finitely generated ends is finitely generated.

theorem TauCeti.finiteProjectiveModules_le_isProjective (R : Type u) [Ring R] : finiteProjectiveModules R ≤ (ExactStructure.abelian (ModuleCat R)).isProjective

A finitely generated projective module is a projective object for the canonical exact structure of ModuleCat R.

instance TauCeti.instIsClosedUnderBinaryProductsModuleCatIsFG_tauCeti (R : Type u) [Ring R] : (ModuleCat.isFG R).IsClosedUnderBinaryProducts

instance TauCeti.instIsClosedUnderBinaryProductsModuleCatFiniteProjectiveModules (R : Type u) [Ring R] : (finiteProjectiveModules R).IsClosedUnderBinaryProducts

noncomputable def TauCeti.finiteModulesExactStructure (R : Type u) [Ring R] : ExactStructure (FGModuleCat R)

The exact structure of the finitely generated modules: the short exact sequences of R-modules all of whose terms are finitely generated.

Equations

• TauCeti.finiteModulesExactStructure R = TauCeti.ExactStructure.fullSubcategory (ModuleCat.isFG R) ⋯

noncomputable def TauCeti.finiteProjectiveModulesExactStructure (R : Type u) [Ring R] : ExactStructure (finiteProjectiveModules R).FullSubcategory

The exact structure of the finitely generated projective modules, induced from the canonical exact structure of ModuleCat R. It is the split one, by TauCeti.finiteProjectiveModulesExactStructure_eq_split.

Equations

• TauCeti.finiteProjectiveModulesExactStructure R = TauCeti.ExactStructure.fullSubcategory (TauCeti.finiteProjectiveModules R) ⋯

theorem TauCeti.finiteProjectiveModulesExactStructure_eq_split (R : Type u) [Ring R] : finiteProjectiveModulesExactStructure R = ExactStructure.split (finiteProjectiveModules R).FullSubcategory

The exact structure of the finitely generated projectives is the split one: a short exact sequence of modules whose quotient is projective splits, so the induced exact structure has exactly the split conflations.

@[simp]

theorem TauCeti.finiteModulesExactStructure_conflation_iff (R : Type u) [Ring R] (S : CategoryTheory.ShortComplex (FGModuleCat R)) : (finiteModulesExactStructure R).Conflation S ↔ (S.map (ModuleCat.isFG R).ι).ShortExact

The conflations of finitely generated modules are the short exact sequences of R-modules whose three terms are finitely generated.

theorem TauCeti.finiteModulesExactStructure_eq_abelian (R : Type u) [Ring R] [IsNoetherianRing R] : finiteModulesExactStructure R = ExactStructure.abelian (FGModuleCat R)

Over a noetherian ring, the finitely generated modules carry their abelian exact structure: the exact structure induced from all modules is the canonical exact structure of the abelian category FGModuleCat R, because the inclusion into ModuleCat R is exact and faithful.

noncomputable def TauCeti.finiteModulesExactK0Equiv (R : Type u) [Ring R] : ExactK0 (finiteModulesExactStructure R) ≃+ ExactK0 (ExactStructure.fullSubcategory (ModuleCat.isFG R) ⋯)

The exact Grothendieck group defined using finiteModulesExactStructure agrees with the one defined directly from the exact structure induced from all modules. This explicit bridge keeps the implementation of finiteModulesExactStructure opaque.

Equations

• TauCeti.finiteModulesExactK0Equiv R = TauCeti.ExactK0.ofLEEquiv ⋯

@[simp]

theorem TauCeti.finiteModulesExactK0Equiv_of (R : Type u) [Ring R] (X : FGModuleCat R) : (finiteModulesExactK0Equiv R) (ExactK0.of X) = ExactK0.of X

@[simp]

theorem TauCeti.exactK0_fgModuleCat_prod (R : Type u) [Ring R] (M N : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module.Finite R N] : ExactK0.of ↧(M × N) = ExactK0.of ↧M + ExactK0.of ↧N

The class of a product of finitely generated modules is the sum of the classes: the product M × N is the biproduct of M and N in the category of finitely generated modules.

theorem TauCeti.exactK0_of_eq_range_add_range (R : Type u) [Ring R] {M N P : Type u} [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module.Finite R N] [AddCommGroup P] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) : ExactK0.of ↧N = ExactK0.of ↧↥f.range + ExactK0.of ↧↥g.range

The class of the middle term of an exact pair. If M → N → P is exact at N, with M and N finitely generated, then [N] is the sum of the classes of the images of the two maps in G₀(mod R): 0 → range f → N → range g → 0 is a short exact sequence of finitely generated modules. Telescoping this along a longer exact sequence with zero ends makes its alternating sum of classes vanish.

theorem TauCeti.exactK0_of_range_of_injective (R : Type u) [Ring R] {M N : Type u} [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) : ExactK0.of ↧↥f.range = ExactK0.of ↧M

The image of an injective linear map out of a finitely generated module has the class of its source in G₀(mod R).

theorem TauCeti.exactK0_of_range_of_surjective (R : Type u) [Ring R] {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f) : ExactK0.of ↧↥f.range = ExactK0.of ↧N

The image of a surjective linear map onto a finitely generated module has the class of its target in G₀(mod R).

theorem TauCeti.exactK0_add_add_eq_add_add_of_exact (R : Type u) [Ring R] {M₁ M₂ M₃ M₄ M₅ M₆ : Type u} [AddCommGroup M₁] [Module R M₁] [Module.Finite R M₁] [AddCommGroup M₂] [Module R M₂] [Module.Finite R M₂] [AddCommGroup M₃] [Module R M₃] [Module.Finite R M₃] [AddCommGroup M₄] [Module R M₄] [Module.Finite R M₄] [AddCommGroup M₅] [Module R M₅] [Module.Finite R M₅] [AddCommGroup M₆] [Module R M₆] [Module.Finite R M₆] {f₁ : M₁ →ₗ[R] M₂} {f₂ : M₂ →ₗ[R] M₃} {f₃ : M₃ →ₗ[R] M₄} {f₄ : M₄ →ₗ[R] M₅} {f₅ : M₅ →ₗ[R] M₆} (h₁ : Function.Injective ⇑f₁) (h₁₂ : Function.Exact ⇑f₁ ⇑f₂) (h₂₃ : Function.Exact ⇑f₂ ⇑f₃) (h₃₄ : Function.Exact ⇑f₃ ⇑f₄) (h₄₅ : Function.Exact ⇑f₄ ⇑f₅) (h₅ : Function.Surjective ⇑f₅) : ExactK0.of ↧M₁ + ExactK0.of ↧M₃ + ExactK0.of ↧M₅ = ExactK0.of ↧M₂ + ExactK0.of ↧M₄ + ExactK0.of ↧M₆

The Euler relation of a six-term exact sequence. For an exact sequence 0 → M₁ → M₂ → M₃ → M₄ → M₅ → M₆ → 0 of finitely generated modules, the classes of the odd-indexed terms and of the even-indexed terms have the same sum in G₀(mod R). This is the six-term case of Euler–Poincaré (TauCeti.ExactK0.sum_negOnePow_of_X_eq_sum_negOnePow_of_homology), stated for linear maps between finitely generated modules rather than for a cochain complex of modules whose boundaries and cohomology are finitely generated.

@[simp]

theorem TauCeti.finiteProjectiveModulesExactStructure_conflation_iff (R : Type u) [Ring R] (S : CategoryTheory.ShortComplex (finiteProjectiveModules R).FullSubcategory) : (finiteProjectiveModulesExactStructure R).Conflation S ↔ (S.map (finiteProjectiveModules R).ι).ShortExact

The conflations of finitely generated projective modules are the short exact sequences of R-modules whose three terms are finitely generated projective; by TauCeti.finiteProjectiveModulesExactStructure_eq_split these are exactly the split ones.

The Cartan map

noncomputable def TauCeti.cartanMap (R : Type u) [Ring R] : ExactK0 (finiteProjectiveModulesExactStructure R) →+ ExactK0 (finiteModulesExactStructure R)

The Cartan map c_R : K₀(proj R) ⟶ G₀(mod R), induced by the inclusion of the finitely generated projective modules into the finitely generated modules. The inclusion is conflation-exact because a split short exact sequence of modules is a short exact sequence.

Equations

• TauCeti.cartanMap R = TauCeti.ExactK0.map (CategoryTheory.ObjectProperty.ιOfLE ⋯) ⋯

@[simp]

theorem TauCeti.cartanMap_of (R : Type u) [Ring R] {M : ModuleCat R} (hM : finiteProjectiveModules R M) : (cartanMap R) (ExactK0.of { obj := M, property := hM }) = ExactK0.of { obj := M, property := ⋯ }

Transport along exact equivalences

theorem CategoryTheory.Equivalence.isConflationExact_finiteModules_congrFullSubcategory_functor {S : Type u} [Ring S] {R : Type u'} [Ring R] (e : ModuleCat S ≌ ModuleCat R) [e.functor.Additive] (hF : (TauCeti.ExactStructure.abelian (ModuleCat S)).IsConflationExact (TauCeti.ExactStructure.abelian (ModuleCat R)) e.functor) (h : (ModuleCat.isFG R).inverseImage e.functor = ModuleCat.isFG S) : (TauCeti.finiteModulesExactStructure S).IsConflationExact (TauCeti.finiteModulesExactStructure R) (e.congrFullSubcategory h).functor

An exact equivalence of module categories pulling the finitely generated R-modules back to the finitely generated S-modules restricts to a conflation-exact functor between the finitely generated modules.

theorem CategoryTheory.Equivalence.isConflationExact_finiteModules_congrFullSubcategory_inverse {S : Type u} [Ring S] {R : Type u'} [Ring R] (e : ModuleCat S ≌ ModuleCat R) [e.functor.Additive] (hG : (TauCeti.ExactStructure.abelian (ModuleCat R)).IsConflationExact (TauCeti.ExactStructure.abelian (ModuleCat S)) e.inverse) (h : (ModuleCat.isFG R).inverseImage e.functor = ModuleCat.isFG S) : (TauCeti.finiteModulesExactStructure R).IsConflationExact (TauCeti.finiteModulesExactStructure S) (e.congrFullSubcategory h).inverse

The inverse of an exact equivalence of module categories pulling the finitely generated R-modules back to the finitely generated S-modules restricts to a conflation-exact functor between the finitely generated modules.

theorem CategoryTheory.Equivalence.isConflationExact_finiteProjectiveModules_congrFullSubcategory_functor {S : Type u} [Ring S] {R : Type u'} [Ring R] (e : ModuleCat S ≌ ModuleCat R) [e.functor.Additive] (hF : (TauCeti.ExactStructure.abelian (ModuleCat S)).IsConflationExact (TauCeti.ExactStructure.abelian (ModuleCat R)) e.functor) (h : (TauCeti.finiteProjectiveModules R).inverseImage e.functor = TauCeti.finiteProjectiveModules S) : (TauCeti.finiteProjectiveModulesExactStructure S).IsConflationExact (TauCeti.finiteProjectiveModulesExactStructure R) (e.congrFullSubcategory h).functor

An exact equivalence of module categories pulling the finitely generated projective R-modules back to the finitely generated projective S-modules restricts to a conflation-exact functor between the finitely generated projective modules.

theorem CategoryTheory.Equivalence.isConflationExact_finiteProjectiveModules_congrFullSubcategory_inverse {S : Type u} [Ring S] {R : Type u'} [Ring R] (e : ModuleCat S ≌ ModuleCat R) [e.functor.Additive] (hG : (TauCeti.ExactStructure.abelian (ModuleCat R)).IsConflationExact (TauCeti.ExactStructure.abelian (ModuleCat S)) e.inverse) (h : (TauCeti.finiteProjectiveModules R).inverseImage e.functor = TauCeti.finiteProjectiveModules S) : (TauCeti.finiteProjectiveModulesExactStructure R).IsConflationExact (TauCeti.finiteProjectiveModulesExactStructure S) (e.congrFullSubcategory h).inverse

The inverse of an exact equivalence of module categories pulling the finitely generated projective R-modules back to the finitely generated projective S-modules restricts to a conflation-exact functor between the finitely generated projective modules.

The resolution theorem

theorem TauCeti.admitsFiniteResolution_le_finiteModules (R : Type u) [Ring R] : (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R) ≤ ModuleCat.isFG R

A module admitting a finite resolution by finitely generated projectives is itself finitely generated: each step of the resolution presents it as a quotient of a finitely generated module.

instance TauCeti.instEssentiallySmallModuleCatAdmitsFiniteResolutionAbelianFiniteProjectiveModules (R : Type u) [Ring R] : CategoryTheory.ObjectProperty.EssentiallySmall.{u, u, u + 1} ((ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R))

noncomputable def TauCeti.finiteProjectiveResolutionExactStructure (R : Type u) [Ring R] : ExactStructure ((ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)).FullSubcategory

The exact structure of the modules admitting finite resolutions by finitely generated projectives: the short exact sequences of R-modules all of whose terms admit such a resolution.

Equations

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

@[simp]

theorem TauCeti.finiteProjectiveResolutionExactStructure_conflation_iff (R : Type u) [Ring R] (S : CategoryTheory.ShortComplex ((ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)).FullSubcategory) : (finiteProjectiveResolutionExactStructure R).Conflation S ↔ (S.map ((ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)).ι).ShortExact

The conflations of modules admitting finite resolutions by finitely generated projectives are the short exact sequences of modules whose three terms admit such resolutions.

noncomputable def TauCeti.moduleResolutionEquiv (R : Type u) [Ring R] : ExactK0 (finiteProjectiveModulesExactStructure R) ≃+ ExactK0 (finiteProjectiveResolutionExactStructure R)

The resolution theorem for modules admitting finite resolutions by finitely generated projectives: their exact K₀ is the exact K₀ of the finitely generated projective modules. This is TauCeti.ExactStructure.resolutionEquiv in ModuleCat R; its inverse sends the class of a module to the alternating class of any such resolution.

Equations

• TauCeti.moduleResolutionEquiv R = TauCeti.ExactStructure.resolutionEquiv ⋯

@[simp]

theorem TauCeti.moduleResolutionEquiv_of (R : Type u) [Ring R] {M : ModuleCat R} (hM : finiteProjectiveModules R M) : (moduleResolutionEquiv R) (ExactK0.of { obj := M, property := hM }) = ExactK0.of { obj := M, property := ⋯ }

noncomputable def TauCeti.moduleEulerClassOf (R : Type u) [Ring R] {M : ModuleCat R} (hM : (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R) M) : ExactK0 (finiteProjectiveModulesExactStructure R)

The alternating class of a finite projective resolution, as an element of K₀(proj R): TauCeti.ExactStructure.eulerClassOf for the finitely generated projective modules. Any finite resolution of M by finitely generated projectives computes it, by TauCeti.ExactStructure.eulerClassOf_eq.

Equations

• TauCeti.moduleEulerClassOf R hM = TauCeti.ExactStructure.eulerClassOf ⋯ hM

noncomputable def TauCeti.moduleEulerClass (R : Type u) [Ring R] {M : ModuleCat R} (r : (ExactStructure.abelian (ModuleCat R)).FiniteResolution (finiteProjectiveModules R) M) : ExactK0 (finiteProjectiveModulesExactStructure R)

The alternating class of a particular finite resolution by finitely generated projectives, as an element of K₀(proj R). It is evaluated on both constructors of a resolution by TauCeti.moduleEulerClass_base and TauCeti.moduleEulerClass_step.

Equations

• TauCeti.moduleEulerClass R r = TauCeti.ExactStructure.FiniteResolution.eulerClassFullSubcategory ⋯ r

@[simp]

theorem TauCeti.moduleEulerClass_base (R : Type u) [Ring R] {M : ModuleCat R} (hM : finiteProjectiveModules R M) : moduleEulerClass R (ExactStructure.FiniteResolution.base hM) = ExactK0.of { obj := M, property := hM }

The alternating class of the resolution of a finitely generated projective module by itself is the class of that module.

@[simp]

theorem TauCeti.moduleEulerClass_step (R : Type u) [Ring R] {K Q M : ModuleCat R} (hQ : finiteProjectiveModules R Q) (i : K ⟶ Q) (p : Q ⟶ M) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : (ExactStructure.abelian (ModuleCat R)).Conflation { X₁ := K, X₂ := Q, X₃ := M, f := i, g := p, zero := zero }) (r : (ExactStructure.abelian (ModuleCat R)).FiniteResolution (finiteProjectiveModules R) K) : moduleEulerClass R (ExactStructure.FiniteResolution.step hQ i p zero hp r) = ExactK0.of { obj := Q, property := hQ } - moduleEulerClass R r

Prepending a resolving term to a finite resolution subtracts the remaining alternating class from the class of that term.

theorem TauCeti.moduleEulerClassOf_eq (R : Type u) [Ring R] {M : ModuleCat R} (hM : (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R) M) (r : (ExactStructure.abelian (ModuleCat R)).FiniteResolution (finiteProjectiveModules R) M) : moduleEulerClassOf R hM = moduleEulerClass R r

Every finite resolution of a module by finitely generated projectives computes its alternating class.

@[simp]

theorem TauCeti.moduleEulerClassOf_of_prop (R : Type u) [Ring R] {M : ModuleCat R} (hM : Module.Finite R ↑M ∧ Module.Projective R ↑M) : moduleEulerClassOf R ⋯ = ExactK0.of { obj := M, property := ⋯ }

A finitely generated projective module is its own resolution, so its alternating class is its own class.

@[simp]

theorem TauCeti.moduleResolutionEquiv_symm_of (R : Type u) [Ring R] {M : ModuleCat R} (hM : (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R) M) : (moduleResolutionEquiv R).symm (ExactK0.of { obj := M, property := hM }) = moduleEulerClassOf R hM

noncomputable def TauCeti.fromFiniteProjectiveResolution (R : Type u) [Ring R] : ExactK0 (finiteProjectiveResolutionExactStructure R) →+ ExactK0 (finiteModulesExactStructure R)

The comparison map from the Grothendieck group of the modules admitting finite resolutions by finitely generated projectives to G₀(mod R).

Equations

• TauCeti.fromFiniteProjectiveResolution R = TauCeti.ExactK0.map (CategoryTheory.ObjectProperty.ιOfLE ⋯) ⋯

@[simp]

theorem TauCeti.fromFiniteProjectiveResolution_of (R : Type u) [Ring R] {M : ModuleCat R} (hM : (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R) M) : (fromFiniteProjectiveResolution R) (ExactK0.of { obj := M, property := hM }) = ExactK0.of { obj := M, property := ⋯ }

theorem TauCeti.cartanMap_apply (R : Type u) [Ring R] (x : ExactK0 (finiteProjectiveModulesExactStructure R)) : (cartanMap R) x = (fromFiniteProjectiveResolution R) ((moduleResolutionEquiv R) x)

The Cartan map factors through the modules admitting finite resolutions by finitely generated projectives, where the resolution theorem TauCeti.moduleResolutionEquiv has already made it an isomorphism. All that is left of the Cartan map is therefore the comparison of these modules with all finitely generated modules.

noncomputable def TauCeti.toFiniteProjectiveResolution (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : ExactK0 (finiteModulesExactStructure R) →+ ExactK0 (finiteProjectiveResolutionExactStructure R)

Under the hypothesis that every finitely generated module admits a finite resolution by finitely generated projectives, the comparison map from G₀(mod R) to the Grothendieck group of the modules admitting such resolutions.

Equations

• TauCeti.toFiniteProjectiveResolution R h = TauCeti.ExactK0.map (CategoryTheory.ObjectProperty.ιOfLE h) ⋯

@[simp]

theorem TauCeti.toFiniteProjectiveResolution_of (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) {M : ModuleCat R} (hM : ModuleCat.isFG R M) : (toFiniteProjectiveResolution R h) (ExactK0.of { obj := M, property := hM }) = ExactK0.of { obj := M, property := ⋯ }

@[simp]

theorem TauCeti.fromFiniteProjectiveResolution_toFiniteProjectiveResolution (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) (y : ExactK0 (finiteModulesExactStructure R)) : (fromFiniteProjectiveResolution R) ((toFiniteProjectiveResolution R h) y) = y

fromFiniteProjectiveResolution is a left inverse of toFiniteProjectiveResolution, since under the hypothesis the two object properties agree. The other composite is toFiniteProjectiveResolution_fromFiniteProjectiveResolution.

@[simp]

theorem TauCeti.toFiniteProjectiveResolution_fromFiniteProjectiveResolution (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) (y : ExactK0 (finiteProjectiveResolutionExactStructure R)) : (toFiniteProjectiveResolution R h) ((fromFiniteProjectiveResolution R) y) = y

noncomputable def TauCeti.cartanInverse (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : ExactK0 (finiteModulesExactStructure R) →+ ExactK0 (finiteProjectiveModulesExactStructure R)

The inverse of the Cartan map, under the hypothesis that every finitely generated module admits a finite resolution by finitely generated projectives: the class of a module is sent to the alternating class of any such resolution.

Equations

• TauCeti.cartanInverse R h = (TauCeti.moduleResolutionEquiv R).symm.toAddMonoidHom.comp (TauCeti.toFiniteProjectiveResolution R h)

@[simp]

theorem TauCeti.cartanInverse_of (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) {M : ModuleCat R} (hM : ModuleCat.isFG R M) : (cartanInverse R h) (ExactK0.of { obj := M, property := hM }) = moduleEulerClassOf R ⋯

noncomputable def TauCeti.cartanEquiv (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : ExactK0 (finiteProjectiveModulesExactStructure R) ≃+ ExactK0 (finiteModulesExactStructure R)

The resolution theorem for modules. If every finitely generated R-module admits a finite resolution by finitely generated projective modules, then the Cartan map K₀(proj R) ⟶ G₀(mod R) is an isomorphism; its inverse sends the class of a module to the alternating class of any such resolution.

Equations

• TauCeti.cartanEquiv R h = { toFun := ⇑(TauCeti.cartanMap R), invFun := ⇑(TauCeti.cartanInverse R h), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.cartanEquiv_apply (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) (x : ExactK0 (finiteProjectiveModulesExactStructure R)) : (cartanEquiv R h) x = (cartanMap R) x

@[simp]

theorem TauCeti.cartanEquiv_symm_apply (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) (x : ExactK0 (finiteModulesExactStructure R)) : (cartanEquiv R h).symm x = (cartanInverse R h) x

The inverse of the Cartan equivalence is the alternating-resolution homomorphism.

theorem TauCeti.cartanMap_bijective (R : Type u) [Ring R] (h : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)) : Function.Bijective ⇑(cartanMap R)

The Cartan map is an isomorphism whenever every finitely generated R-module admits a finite resolution by finitely generated projective modules; this is the bijectivity statement of TauCeti.cartanEquiv.

The semisimple case

theorem TauCeti.finiteModules_le_finiteProjectiveModules (R : Type u) [Ring R] [IsSemisimpleRing R] : ModuleCat.isFG R ≤ finiteProjectiveModules R

Over a semisimple ring every module is projective, so every finitely generated module is a finitely generated projective module.

theorem TauCeti.finiteModules_le_admitsFiniteResolution (R : Type u) [Ring R] [IsSemisimpleRing R] : ModuleCat.isFG R ≤ (ExactStructure.abelian (ModuleCat R)).admitsFiniteResolution (finiteProjectiveModules R)

Over a semisimple ring every finitely generated module is its own finite projective resolution, so the hypothesis of the resolution theorem holds.

noncomputable def TauCeti.cartanEquivOfIsSemisimpleRing (R : Type u) [Ring R] [IsSemisimpleRing R] : ExactK0 (finiteProjectiveModulesExactStructure R) ≃+ ExactK0 (finiteModulesExactStructure R)

The Cartan map of a semisimple ring is an isomorphism, because every finitely generated module is already projective.

Equations

• TauCeti.cartanEquivOfIsSemisimpleRing R = TauCeti.cartanEquiv R ⋯

@[simp]

theorem TauCeti.cartanEquivOfIsSemisimpleRing_apply (R : Type u) [Ring R] [IsSemisimpleRing R] (x : ExactK0 (finiteProjectiveModulesExactStructure R)) : (cartanEquivOfIsSemisimpleRing R) x = (cartanMap R) x

@[simp]

theorem TauCeti.cartanEquivOfIsSemisimpleRing_symm_apply (R : Type u) [Ring R] [IsSemisimpleRing R] (x : ExactK0 (finiteModulesExactStructure R)) : (cartanEquivOfIsSemisimpleRing R).symm x = (cartanInverse R ⋯) x

The inverse of the semisimple Cartan equivalence is the alternating-resolution map.

theorem TauCeti.cartanMap_bijective_of_isSemisimpleRing (R : Type u) [Ring R] [IsSemisimpleRing R] : Function.Bijective ⇑(cartanMap R)

The Cartan map of a semisimple ring is bijective, with no finite-resolution hypothesis: over a semisimple ring every finitely generated module is projective, hence its own finite projective resolution.