Restriction of scalars on G₀(mod R) along a finite ring homomorphism

Let f : R →+* S be a ring homomorphism making S a finitely generated R-module. Restriction of scalars along f keeps the underlying abelian group of an S-module, so it is exact, and it sends a finitely generated S-module to a finitely generated R-module: a finite generating set of M over S multiplied by a finite generating set of S over R generates M over R. It therefore induces a homomorphism of exact Grothendieck groups

f^* : G₀(mod S) →+ G₀(mod R),   [M] ↦ [M with scalars restricted along f],

contravariantly functorial in f. Along a ring isomorphism it is the isomorphism RingEquiv.finiteModulesK0Equiv. The motivating instance is restriction of representations along a group homomorphism H →* G with G finite, where k[G] is finite over k[H].

The finiteness hypothesis is stated as the finite generation of S itself over R through f. It is also necessary: restriction of scalars sends the finitely generated S-module S to a finitely generated R-module only when it holds.

The API is dot notation on the ring homomorphism: use f.finiteModulesRestrictScalars hf and f.finiteModulesK0Restrict hf.

The functor on finitely generated modules, RingHom.finiteModulesRestrictScalars, is in TauCeti.Algebra.Category.ModuleCat.RestrictScalars.

Main definitions

• RingHom.finiteModulesK0Restrict: the induced homomorphism G₀(mod S) →+ G₀(mod R).

Main results

• RingHom.isConflationExact_finiteModulesRestrictScalars: the restricted functor is conflation-exact.
• RingHom.finiteModulesK0Restrict_of: the induced homomorphism sends the class of a module to the class of its restriction of scalars.
• RingHom.finiteModulesK0Restrict_id' and RingHom.finiteModulesK0Restrict_comp': the induced homomorphisms are functorial, with RingHom.finiteModulesK0Restrict_id and RingHom.finiteModulesK0Restrict_comp their forms for the literal identity and composite.
• RingEquiv.finiteModulesK0Restrict_toRingHom: along a ring isomorphism the induced homomorphism is RingEquiv.finiteModulesK0Equiv.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 6, for the functoriality of G₀ along finite ring homomorphisms.

theorem RingHom.isConflationExact_finiteModulesRestrictScalars {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) : (TauCeti.finiteModulesExactStructure S).IsConflationExact (TauCeti.finiteModulesExactStructure R) (f.finiteModulesRestrictScalars hf)

Restriction of scalars on finitely generated modules is conflation-exact: it sends a short exact sequence of finitely generated S-modules to a short exact sequence of R-modules.

noncomputable def RingHom.finiteModulesK0Restrict {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) : TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure S) →+ TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure R)

Restriction of scalars on G₀(mod R). A ring homomorphism f : R →+* S making S a finitely generated R-module 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 f.

Equations

• f.finiteModulesK0Restrict hf = TauCeti.ExactK0.map (f.finiteModulesRestrictScalars hf) ⋯

@[simp]

theorem RingHom.finiteModulesK0Restrict_of {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) (M : FGModuleCat S) : (f.finiteModulesK0Restrict hf) (TauCeti.ExactK0.of M) = TauCeti.ExactK0.of ((f.finiteModulesRestrictScalars hf).obj M)

Functoriality in the ring homomorphism

As for RingEquiv.finiteModulesK0Equiv, functoriality is proved from the isomorphisms ModuleCat.restrictScalarsId'App and ModuleCat.restrictScalarsComp'App between restricted modules: isomorphic objects have the same class. The primed forms take an equation of ring homomorphisms, so they apply to ring homomorphisms that are only propositionally an identity or a composite, such as the maps of monoid algebras induced by an identity or a composite of monoid homomorphisms.

theorem RingHom.finiteModulesK0Restrict_id' {R : Type u} [Ring R] (f : R →+* R) (h : f = id R) (hf : Module.Finite R R) : f.finiteModulesK0Restrict hf = AddMonoidHom.id (TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure R))

Restriction along a ring endomorphism equal to the identity induces the identity on G₀(mod R).

@[simp]

theorem RingHom.finiteModulesK0Restrict_id {R : Type u} [Ring R] (hf : Module.Finite R R) : (id R).finiteModulesK0Restrict hf = AddMonoidHom.id (TauCeti.ExactK0 (TauCeti.finiteModulesExactStructure R))

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

theorem RingHom.finiteModulesK0Restrict_comp' {R S T : Type u} [Ring R] [Ring S] [Ring T] (f : R →+* S) (hf : Module.Finite R S) (g : S →+* T) (gf : R →+* T) (h : gf = g.comp f) (hg : Module.Finite S T) (hgf : Module.Finite R T) : gf.finiteModulesK0Restrict hgf = (f.finiteModulesK0Restrict hf).comp (g.finiteModulesK0Restrict hg)

Restriction along a ring homomorphism equal to a composite g ∘ f induces the composite of the restrictions along g and along f, in the reverse order.

@[simp]

theorem RingHom.finiteModulesK0Restrict_comp {R S T : Type u} [Ring R] [Ring S] [Ring T] (f : R →+* S) (hf : Module.Finite R S) (g : S →+* T) (hg : Module.Finite S T) (hgf : Module.Finite R T) : (g.comp f).finiteModulesK0Restrict hgf = (f.finiteModulesK0Restrict hf).comp (g.finiteModulesK0Restrict hg)

Restriction along a composite g ∘ f of ring homomorphisms induces the composite of the restrictions along g and along f, in the reverse order.

theorem RingEquiv.finiteModulesK0Restrict_toRingHom {R S : Type u} [Ring R] [Ring S] (e : R ≃+* S) (hf : Module.Finite R S) : e.toRingHom.finiteModulesK0Restrict hf = e.finiteModulesK0Equiv.toAddMonoidHom

Along a ring isomorphism, restriction of scalars on G₀(mod S) is the isomorphism RingEquiv.finiteModulesK0Equiv.