Morita invariance of K₀(proj A), G₀(mod A) and the Cartan map

An equivalence of categories e : ModuleCat A ≌ ModuleCat B between the module categories of two rings -- for instance the underlying equivalence of a Morita equivalence -- preserves and reflects finite generation and projectivity, and it is exact. It therefore restricts to exact equivalences between the finitely generated modules and between the finitely generated projective modules over the two rings, and on Grothendieck groups it induces isomorphisms

K₀(proj A) ≃ K₀(proj B),   G₀(mod A) ≃ G₀(mod B),

both sending the class of a module M to the class of e.functor.obj M. The square they form with the two Cartan maps commutes, so the Cartan map of A is an isomorphism if and only if that of B is. In particular, for Morita equivalent algebras A and B in Mathlib's sense (IsMoritaEquivalent R A B), the groups K₀(proj A) and G₀(mod A) and the bijectivity of the Cartan map are Morita invariants.

The special case of the equivalence induced by a ring isomorphism is TauCeti/Algebra/Category/ModuleCat/CartanMap/RingEquiv.lean, where the induced maps are described through restriction of scalars.

The API is dot notation on the equivalence: use e.finiteModulesK0Equiv, e.finiteProjectiveModulesK0Equiv and e.cartanMap_bijective_iff. The two rings may live in different universes; only the Morita corollaries put them in one, as Mathlib's MoritaEquivalence does.

Main definitions

• CategoryTheory.Equivalence.finiteModulesEquivalence and CategoryTheory.Equivalence.finiteProjectiveModulesEquivalence: the restrictions of an equivalence of module categories to the finitely generated, respectively finitely generated projective, modules over the two rings.
• CategoryTheory.Equivalence.finiteModulesK0Equiv and CategoryTheory.Equivalence.finiteProjectiveModulesK0Equiv: the induced isomorphisms G₀(mod A) ≃+ G₀(mod B) and K₀(proj A) ≃+ K₀(proj B).

Main results

• CategoryTheory.Equivalence.finiteProjectiveModules_inverseImage: an equivalence of module categories pulls the finitely generated projective modules back to the finitely generated projective modules.
• CategoryTheory.Equivalence.cartanMap_comp_finiteProjectiveModulesK0Equiv and CategoryTheory.Equivalence.cartanMap_finiteProjectiveModulesK0Equiv: the Cartan maps of A and B commute with the two induced isomorphisms.
• CategoryTheory.Equivalence.cartanMap_bijective_iff: the Cartan map of A is bijective if and only if the Cartan map of B is.
• IsMoritaEquivalent.nonempty_finiteProjectiveModulesK0Equiv, IsMoritaEquivalent.nonempty_finiteModulesK0Equiv and IsMoritaEquivalent.cartanMap_bijective_iff: the same statements for Morita equivalent algebras.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 2, for the Morita invariance of K₀ of a ring.

The two object properties

@[simp]

