Invariance of K₀(proj R), G₀(mod R) and the Cartan map under ring isomorphisms

A ring isomorphism e : R ≃+* S induces, by restriction of scalars, an equivalence of module categories ModuleCat S ≌ ModuleCat R. It preserves and reflects finite generation and projectivity, and it is exact, so it restricts to exact equivalences between the finitely generated modules and between the finitely generated projective modules over the two rings. On Grothendieck groups this gives isomorphisms

K₀(proj S) ≃ K₀(proj R),   G₀(mod S) ≃ G₀(mod R),

both sending the class of a module to the class of the same module with scalars restricted along e, and the square they form with the two Cartan maps commutes. In particular the Cartan map of R is an isomorphism if and only if that of S is.

For an algebra isomorphism e : A ≃ₐ[k] B the statements apply to e.toRingEquiv, so K₀(proj A), G₀(mod A) and the Cartan map are invariants of the isomorphism class of the algebra A.

The API is dot notation on the ring isomorphism: use e.finiteModulesK0Equiv, e.finiteProjectiveModulesK0Equiv and e.cartanMap_bijective_iff.

Main definitions

• RingEquiv.finiteModulesEquivalence and RingEquiv.finiteProjectiveModulesEquivalence: restriction of scalars along a ring isomorphism, as equivalences between the finitely generated, respectively finitely generated projective, modules over the two rings.
• RingEquiv.finiteModulesK0Equiv and RingEquiv.finiteProjectiveModulesK0Equiv: the induced isomorphisms G₀(mod S) ≃+ G₀(mod R) and K₀(proj S) ≃+ K₀(proj R).

Main results

• RingEquiv.isFG_inverseImage_restrictScalars and RingEquiv.finiteProjectiveModules_inverseImage_restrictScalars: restriction of scalars along a ring isomorphism pulls the two object properties back to each other.
• RingEquiv.finiteModulesK0Equiv_refl, RingEquiv.finiteModulesK0Equiv_symm and RingEquiv.finiteModulesK0Equiv_trans, with their finiteProjectiveModulesK0Equiv companions: the induced isomorphisms are functorial in the ring isomorphism.
• RingEquiv.cartanMap_comp_finiteProjectiveModulesK0Equiv and RingEquiv.cartanMap_finiteProjectiveModulesK0Equiv: the Cartan maps of R and S commute with the two induced isomorphisms.
• RingEquiv.cartanMap_bijective_iff: the Cartan map of R is bijective if and only if the Cartan map of S is.

References

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

Restriction of scalars on the two object properties

