Change Of Rings

Main definitions

• ModuleCat.restrictScalars: given rings R, S and a ring homomorphism R ⟶ S, then restrictScalars : ModuleCat S ⥤ ModuleCat R is defined by M ↦ M where an S-module M is seen as an R-module by r • m := f r • m and S-linear map l : M ⟶ M' is R-linear as well.

• ModuleCat.extendScalars: given commutative rings R, S and ring homomorphism f : R ⟶ S, then extendScalars : ModuleCat R ⥤ ModuleCat S is defined by M ↦ S ⨂ M where the module structure is defined by s • (s' ⊗ m) := (s * s') ⊗ m and R-linear map l : M ⟶ M' is sent to S-linear map s ⊗ m ↦ s ⊗ l m : S ⨂ M ⟶ S ⨂ M'.

• ModuleCat.coextendScalars: given rings R, S and a ring homomorphism R ⟶ S then coextendScalars : ModuleCat R ⥤ ModuleCat S is defined by M ↦ (S →ₗ[R] M) where S is seen as an R-module by restriction of scalars and l ↦ l ∘ _.

Main results

• ModuleCat.extendRestrictScalarsAdj: given commutative rings R, S and a ring homomorphism f : R →+* S, the extension and restriction of scalars by f are adjoint functors.
• ModuleCat.restrictCoextendScalarsAdj: given rings R, S and a ring homomorphism f : R ⟶ S then coextendScalars f is the right adjoint of restrictScalars f.

List of notations

Let R, S be rings and f : R →+* S

• if M is an R-module, s : S and m : M, then s ⊗ₜ[R, f] m is the pure tensor s ⊗ m : S ⊗[R, f] M.

noncomputable def ModuleCat.RestrictScalars.obj' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat S) : ModuleCat R

Any S-module M is also an R-module via a ring homomorphism f : R ⟶ S by defining r • m := f r • m (Module.compHom). This is called restriction of scalars.

Equations

• ModuleCat.RestrictScalars.obj' f M = ModuleCat.mk ↑M

noncomputable def ModuleCat.RestrictScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat S} {M' : ModuleCat S} (g : M ⟶ M') : ModuleCat.RestrictScalars.obj' f M ⟶ ModuleCat.RestrictScalars.obj' f M'

Given an S-linear map g : M → M' between S-modules, g is also R-linear between M and M' by means of restriction of scalars.

Equations

• ModuleCat.RestrictScalars.map' f g = { toAddHom := g.toAddHom, map_smul' := ⋯ }

noncomputable def ModuleCat.restrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.Functor (ModuleCat S) (ModuleCat R)

The restriction of scalars operation is functorial. For any f : R →+* S a ring homomorphism,

• an S-module M can be considered as R-module by r • m = f r • m
• an S-linear map is also R-linear

Equations

• ModuleCat.restrictScalars f = { obj := ModuleCat.RestrictScalars.obj' f, map := fun {X Y : ModuleCat S} => ModuleCat.RestrictScalars.map' f, map_id := ⋯, map_comp := ⋯ }

noncomputable instance ModuleCat.instFaithfulRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : (ModuleCat.restrictScalars f).Faithful

Equations

• ⋯ = ⋯

noncomputable instance ModuleCat.instPreservesMonomorphismsRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : (ModuleCat.restrictScalars f).PreservesMonomorphisms

Equations

• ⋯ = ⋯

noncomputable instance ModuleCat.instModuleCarrierObjRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : ModuleCat S} : Module R ↑((ModuleCat.restrictScalars f).obj M)

Equations

