Exactness and finite generation under coextension of scalars

Let f : R →+* S be a ring homomorphism. Mathlib's coextension of scalars ModuleCat.coextendScalars f sends an R-module M to the S-module Hom_R(S, M), with S acting through right multiplication on the source. It is right adjoint to restriction of scalars, so it is left exact. This file records when it is exact and when it preserves finite generation.

• If S is a projective R-module through f, then Hom_R(S, -) preserves surjections, so coextension of scalars sends short exact sequences to short exact sequences.
• If R and S are algebras over a commutative ring k, f is a k-algebra homomorphism, R is a finitely generated k-module and S is a finitely generated projective R-module through f, then coextension of scalars sends finitely generated R-modules to finitely generated S-modules: Hom_R(S, M) is then finitely generated already over k.

The motivating instance is coinduction of representations from a subgroup H of a finite group G: the group algebra k[G] is free of finite rank over k[H], and Hom_{k[H]}(k[G], M) is the coinduced module.

Main definitions

• AlgHom.finiteModulesCoextendScalars: coextension of scalars as a functor between the categories of finitely generated modules.

Main results

• ModuleCat.coextendScalars_map_shortExact: coextension of scalars along a ring homomorphism making S a projective R-module preserves short exact sequences.
• AlgHom.isFG_coextendScalars: coextension of scalars along a finite projective homomorphism of algebras over k, with R finite over k, preserves finite generation.

instance ModuleCat.instAdditiveCoextendScalars_tauCeti {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : (coextendScalars f).Additive

Coextension of scalars is additive, as a right adjoint of the additive restriction of scalars.

theorem ModuleCat.coextendScalars_map_shortExact {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Projective R S) {T : CategoryTheory.ShortComplex (ModuleCat R)} (hT : T.ShortExact) : (T.map (coextendScalars f)).ShortExact

Coextension of scalars along a projective ring homomorphism is exact. If S is a projective R-module through f, then Hom_R(S, -) sends a short exact sequence of R-modules to a short exact sequence of S-modules.

theorem AlgHom.isFG_coextendScalars {k : Type u_1} [CommRing k] {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] [Algebra k R] [Algebra k S] (f : R →ₐ[k] S) [Module.Finite k R] (hproj : Module.Projective R S) (hfin : Module.Finite R S) {M : ModuleCat R} (hM : ModuleCat.isFG R M) : ModuleCat.isFG S ((ModuleCat.coextendScalars f.toRingHom).obj M)

Finite generation under coextension of scalars. Let f : R →ₐ[k] S be a homomorphism of algebras over a commutative ring k, with R finitely generated over k and S finitely generated and projective over R through f. Then Hom_R(S, M) is a finitely generated S-module for every finitely generated R-module M.

noncomputable def AlgHom.finiteModulesCoextendScalars {k : Type u_1} [CommRing k] {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] [Algebra k R] [Algebra k S] (f : R →ₐ[k] S) [Module.Finite k R] (hproj : Module.Projective R S) (hfin : Module.Finite R S) : CategoryTheory.Functor (FGModuleCat R) (FGModuleCat S)

Coextension of scalars on finitely generated modules. A homomorphism f : R →ₐ[k] S of algebras over a commutative ring k, with R finitely generated over k and S finitely generated and projective over R through f, induces a functor from the finitely generated R-modules to the finitely generated S-modules, sending M to Hom_R(S, M).

Equations

• f.finiteModulesCoextendScalars hproj hfin = (ModuleCat.isFG S).lift ((ModuleCat.isFG R).ι.comp (ModuleCat.coextendScalars f.toRingHom)) ⋯

instance AlgHom.instAdditiveFGModuleCatFiniteModulesCoextendScalars {k : Type u_1} [CommRing k] {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] [Algebra k R] [Algebra k S] (f : R →ₐ[k] S) [Module.Finite k R] (hproj : Module.Projective R S) (hfin : Module.Finite R S) : (f.finiteModulesCoextendScalars hproj hfin).Additive

noncomputable def AlgHom.finiteModulesCoextendScalarsCompιIso {k : Type u_1} [CommRing k] {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] [Algebra k R] [Algebra k S] (f : R →ₐ[k] S) [Module.Finite k R] (hproj : Module.Projective R S) (hfin : Module.Finite R S) : (f.finiteModulesCoextendScalars hproj hfin).comp (ModuleCat.isFG S).ι ≅ (ModuleCat.isFG R).ι.comp (ModuleCat.coextendScalars f.toRingHom)

The underlying module of the image of a finitely generated module under AlgHom.finiteModulesCoextendScalars is its coextension of scalars, naturally in the module.

Equations

• f.finiteModulesCoextendScalarsCompιIso hproj hfin = (ModuleCat.isFG S).liftCompιIso ((ModuleCat.isFG R).ι.comp (ModuleCat.coextendScalars f.toRingHom)) ⋯

@[simp]

theorem AlgHom.finiteModulesCoextendScalars_obj_obj {k : Type u_1} [CommRing k] {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] [Algebra k R] [Algebra k S] (f : R →ₐ[k] S) [Module.Finite k R] (hproj : Module.Projective R S) (hfin : Module.Finite R S) (M : FGModuleCat R) : ((f.finiteModulesCoextendScalars hproj hfin).obj M).obj = (ModuleCat.coextendScalars f.toRingHom).obj M.obj