theorem RingEquiv.isFG_inverseImage_restrictScalars {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (ModuleCat.isFG R).inverseImage (ModuleCat.restrictScalars e.toRingHom) = ModuleCat.isFG S

Restriction of scalars along a ring isomorphism pulls the finitely generated R-modules back to the finitely generated S-modules.

theorem RingEquiv.finiteProjectiveModules_inverseImage_restrictScalars {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (TauCeti.finiteProjectiveModules R).inverseImage (ModuleCat.restrictScalars e.toRingHom) = TauCeti.finiteProjectiveModules S

Restriction of scalars along a ring isomorphism pulls the finitely generated projective R-modules back to the finitely generated projective S-modules.

The equivalences of module subcategories

The two pullback equalities above are transported along ModuleCat.restrictScalarsEquivalenceOfRingEquiv_functor before being passed to CategoryTheory.Equivalence.congrFullSubcategory: the additivity instance of the restricted equivalence is found by instance search only when the hypothesis is stated syntactically for the functor of ModuleCat.restrictScalarsEquivalenceOfRingEquiv e.

noncomputable def RingEquiv.finiteModulesEquivalence {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : FGModuleCat S ≌ FGModuleCat R

Restriction of scalars on finitely generated modules. A ring isomorphism e : R ≃+* S induces an equivalence from the finitely generated S-modules to the finitely generated R-modules, sending a module to the same module with scalars restricted along e.

Equations

• e.finiteModulesEquivalence = (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e).congrFullSubcategory ⋯

noncomputable def RingEquiv.finiteProjectiveModulesEquivalence {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (TauCeti.finiteProjectiveModules S).FullSubcategory ≌ (TauCeti.finiteProjectiveModules R).FullSubcategory

Restriction of scalars on finitely generated projective modules. A ring isomorphism e : R ≃+* S induces an equivalence from the finitely generated projective S-modules to the finitely generated projective R-modules, sending a module to the same module with scalars restricted along e.

Equations

• e.finiteProjectiveModulesEquivalence = (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e).congrFullSubcategory ⋯

instance RingEquiv.instAdditiveFGModuleCatFunctorFiniteModulesEquivalence {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : e.finiteModulesEquivalence.functor.Additive

instance RingEquiv.instAdditiveFullSubcategoryModuleCatFiniteProjectiveModulesFunctorFiniteProjectiveModulesEquivalence {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : e.finiteProjectiveModulesEquivalence.functor.Additive

@[simp]

theorem RingEquiv.finiteModulesEquivalence_functor_obj_obj {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : FGModuleCat S) : (e.finiteModulesEquivalence.functor.obj M).obj = (ModuleCat.restrictScalars e.toRingHom).obj M.obj

@[simp]

theorem RingEquiv.finiteModulesEquivalence_functor_map_hom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) {M N : FGModuleCat S} (f : M ⟶ N) : (e.finiteModulesEquivalence.functor.map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars e.toRingHom).map f.hom) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem RingEquiv.finiteModulesEquivalence_inverse_obj_obj {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : FGModuleCat R) : (e.finiteModulesEquivalence.inverse.obj M).obj = (ModuleCat.restrictScalars e.symm.toRingHom).obj M.obj

@[simp]

theorem RingEquiv.finiteModulesEquivalence_inverse_map_hom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) {M N : FGModuleCat R} (f : M ⟶ N) : (e.finiteModulesEquivalence.inverse.map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars e.symm.toRingHom).map f.hom) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem RingEquiv.finiteProjectiveModulesEquivalence_functor_obj_obj {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : (TauCeti.finiteProjectiveModules S).FullSubcategory) : (e.finiteProjectiveModulesEquivalence.functor.obj M).obj = (ModuleCat.restrictScalars e.toRingHom).obj M.obj

@[simp]

theorem RingEquiv.finiteProjectiveModulesEquivalence_functor_map_hom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) {M N : (TauCeti.finiteProjectiveModules S).FullSubcategory} (f : M ⟶ N) : (e.finiteProjectiveModulesEquivalence.functor.map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars e.toRingHom).map f.hom) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem RingEquiv.finiteProjectiveModulesEquivalence_inverse_obj_obj {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : (TauCeti.finiteProjectiveModules R).FullSubcategory) : (e.finiteProjectiveModulesEquivalence.inverse.obj M).obj = (ModuleCat.restrictScalars e.symm.toRingHom).obj M.obj

@[simp]

theorem RingEquiv.finiteProjectiveModulesEquivalence_inverse_map_hom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) {M N : (TauCeti.finiteProjectiveModules R).FullSubcategory} (f : M ⟶ N) : (e.finiteProjectiveModulesEquivalence.inverse.map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars e.symm.toRingHom).map f.hom) (CategoryTheory.eqToHom ⋯))