• ModuleCat.instModuleCarrierObjRestrictScalars = inferInstanceAs (Module R ↑(ModuleCat.RestrictScalars.obj' f M))

noncomputable instance ModuleCat.instModuleCarrierObjRestrictScalars_1 {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S} {M : ModuleCat S} : Module S ↑((ModuleCat.restrictScalars f).obj M)

Equations

• ModuleCat.instModuleCarrierObjRestrictScalars_1 = inferInstanceAs (Module S ↑M)

@[simp]

theorem ModuleCat.restrictScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat S} {M' : ModuleCat S} (g : M ⟶ M') (x : ↑((ModuleCat.restrictScalars f).obj M)) : ((ModuleCat.restrictScalars f).map g) x = g x

@[simp]

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

theorem ModuleCat.restrictScalars.smul_def' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat S} (r : R) (m : ↑M) : let m' := m; r • m' = f r • m

noncomputable instance ModuleCat.sMulCommClass_mk {R : Type u₁} {S : Type u₂} [Ring R] [CommRing S] (f : R →+* S) (M : Type v) [I : AddCommGroup M] [Module S M] : SMulCommClass R S M

Equations

• ⋯ = ⋯

noncomputable def ModuleCat.semilinearMapAddEquiv {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S) : (↑M →ₛₗ[f] ↑N) ≃+ (M ⟶ (ModuleCat.restrictScalars f).obj N)

Semilinear maps M →ₛₗ[f] N identify to morphisms M ⟶ (ModuleCat.restrictScalars f).obj N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.semilinearMapAddEquiv_symm_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S) (g : M ⟶ (ModuleCat.restrictScalars f).obj N) (a : ↑M) : ((ModuleCat.semilinearMapAddEquiv f M N).symm g) a = g a

@[simp]

theorem ModuleCat.semilinearMapAddEquiv_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S) (g : ↑M →ₛₗ[f] ↑N) (a : ↑M) : ((ModuleCat.semilinearMapAddEquiv f M N) g) a = g a

noncomputable def ModuleCat.restrictScalarsId'App {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) : (ModuleCat.restrictScalars f).obj M ≅ M

For a R-module M, the restriction of scalars of M by the identity morphisms identifies to M.

Equations

• ModuleCat.restrictScalarsId'App f hf M = ((AddEquiv.refl ↑((ModuleCat.restrictScalars f).obj M)).toLinearEquiv ⋯).toModuleIso'

theorem ModuleCat.restrictScalarsId'App_hom_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : ↑M) : (ModuleCat.restrictScalarsId'App f hf M).hom x = x

theorem ModuleCat.restrictScalarsId'App_inv_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : ↑M) : (ModuleCat.restrictScalarsId'App f hf M).inv x = x

noncomputable def ModuleCat.restrictScalarsId' {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) : ModuleCat.restrictScalars f ≅ CategoryTheory.Functor.id (ModuleCat R)

The restriction of scalars by a ring morphism that is the identity identify to the identity functor.

Equations

• ModuleCat.restrictScalarsId' f hf = CategoryTheory.NatIso.ofComponents (fun (M : ModuleCat R) => ModuleCat.restrictScalarsId'App f hf M) ⋯

@[simp]

theorem ModuleCat.restrictScalarsId'_inv_app {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (X : ModuleCat R) : (ModuleCat.restrictScalarsId' f hf).inv.app X = (ModuleCat.restrictScalarsId'App f hf X).inv

@[simp]

theorem ModuleCat.restrictScalarsId'_hom_app {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (X : ModuleCat R) : (ModuleCat.restrictScalarsId' f hf).hom.app X = (ModuleCat.restrictScalarsId'App f hf X).hom

theorem ModuleCat.restrictScalarsId'App_hom_naturality_assoc {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M : ModuleCat R} {N : ModuleCat R} (φ : M ⟶ N) {Z : ModuleCat R} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map φ) (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf N).hom h) = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).hom (CategoryTheory.CategoryStruct.comp φ h)

theorem ModuleCat.restrictScalarsId'App_hom_naturality {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M : ModuleCat R} {N : ModuleCat R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map φ) (ModuleCat.restrictScalarsId'App f hf N).hom = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).hom φ

theorem ModuleCat.restrictScalarsId'App_inv_naturality_assoc {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M : ModuleCat R} {N : ModuleCat R} (φ : M ⟶ N) {Z : ModuleCat R} (h : (ModuleCat.restrictScalars f).obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf N).inv h) = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).inv (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map φ) h)

theorem ModuleCat.restrictScalarsId'App_inv_naturality {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M : ModuleCat R} {N : ModuleCat R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp φ (ModuleCat.restrictScalarsId'App f hf N).inv = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).inv ((ModuleCat.restrictScalars f).map φ)