theorem CategoryTheory.Equivalence.finiteProjectiveModules_inverseImage {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (TauCeti.finiteProjectiveModules B).inverseImage e.functor = TauCeti.finiteProjectiveModules A

An equivalence of module categories pulls the finitely generated projective B-modules back to the finitely generated projective A-modules.

The equivalences of module subcategories

noncomputable def CategoryTheory.Equivalence.finiteModulesEquivalence {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : FGModuleCat A ≌ FGModuleCat B

Finitely generated modules along an equivalence of module categories. An equivalence e : ModuleCat A ≌ ModuleCat B restricts to an equivalence from the finitely generated A-modules to the finitely generated B-modules.

Equations

• e.finiteModulesEquivalence = e.congrFullSubcategory ⋯

noncomputable def CategoryTheory.Equivalence.finiteProjectiveModulesEquivalence {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (TauCeti.finiteProjectiveModules A).FullSubcategory ≌ (TauCeti.finiteProjectiveModules B).FullSubcategory

Finitely generated projective modules along an equivalence of module categories. An equivalence e : ModuleCat A ≌ ModuleCat B restricts to an equivalence from the finitely generated projective A-modules to the finitely generated projective B-modules.

Equations

• e.finiteProjectiveModulesEquivalence = e.congrFullSubcategory ⋯

instance CategoryTheory.Equivalence.instAdditiveFGModuleCatFunctorFiniteModulesEquivalence {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : e.finiteModulesEquivalence.functor.Additive

instance CategoryTheory.Equivalence.instAdditiveFullSubcategoryModuleCatFiniteProjectiveModulesFunctorFiniteProjectiveModulesEquivalence {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : e.finiteProjectiveModulesEquivalence.functor.Additive

@[simp]

theorem CategoryTheory.Equivalence.finiteModulesEquivalence_functor_obj_obj {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : FGModuleCat A) : (e.finiteModulesEquivalence.functor.obj M).obj = e.functor.obj M.obj

@[simp]

theorem CategoryTheory.Equivalence.finiteModulesEquivalence_functor_map_hom {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) {M N : FGModuleCat A} (f : M ⟶ N) : (e.finiteModulesEquivalence.functor.map f).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (e.functor.map f.hom) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Equivalence.finiteModulesEquivalence_inverse_obj_obj {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : FGModuleCat B) : (e.finiteModulesEquivalence.inverse.obj M).obj = e.inverse.obj M.obj

@[simp]

theorem CategoryTheory.Equivalence.finiteModulesEquivalence_inverse_map_hom {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) {M N : FGModuleCat B} (f : M ⟶ N) : (e.finiteModulesEquivalence.inverse.map f).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (e.inverse.map f.hom) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Equivalence.finiteProjectiveModulesEquivalence_functor_obj_obj {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : (TauCeti.finiteProjectiveModules A).FullSubcategory) : (e.finiteProjectiveModulesEquivalence.functor.obj M).obj = e.functor.obj M.obj

@[simp]

theorem CategoryTheory.Equivalence.finiteProjectiveModulesEquivalence_functor_map_hom {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) {M N : (TauCeti.finiteProjectiveModules A).FullSubcategory} (f : M ⟶ N) : (e.finiteProjectiveModulesEquivalence.functor.map f).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (e.functor.map f.hom) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Equivalence.finiteProjectiveModulesEquivalence_inverse_obj_obj {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : (TauCeti.finiteProjectiveModules B).FullSubcategory) : (e.finiteProjectiveModulesEquivalence.inverse.obj M).obj = e.inverse.obj M.obj

@[simp]

theorem CategoryTheory.Equivalence.finiteProjectiveModulesEquivalence_inverse_map_hom {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) {M N : (TauCeti.finiteProjectiveModules B).FullSubcategory} (f : M ⟶ N) : (e.finiteProjectiveModulesEquivalence.inverse.map f).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (e.inverse.map f.hom) (eqToHom ⋯))

Exactness of the restricted equivalences

theorem CategoryTheory.Equivalence.isConflationExact_finiteModulesEquivalence_functor {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (TauCeti.finiteModulesExactStructure A).IsConflationExact (TauCeti.finiteModulesExactStructure B) e.finiteModulesEquivalence.functor

The restriction of an equivalence of module categories to the finitely generated modules is conflation-exact.

theorem CategoryTheory.Equivalence.isConflationExact_finiteModulesEquivalence_inverse {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (TauCeti.finiteModulesExactStructure B).IsConflationExact (TauCeti.finiteModulesExactStructure A) e.finiteModulesEquivalence.inverse

The inverse of the restriction of an equivalence of module categories to the finitely generated modules is conflation-exact.

theorem CategoryTheory.Equivalence.isConflationExact_finiteProjectiveModulesEquivalence_functor {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (TauCeti.finiteProjectiveModulesExactStructure A).IsConflationExact (TauCeti.finiteProjectiveModulesExactStructure B) e.finiteProjectiveModulesEquivalence.functor

The restriction of an equivalence of module categories to the finitely generated projective modules is conflation-exact.

theorem CategoryTheory.Equivalence.isConflationExact_finiteProjectiveModulesEquivalence_inverse {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (TauCeti.finiteProjectiveModulesExactStructure B).IsConflationExact (TauCeti.finiteProjectiveModulesExactStructure A) e.finiteProjectiveModulesEquivalence.inverse

The inverse of the restriction of an equivalence of module categories to the finitely generated projective modules is conflation-exact.

The induced isomorphisms of Grothendieck groups

noncomputable def CategoryTheory.Equivalence.finiteModulesK0Equiv {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure A) ≃+ TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure B)

Morita invariance of G₀(mod A). An equivalence e : ModuleCat A ≌ ModuleCat B induces G₀(mod A) ≃+ G₀(mod B), sending the class of a finitely generated A-module M to the class of e.functor.obj M.

Equations

• e.finiteModulesK0Equiv = TauCeti.ExactK0.mapEquiv e.finiteModulesEquivalence ⋯ ⋯

noncomputable def CategoryTheory.Equivalence.finiteProjectiveModulesK0Equiv {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure A) ≃+ TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure B)

Morita invariance of K₀(proj A). An equivalence e : ModuleCat A ≌ ModuleCat B induces K₀(proj A) ≃+ K₀(proj B), sending the class of a finitely generated projective A-module M to the class of e.functor.obj M.

Equations

• e.finiteProjectiveModulesK0Equiv = TauCeti.ExactK0.mapEquiv e.finiteProjectiveModulesEquivalence ⋯ ⋯

@[simp]

theorem CategoryTheory.Equivalence.finiteModulesK0Equiv_of {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : FGModuleCat A) : e.finiteModulesK0Equiv (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteModulesEquivalence.functor.obj M)

@[simp]

theorem CategoryTheory.Equivalence.finiteModulesK0Equiv_symm_of {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : FGModuleCat B) : e.finiteModulesK0Equiv.symm (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteModulesEquivalence.inverse.obj M)

@[simp]

theorem CategoryTheory.Equivalence.finiteProjectiveModulesK0Equiv_of {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : (TauCeti.finiteProjectiveModules A).FullSubcategory) : e.finiteProjectiveModulesK0Equiv (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteProjectiveModulesEquivalence.functor.obj M)

@[simp]

theorem CategoryTheory.Equivalence.finiteProjectiveModulesK0Equiv_symm_of {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : (TauCeti.finiteProjectiveModules B).FullSubcategory) : e.finiteProjectiveModulesK0Equiv.symm (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteProjectiveModulesEquivalence.inverse.obj M)

Compatibility with the Cartan map

theorem CategoryTheory.Equivalence.cartanMap_comp_finiteProjectiveModulesK0Equiv {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (TauCeti.cartanMap B).comp e.finiteProjectiveModulesK0Equiv.toAddMonoidHom = e.finiteModulesK0Equiv.toAddMonoidHom.comp (TauCeti.cartanMap A)

Morita naturality of the Cartan map. The Cartan maps of two rings with equivalent module categories are intertwined by the induced isomorphisms of Grothendieck groups.

@[simp]

theorem CategoryTheory.Equivalence.cartanMap_finiteProjectiveModulesK0Equiv {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (x : TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure A)) : (TauCeti.cartanMap B) (e.finiteProjectiveModulesK0Equiv x) = e.finiteModulesK0Equiv ((TauCeti.cartanMap A) x)

Pointwise form of CategoryTheory.Equivalence.cartanMap_comp_finiteProjectiveModulesK0Equiv: applying the Cartan map of B after transporting a class from K₀(proj A) along e agrees with transporting its image under the Cartan map of A from G₀(mod A) along e.

theorem CategoryTheory.Equivalence.cartanMap_bijective_iff {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : Function.Bijective ⇑(TauCeti.cartanMap A) ↔ Function.Bijective ⇑(TauCeti.cartanMap B)

The resolution-theorem hypothesis is a Morita invariant: for rings with equivalent module categories, the Cartan map of A is bijective if and only if the Cartan map of B is.

Morita equivalent algebras

theorem IsMoritaEquivalent.nonempty_finiteProjectiveModulesK0Equiv {R : Type u₀} [CommSemiring R] {A B : Type u} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (h : IsMoritaEquivalent R A B) : Nonempty (TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure A) ≃+ TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure B))

K₀(proj A) is a Morita invariant: Morita equivalent algebras have isomorphic Grothendieck groups of finitely generated projective modules.

theorem IsMoritaEquivalent.nonempty_finiteModulesK0Equiv {R : Type u₀} [CommSemiring R] {A B : Type u} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (h : IsMoritaEquivalent R A B) : Nonempty (TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure A) ≃+ TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure B))

G₀(mod A) is a Morita invariant: Morita equivalent algebras have isomorphic Grothendieck groups of finitely generated modules.

theorem IsMoritaEquivalent.cartanMap_bijective_iff {R : Type u₀} [CommSemiring R] {A B : Type u} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (h : IsMoritaEquivalent R A B) : Function.Bijective ⇑(TauCeti.cartanMap A) ↔ Function.Bijective ⇑(TauCeti.cartanMap B)

Bijectivity of the Cartan map is a Morita invariant: for Morita equivalent algebras, the Cartan map of A is bijective if and only if the Cartan map of B is.