Finite generation and projectivity under restriction of scalars

Restriction of scalars along a ring homomorphism f : R →+* S keeps the underlying abelian group of a module and only changes which ring acts on it. This file records when the two finiteness properties defining K₀(proj R) and G₀(mod R) survive it.

• Along a surjective ring homomorphism, finite generation is preserved and reflected: every scalar of S is the image of a scalar of R, so the S-span and the R-span of a set coincide.
• Along a ring homomorphism making S a finitely generated R-module, finite generation is preserved, so restriction of scalars is a functor between the categories of finitely generated modules.
• Along a ring isomorphism, projectivity is preserved and reflected: the identity of the module is then a semilinear equivalence between the two module structures.

The API is dot notation on the ring homomorphism, respectively the ring isomorphism: use f.finite_restrictScalars_iff hf M and e.projective_restrictScalars_iff M.

Main definitions

• RingHom.restrictScalarsSemilinearMap: the identity of a module, as a semilinear map from its restriction of scalars.
• RingHom.finiteModulesRestrictScalars: restriction of scalars along a finite ring homomorphism, as a functor between the categories of finitely generated modules.
• RingHom.finiteModulesRestrictScalarsCompιIso: the underlying module of an image under RingHom.finiteModulesRestrictScalars is the restriction of scalars, naturally in the module.

Main results

• RingHom.finite_restrictScalars_iff and RingHom.isFG_restrictScalars_iff: finite generation is invariant under restriction of scalars along a surjective ring homomorphism.
• RingHom.isFG_restrictScalars_of_finite: finite generation is preserved by restriction of scalars along a ring homomorphism f : R →+* S making S a finitely generated R-module.
• RingEquiv.projective_restrictScalars_iff: projectivity is invariant under restriction of scalars along a ring isomorphism.

def RingHom.restrictScalarsSemilinearMap {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat S) : ↑((ModuleCat.restrictScalars f).obj M) →ₛₗ[f] ↑M

The identity map of an S-module M, as an f-semilinear map from M with scalars restricted along f : R →+* S to M itself.

Equations

• f.restrictScalarsSemilinearMap M = { toFun := fun (m : ↑((ModuleCat.restrictScalars f).obj M)) => m, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RingHom.restrictScalarsSemilinearMap_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat S) (m : ↑((ModuleCat.restrictScalars f).obj M)) : (f.restrictScalarsSemilinearMap M) m = m

theorem RingHom.finite_restrictScalars_iff {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Surjective ⇑f) (M : ModuleCat S) : Module.Finite R ↑((ModuleCat.restrictScalars f).obj M) ↔ Module.Finite S ↑M

Finite generation along a surjective ring homomorphism. Restricting scalars along a surjective ring homomorphism preserves and reflects finite generation: every scalar of S is the image of a scalar of R, so the two spans of a set agree.

theorem RingHom.isFG_restrictScalars_iff {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Surjective ⇑f) (M : ModuleCat S) : ModuleCat.isFG R ((ModuleCat.restrictScalars f).obj M) ↔ ModuleCat.isFG S M

Restricting scalars along a surjective ring homomorphism preserves and reflects the object property of being finitely generated.

theorem RingHom.isFG_restrictScalars_of_finite {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) {M : ModuleCat S} (hM : ModuleCat.isFG S M) : ModuleCat.isFG R ((ModuleCat.restrictScalars f).obj M)

Finite generation along a finite ring homomorphism. If S is finitely generated as an R-module through f : R →+* S, then restriction of scalars along f sends every finitely generated S-module to a finitely generated R-module.

noncomputable def RingHom.finiteModulesRestrictScalars {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) : CategoryTheory.Functor (FGModuleCat S) (FGModuleCat R)

Restriction of scalars on finitely generated modules. A ring homomorphism f : R →+* S making S a finitely generated R-module induces a functor from the finitely generated S-modules to the finitely generated R-modules, sending a module to the same module with scalars restricted along f.

Equations

• f.finiteModulesRestrictScalars hf = (ModuleCat.isFG R).lift ((ModuleCat.isFG S).ι.comp (ModuleCat.restrictScalars f)) ⋯

instance RingHom.instAdditiveFGModuleCatFiniteModulesRestrictScalars {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) : (f.finiteModulesRestrictScalars hf).Additive

noncomputable def RingHom.finiteModulesRestrictScalarsCompιIso {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) : (f.finiteModulesRestrictScalars hf).comp (ModuleCat.isFG R).ι ≅ (ModuleCat.isFG S).ι.comp (ModuleCat.restrictScalars f)

The underlying module of the image of a finitely generated module under RingHom.finiteModulesRestrictScalars is the module with scalars restricted along f, naturally in the module.

Equations

• f.finiteModulesRestrictScalarsCompιIso hf = (ModuleCat.isFG R).liftCompιIso ((ModuleCat.isFG S).ι.comp (ModuleCat.restrictScalars f)) ⋯

@[simp]

theorem RingHom.finiteModulesRestrictScalars_obj_obj {R S : Type u} [Ring R] [Ring S] (f : R →+* S) (hf : Module.Finite R S) (M : FGModuleCat S) : ((f.finiteModulesRestrictScalars hf).obj M).obj = (ModuleCat.restrictScalars f).obj M.obj

theorem RingEquiv.projective_restrictScalars_iff {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (e : R ≃+* S) (M : ModuleCat S) : Module.Projective R ↑((ModuleCat.restrictScalars e.toRingHom).obj M) ↔ Module.Projective S ↑M

Projectivity along a ring isomorphism. Restricting scalars along a ring isomorphism preserves and reflects projectivity: the identity is a semilinear equivalence between the two module structures, and projectivity transports along semilinear equivalences.