@[reducible, inline]

noncomputable abbrev ModuleCat.restrictScalarsId (R : Type u₁) [Ring R] : ModuleCat.restrictScalars (RingHom.id R) ≅ CategoryTheory.Functor.id (ModuleCat R)

The restriction of scalars by the identity morphisms identify to the identity functor.

Equations

• ModuleCat.restrictScalarsId R = ModuleCat.restrictScalarsId' (RingHom.id R) ⋯

noncomputable def ModuleCat.restrictScalarsComp'App {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ModuleCat R₃) : (ModuleCat.restrictScalars gf).obj M ≅ (ModuleCat.restrictScalars f).obj ((ModuleCat.restrictScalars g).obj M)

For each R₃-module M, restriction of scalars of M by a composition of ring morphisms identifies to successively restricting scalars.

Equations

• ModuleCat.restrictScalarsComp'App f g gf hgf M = ((AddEquiv.refl ↑((ModuleCat.restrictScalars gf).obj M)).toLinearEquiv ⋯).toModuleIso'

theorem ModuleCat.restrictScalarsComp'App_hom_apply {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ModuleCat R₃) (x : ↑M) : (ModuleCat.restrictScalarsComp'App f g gf hgf M).hom x = x

theorem ModuleCat.restrictScalarsComp'App_inv_apply {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ModuleCat R₃) (x : ↑M) : (ModuleCat.restrictScalarsComp'App f g gf hgf M).inv x = x

noncomputable def ModuleCat.restrictScalarsComp' {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) : ModuleCat.restrictScalars gf ≅ (ModuleCat.restrictScalars g).comp (ModuleCat.restrictScalars f)

The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.

Equations

• ModuleCat.restrictScalarsComp' f g gf hgf = CategoryTheory.NatIso.ofComponents (fun (M : ModuleCat R₃) => ModuleCat.restrictScalarsComp'App f g gf hgf M) ⋯

@[simp]

theorem ModuleCat.restrictScalarsComp'_hom_app {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (X : ModuleCat R₃) : (ModuleCat.restrictScalarsComp' f g gf hgf).hom.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).hom

@[simp]

theorem ModuleCat.restrictScalarsComp'_inv_app {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (X : ModuleCat R₃) : (ModuleCat.restrictScalarsComp' f g gf hgf).inv.app X = (ModuleCat.restrictScalarsComp'App f g gf hgf X).inv

theorem ModuleCat.restrictScalarsComp'App_hom_naturality_assoc {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : ModuleCat R₃} {N : ModuleCat R₃} (φ : M ⟶ N) {Z : ModuleCat R₁} (h : (ModuleCat.restrictScalars f).obj ((ModuleCat.restrictScalars g).obj N) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars gf).map φ) (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf N).hom h) = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).hom (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ)) h)

theorem ModuleCat.restrictScalarsComp'App_hom_naturality {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : ModuleCat R₃} {N : ModuleCat R₃} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars gf).map φ) (ModuleCat.restrictScalarsComp'App f g gf hgf N).hom = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).hom ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ))

theorem ModuleCat.restrictScalarsComp'App_inv_naturality_assoc {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : ModuleCat R₃} {N : ModuleCat R₃} (φ : M ⟶ N) {Z : ModuleCat R₁} (h : (ModuleCat.restrictScalars gf).obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ)) (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf N).inv h) = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).inv (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars gf).map φ) h)

theorem ModuleCat.restrictScalarsComp'App_inv_naturality {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M : ModuleCat R₃} {N : ModuleCat R₃} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ)) (ModuleCat.restrictScalarsComp'App f g gf hgf N).inv = CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).inv ((ModuleCat.restrictScalars gf).map φ)

@[reducible, inline]