theorem RingEquiv.isConflationExact_finiteModulesEquivalence_functor {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (TauCeti.finiteModulesExactStructure S).IsConflationExact (TauCeti.finiteModulesExactStructure R) e.finiteModulesEquivalence.functor

The equivalence of finitely generated module categories induced by a ring isomorphism is conflation-exact.

theorem RingEquiv.isConflationExact_finiteModulesEquivalence_inverse {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (TauCeti.finiteModulesExactStructure R).IsConflationExact (TauCeti.finiteModulesExactStructure S) e.finiteModulesEquivalence.inverse

The inverse of the equivalence of finitely generated module categories induced by a ring isomorphism is conflation-exact.

theorem RingEquiv.isConflationExact_finiteProjectiveModulesEquivalence_functor {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (TauCeti.finiteProjectiveModulesExactStructure S).IsConflationExact (TauCeti.finiteProjectiveModulesExactStructure R) e.finiteProjectiveModulesEquivalence.functor

The equivalence of finitely generated projective module categories induced by a ring isomorphism is conflation-exact.

theorem RingEquiv.isConflationExact_finiteProjectiveModulesEquivalence_inverse {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (TauCeti.finiteProjectiveModulesExactStructure R).IsConflationExact (TauCeti.finiteProjectiveModulesExactStructure S) e.finiteProjectiveModulesEquivalence.inverse

The inverse of the equivalence of finitely generated projective module categories induced by a ring isomorphism is conflation-exact.

The induced isomorphisms of Grothendieck groups

noncomputable def RingEquiv.finiteModulesK0Equiv {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure S) ≃+ TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure R)

Invariance of G₀(mod R) under ring isomorphisms. A ring isomorphism e : R ≃+* S induces G₀(mod S) ≃+ G₀(mod R), sending the class of a finitely generated S-module to the class of the same module with scalars restricted along e.

Equations

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

noncomputable def RingEquiv.finiteProjectiveModulesK0Equiv {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure S) ≃+ TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure R)

Invariance of K₀(proj R) under ring isomorphisms. A ring isomorphism e : R ≃+* S induces K₀(proj S) ≃+ K₀(proj R), sending the class of a finitely generated projective S-module to the class of the same module with scalars restricted along e.

Equations

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

@[simp]

theorem RingEquiv.finiteModulesK0Equiv_of {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : FGModuleCat S) : e.finiteModulesK0Equiv (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteModulesEquivalence.functor.obj M)

theorem RingEquiv.finiteModulesK0Equiv_symm_of {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : FGModuleCat R) : e.finiteModulesK0Equiv.symm (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteModulesEquivalence.inverse.obj M)

@[simp]

theorem RingEquiv.finiteProjectiveModulesK0Equiv_of {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : (TauCeti.finiteProjectiveModules S).FullSubcategory) : e.finiteProjectiveModulesK0Equiv (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteProjectiveModulesEquivalence.functor.obj M)

theorem RingEquiv.finiteProjectiveModulesK0Equiv_symm_of {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (M : (TauCeti.finiteProjectiveModules R).FullSubcategory) : e.finiteProjectiveModulesK0Equiv.symm (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of (e.finiteProjectiveModulesEquivalence.inverse.obj M)

Functoriality in the ring isomorphism

Restriction of scalars along the identity, along the inverse and along a composite of ring isomorphisms identifies with the identity, the inverse and the composite of the restrictions. The identity and composition isomorphisms in ModuleCat lift to the full subcategories. Isomorphic objects have the same class in exact K₀, so these comparisons give functoriality without requiring equality of the underlying restricted module structures.

@[simp]

theorem RingEquiv.finiteModulesK0Equiv_refl {R : Type u} [Ring R] : (refl R).finiteModulesK0Equiv = AddEquiv.refl (TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure R))

Restriction along the identity ring isomorphism induces the identity on G₀(mod R).

@[simp]

theorem RingEquiv.finiteModulesK0Equiv_symm {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : e.finiteModulesK0Equiv.symm = e.symm.finiteModulesK0Equiv

Restriction along the inverse ring isomorphism induces the inverse isomorphism on G₀.

@[simp]

theorem RingEquiv.finiteModulesK0Equiv_trans {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) {T : Type u} [Ring T] (e' : S ≃+* T) : e'.finiteModulesK0Equiv.trans e.finiteModulesK0Equiv = (e.trans e').finiteModulesK0Equiv

Restriction along a composite of ring isomorphisms induces the reverse composite on G₀.

@[simp]

theorem RingEquiv.finiteProjectiveModulesK0Equiv_refl {R : Type u} [Ring R] : (refl R).finiteProjectiveModulesK0Equiv = AddEquiv.refl (TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure R))

Restriction along the identity ring isomorphism induces the identity on K₀(proj R).

@[simp]

theorem RingEquiv.finiteProjectiveModulesK0Equiv_symm {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : e.finiteProjectiveModulesK0Equiv.symm = e.symm.finiteProjectiveModulesK0Equiv

Restriction along the inverse ring isomorphism induces the inverse isomorphism on K₀.

@[simp]

theorem RingEquiv.finiteProjectiveModulesK0Equiv_trans {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) {T : Type u} [Ring T] (e' : S ≃+* T) : e'.finiteProjectiveModulesK0Equiv.trans e.finiteProjectiveModulesK0Equiv = (e.trans e').finiteProjectiveModulesK0Equiv

Restriction along a composite of ring isomorphisms induces the reverse composite on K₀.

Compatibility with the Cartan map

theorem RingEquiv.cartanMap_comp_finiteProjectiveModulesK0Equiv {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : (TauCeti.cartanMap R).comp e.finiteProjectiveModulesK0Equiv.toAddMonoidHom = e.finiteModulesK0Equiv.toAddMonoidHom.comp (TauCeti.cartanMap S)

Naturality of the Cartan map in the ring. The Cartan maps of two isomorphic rings are intertwined by the induced isomorphisms of Grothendieck groups.

@[simp]

theorem RingEquiv.cartanMap_finiteProjectiveModulesK0Equiv {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (x : TauCeti.ExactK0 (TauCeti.finiteProjectiveModulesExactStructure S)) : (TauCeti.cartanMap R) (e.finiteProjectiveModulesK0Equiv x) = e.finiteModulesK0Equiv ((TauCeti.cartanMap S) x)

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

theorem RingEquiv.cartanMap_bijective_iff {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) : Function.Bijective ⇑(TauCeti.cartanMap R) ↔ Function.Bijective ⇑(TauCeti.cartanMap S)

The resolution-theorem hypothesis is invariant under ring isomorphisms: the Cartan map of R is bijective if and only if the Cartan map of S is.