noncomputable abbrev ModuleCat.restrictScalarsComp {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [Ring R₁] [Ring R₂] [Ring R₃] (f : R₁ →+* R₂) (g : R₂ →+* R₃) : ModuleCat.restrictScalars (g.comp f) ≅ (ModuleCat.restrictScalars g).comp (ModuleCat.restrictScalars f)

The restriction of scalars by a composition of ring morphisms identify to the composition of the restriction of scalars functors.

Equations

• ModuleCat.restrictScalarsComp f g = ModuleCat.restrictScalarsComp' f g (g.comp f) ⋯

noncomputable instance ModuleCat.restrictScalarsIsEquivalenceOfRingEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (e : R ≃+* S) : (ModuleCat.restrictScalars e.toRingHom).IsEquivalence

Equations

• One or more equations did not get rendered due to their size.

def ChangeOfRings.«term_⊗ₜ[_,_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.ExtendScalars.obj' {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (M : ModuleCat R) : ModuleCat S

Extension of scalars turn an R-module into S-module by M ↦ S ⨂ M

Equations

• ModuleCat.ExtendScalars.obj' f M = ModuleCat.mk (TensorProduct R ↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) ↑M)

noncomputable def ModuleCat.ExtendScalars.map' {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M1 : ModuleCat R} {M2 : ModuleCat R} (l : M1 ⟶ M2) : ModuleCat.ExtendScalars.obj' f M1 ⟶ ModuleCat.ExtendScalars.obj' f M2

Extension of scalars is a functor where an R-module M is sent to S ⊗ M and l : M1 ⟶ M2 is sent to s ⊗ m ↦ s ⊗ l m

Equations

• ModuleCat.ExtendScalars.map' f l = LinearMap.baseChange S l

theorem ModuleCat.ExtendScalars.map'_id {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M : ModuleCat R} : ModuleCat.ExtendScalars.map' f (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (ModuleCat.ExtendScalars.obj' f M)

theorem ModuleCat.ExtendScalars.map'_comp {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M₁ : ModuleCat R} {M₂ : ModuleCat R} {M₃ : ModuleCat R} (l₁₂ : M₁ ⟶ M₂) (l₂₃ : M₂ ⟶ M₃) : ModuleCat.ExtendScalars.map' f (CategoryTheory.CategoryStruct.comp l₁₂ l₂₃) = CategoryTheory.CategoryStruct.comp (ModuleCat.ExtendScalars.map' f l₁₂) (ModuleCat.ExtendScalars.map' f l₂₃)

noncomputable def ModuleCat.extendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.Functor (ModuleCat R) (ModuleCat S)

Extension of scalars is a functor where an R-module M is sent to S ⊗ M and l : M1 ⟶ M2 is sent to s ⊗ m ↦ s ⊗ l m

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.ExtendScalars.smul_tmul {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M : ModuleCat R} (s : S) (s' : S) (m : ↑M) : s • s' ⊗ₜ[R] m = (s * s') ⊗ₜ[R] m

@[simp]

theorem ModuleCat.ExtendScalars.map_tmul {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') (s : S) (m : ↑M) : ((ModuleCat.extendScalars f).map g) (s ⊗ₜ[R] m) = s ⊗ₜ[R] g m

noncomputable instance ModuleCat.CoextendScalars.hasSMul {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : SMul S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M)

Given an R-module M, consider Hom(S, M) -- the R-linear maps between S (as an R-module by means of restriction of scalars) and M. S acts on Hom(S, M) by s • g = x ↦ g (x • s)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.CoextendScalars.smul_apply' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] (s : S) (g : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M) (s' : S) : (s • g) s' = g (s' * s)

noncomputable instance ModuleCat.CoextendScalars.mulAction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : MulAction S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M)

Equations

• ModuleCat.CoextendScalars.mulAction f M = let __src := ModuleCat.CoextendScalars.hasSMul f M; MulAction.mk ⋯ ⋯

noncomputable instance ModuleCat.CoextendScalars.distribMulAction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : DistribMulAction S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M)

Equations

• ModuleCat.CoextendScalars.distribMulAction f M = let __src := ModuleCat.CoextendScalars.mulAction f M; DistribMulAction.mk ⋯ ⋯

noncomputable instance ModuleCat.CoextendScalars.isModule {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : Type v) [AddCommMonoid M] [Module R M] : Module S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] M)

S acts on Hom(S, M) by s • g = x ↦ g (x • s), this action defines an S-module structure on Hom(S, M).

Equations

• ModuleCat.CoextendScalars.isModule f M = let __src := ModuleCat.CoextendScalars.distribMulAction f M; Module.mk ⋯ ⋯

noncomputable def ModuleCat.CoextendScalars.obj' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) : ModuleCat S

If M is an R-module, then the set of R-linear maps S →ₗ[R] M is an S-module with scalar multiplication defined by s • l := x ↦ l (x • s)

Equations

• ModuleCat.CoextendScalars.obj' f M = ModuleCat.mk (↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S)) →ₗ[R] ↑M)

noncomputable instance ModuleCat.CoextendScalars.instCoeFunCarrierObj'Forall {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) : CoeFun ↑(ModuleCat.CoextendScalars.obj' f M) fun (x : ↑(ModuleCat.CoextendScalars.obj' f M)) => S → ↑M

Equations

• ModuleCat.CoextendScalars.instCoeFunCarrierObj'Forall f M = { coe := fun (g : ↑(ModuleCat.CoextendScalars.obj' f M)) => g.toFun }

noncomputable def ModuleCat.CoextendScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') : ModuleCat.CoextendScalars.obj' f M ⟶ ModuleCat.CoextendScalars.obj' f M'

If M, M' are R-modules, then any R-linear map g : M ⟶ M' induces an S-linear map (S →ₗ[R] M) ⟶ (S →ₗ[R] M') defined by h ↦ g ∘ h

Equations

• ModuleCat.CoextendScalars.map' f g = { toFun := fun (h : ↑(ModuleCat.CoextendScalars.obj' f M)) => g ∘ₗ h, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ModuleCat.CoextendScalars.map'_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') (h : ↑(ModuleCat.CoextendScalars.obj' f M)) : (ModuleCat.CoextendScalars.map' f g) h = g ∘ₗ h

noncomputable def ModuleCat.coextendScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.Functor (ModuleCat R) (ModuleCat S)

For any rings R, S and a ring homomorphism f : R →+* S, there is a functor from R-module to S-module defined by M ↦ (S →ₗ[R] M) where S is considered as an R-module via restriction of scalars and g : M ⟶ M' is sent to h ↦ g ∘ h.

Equations

• ModuleCat.coextendScalars f = { obj := ModuleCat.CoextendScalars.obj' f, map := fun {X Y : ModuleCat R} => ModuleCat.CoextendScalars.map' f, map_id := ⋯, map_comp := ⋯ }

noncomputable instance ModuleCat.CoextendScalars.instCoeFunCarrierObjCoextendScalarsForall {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) : CoeFun ↑((ModuleCat.coextendScalars f).obj M) fun (x : ↑((ModuleCat.coextendScalars f).obj M)) => S → ↑M

Equations

• One or more equations did not get rendered due to their size.

theorem ModuleCat.CoextendScalars.smul_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (g : ↑((ModuleCat.coextendScalars f).obj M)) (s : S) (s' : S) : (s • g).toFun s' = g.toFun (s' * s)

@[simp]

theorem ModuleCat.CoextendScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat R} {M' : ModuleCat R} (g : M ⟶ M') (x : ↑((ModuleCat.coextendScalars f).obj M)) (s : S) : (((ModuleCat.coextendScalars f).map g) x).toFun s = g (x.toFun s)

noncomputable def ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.restrictScalars f).obj Y ⟶ X) : Y ⟶ (ModuleCat.coextendScalars f).obj X

Given R-module X and S-module Y, any g : (restrictScalars f).obj Y ⟶ X corresponds to Y ⟶ (coextendScalars f).obj X by sending y ↦ (s ↦ g (s • y))

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.restrictScalars f).obj Y ⟶ X) (y : ↑Y) (s : S) : ((ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction f g) y) s = g (s • y)

noncomputable def ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : Y ⟶ (ModuleCat.coextendScalars f).obj X) : (ModuleCat.restrictScalars f).obj Y ⟶ X

Given R-module X and S-module Y, any g : Y ⟶ (coextendScalars f).obj X corresponds to (restrictScalars f).obj Y ⟶ X by y ↦ g y 1

Equations

• ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction f g = { toFun := fun (y : ↑Y) => (g y).toFun 1, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : Y ⟶ (ModuleCat.coextendScalars f).obj X) (y : ↑Y) : (ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction f g) y = (g y).toFun 1

noncomputable def ModuleCat.RestrictionCoextensionAdj.app' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (Y : ModuleCat S) : ↑Y →ₗ[S] ↑(((ModuleCat.restrictScalars f).comp (ModuleCat.coextendScalars f)).obj Y)

Auxiliary definition for unit'

Equations

• ModuleCat.RestrictionCoextensionAdj.app' f Y = { toFun := fun (y : ↑Y) => { toFun := fun (s : S) => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ModuleCat.RestrictionCoextensionAdj.unit' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.Functor.id (ModuleCat S) ⟶ (ModuleCat.restrictScalars f).comp (ModuleCat.coextendScalars f)

The natural transformation from identity functor to the composition of restriction and coextension of scalars.

Equations

• ModuleCat.RestrictionCoextensionAdj.unit' f = { app := fun (Y : ModuleCat S) => ModuleCat.RestrictionCoextensionAdj.app' f Y, naturality := ⋯ }

noncomputable def ModuleCat.RestrictionCoextensionAdj.counit' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : (ModuleCat.coextendScalars f).comp (ModuleCat.restrictScalars f) ⟶ CategoryTheory.Functor.id (ModuleCat R)

The natural transformation from the composition of coextension and restriction of scalars to identity functor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModuleCat.restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : ModuleCat.restrictScalars f ⊣ ModuleCat.coextendScalars f

Restriction of scalars is left adjoint to coextension of scalars.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance ModuleCat.instIsLeftAdjointRestrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.IsLeftAdjoint (ModuleCat.restrictScalars f)

Equations

• ModuleCat.instIsLeftAdjointRestrictScalars f = { right := ModuleCat.coextendScalars f, adj := ModuleCat.restrictCoextendScalarsAdj f }

noncomputable instance ModuleCat.instIsRightAdjointCoextendScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) : CategoryTheory.IsRightAdjoint (ModuleCat.coextendScalars f)

Equations

• ModuleCat.instIsRightAdjointCoextendScalars f = { left := ModuleCat.restrictScalars f, adj := ModuleCat.restrictCoextendScalarsAdj f }

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.extendScalars f).obj X ⟶ Y) : X ⟶ (ModuleCat.restrictScalars f).obj Y

Given R-module X and S-module Y and a map g : (extendScalars f).obj X ⟶ Y, i.e. S-linear map S ⨂ X → Y, there is a X ⟶ (restrictScalars f).obj Y, i.e. R-linear map X ⟶ Y by x ↦ g (1 ⊗ x).

Equations

• ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g = { toFun := fun (x : ↑X) => g (1 ⊗ₜ[R] x), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (ModuleCat.extendScalars f).obj X ⟶ Y) (x : ↑X) : (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars f g) x = g (1 ⊗ₜ[R] x)

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (s : S) (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) : let_fun this := Module.compHom (↑Y) f; ↑X →ₗ[R] ↑Y

The map S → X →ₗ[R] Y given by fun s x => s • (g x)

Equations

• ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g = { toFun := fun (x : ↑X) => s • g x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (s : S) (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) (x : ↑X) : (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g) x = s • g x

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) : (ModuleCat.extendScalars f).obj X ⟶ Y

Given R-module X and S-module Y and a map X ⟶ (restrictScalars f).obj Y, i.e R-linear map X ⟶ Y, there is a map (extend_scalars f).obj X ⟶ Y, i.e S-linear map S ⨂ X → Y by s ⊗ x ↦ s • g x.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) (z : ↑((ModuleCat.extendScalars f).obj X)) : (ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g) z = (TensorProduct.lift { toFun := fun (s : ↑((ModuleCat.restrictScalars f).obj (ModuleCat.mk S))) => ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) z

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.homEquiv {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} : ((ModuleCat.extendScalars f).obj X ⟶ Y) ≃ (X ⟶ (ModuleCat.restrictScalars f).obj Y)

Given R-module X and S-module Y, S-linear linear maps (extendScalars f).obj X ⟶ Y bijectively correspond to R-linear maps X ⟶ (restrictScalars f).obj Y.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y) : (ModuleCat.ExtendRestrictScalarsAdj.homEquiv f).symm g = ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.Unit.map {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} : X ⟶ ((ModuleCat.extendScalars f).comp (ModuleCat.restrictScalars f)).obj X

For any R-module X, there is a natural R-linear map from X to X ⨂ S by sending x ↦ x ⊗ 1

Equations

• ModuleCat.ExtendRestrictScalarsAdj.Unit.map f = { toFun := fun (x : ↑X) => 1 ⊗ₜ[R] x, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.unit {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.Functor.id (ModuleCat R) ⟶ (ModuleCat.extendScalars f).comp (ModuleCat.restrictScalars f)

The natural transformation from identity functor on R-module to the composition of extension and restriction of scalars.

Equations

• ModuleCat.ExtendRestrictScalarsAdj.unit f = { app := fun (x : ModuleCat R) => ModuleCat.ExtendRestrictScalarsAdj.Unit.map f, naturality := ⋯ }

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.unit_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : ∀ (x : ModuleCat R), (ModuleCat.ExtendRestrictScalarsAdj.unit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Unit.map f

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.Counit.map {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {Y : ModuleCat S} : ((ModuleCat.restrictScalars f).comp (ModuleCat.extendScalars f)).obj Y ⟶ Y

For any S-module Y, there is a natural R-linear map from S ⨂ Y to Y by s ⊗ y ↦ s • y

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.Counit.map_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {Y : ModuleCat S} (a : TensorProduct R S ↑Y) : (ModuleCat.ExtendRestrictScalarsAdj.Counit.map f) a = (TensorProduct.lift { toFun := fun (s : S) => { toFun := fun (y : ↑Y) => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) a

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.counit {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : (ModuleCat.restrictScalars f).comp (ModuleCat.extendScalars f) ⟶ CategoryTheory.Functor.id (ModuleCat S)

The natural transformation from the composition of restriction and extension of scalars to the identity functor on S-module.

Equations

• ModuleCat.ExtendRestrictScalarsAdj.counit f = { app := fun (x : ModuleCat S) => ModuleCat.ExtendRestrictScalarsAdj.Counit.map f, naturality := ⋯ }

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.counit_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : ∀ (x : ModuleCat S), (ModuleCat.ExtendRestrictScalarsAdj.counit f).app x = ModuleCat.ExtendRestrictScalarsAdj.Counit.map f

noncomputable def ModuleCat.extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : ModuleCat.extendScalars f ⊣ ModuleCat.restrictScalars f

Given commutative rings R, S and a ring hom f : R →+* S, the extension and restriction of scalars by f are adjoint to each other.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance ModuleCat.instIsLeftAdjointExtendScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.IsLeftAdjoint (ModuleCat.extendScalars f)

Equations

• ModuleCat.instIsLeftAdjointExtendScalars f = { right := ModuleCat.restrictScalars f, adj := ModuleCat.extendRestrictScalarsAdj f }

noncomputable instance ModuleCat.instIsRightAdjointRestrictScalars {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : CategoryTheory.IsRightAdjoint (ModuleCat.restrictScalars f)

Equations

• ModuleCat.instIsRightAdjointRestrictScalars f = { left := ModuleCat.extendScalars f, adj := ModuleCat.extendRestrictScalarsAdj f }

noncomputable instance ModuleCat.preservesLimitRestrictScalars {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {J : Type u_3} [CategoryTheory.Category.{u_4, u_3} J] (F : CategoryTheory.Functor J (ModuleCat S)) [Small.{v, max u_3 v} ↑(F.comp (CategoryTheory.forget (ModuleCat S))).sections] : CategoryTheory.Limits.PreservesLimit F (ModuleCat.restrictScalars f)

Equations

• One or more equations did not get rendered due to their size.