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.

Notation

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.

noncomputable def ModuleCat.RestrictScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat S} (g : M ⟶ M') : obj' f M ⟶ 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.

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

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

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

instance ModuleCat.instReflectsIsomorphismsRestrictScalars {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) : (restrictScalars f).ReflectsIsomorphisms

@[implicit_reducible]

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

@[simp]

theorem ModuleCat.restrictScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat S} (g : M ⟶ M') (x : ↑((restrictScalars f).obj M)) : (CategoryTheory.ConcreteCategory.hom ((restrictScalars f).map g)) x = (CategoryTheory.ConcreteCategory.hom 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 : ↑((restrictScalars f).obj M)) : r • m = f r • have this := m; this

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) : (r • have this := m; this) = f r • m

@[instance 100]

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

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 ⟶ (restrictScalars f).obj N)

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

@[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 ⟶ (restrictScalars f).obj N) (a : ↑M) : ((semilinearMapAddEquiv f M N).symm g) a = (CategoryTheory.ConcreteCategory.hom g) a

@[simp]

theorem ModuleCat.semilinearMapAddEquiv_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (M : ModuleCat R) (N : ModuleCat S) (g : ↑M →ₛₗ[f] ↑N) : (semilinearMapAddEquiv f M N) g = ofHom { toFun := ⇑g, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ModuleCat.restrictScalarsCongr {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f g : R →+* S} (e : f = g) : restrictScalars f ≅ restrictScalars g

Restrictions scalars along equal ring homomorphisms are naturally isomorphic.

@[simp]

theorem ModuleCat.restrictScalarsCongr_symm {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f g : R →+* S} (e : f = g) : (restrictScalarsCongr e).symm = restrictScalarsCongr ⋯

@[simp]

theorem ModuleCat.restrictScalarsCongr_hom_app {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f g : R →+* S} (e : f = g) (M : ModuleCat S) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom ((restrictScalarsCongr e).hom.app M)) x = x

@[simp]

theorem ModuleCat.restrictScalarsCongr_inv_app {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f g : R →+* S} (e : f = g) (M : ModuleCat S) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom ((restrictScalarsCongr e).inv.app M)) x = x

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

For an R-module M, the restriction of scalars of M by the identity morphism identifies to M.

@[simp]

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

@[simp]

theorem ModuleCat.restrictScalarsId'App_inv_apply {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (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) : restrictScalars f ≅ CategoryTheory.Functor.id (ModuleCat R)

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

@[simp]

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

@[simp]

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

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

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

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

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

@[reducible, inline]

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

The restriction of scalars by the identity morphism identifies to the identity functor.

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₃) : (restrictScalars gf).obj M ≅ (restrictScalars f).obj ((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.

@[simp]

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) : (CategoryTheory.ConcreteCategory.hom (restrictScalarsComp'App f g gf hgf M).hom) x = x

@[simp]

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) : (CategoryTheory.ConcreteCategory.hom (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) : restrictScalars gf ≅ (restrictScalars g).comp (restrictScalars f)

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

@[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₃) : (restrictScalarsComp' f g gf hgf).inv.app X = (restrictScalarsComp'App f g gf hgf X).inv

@[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₃) : (restrictScalarsComp' f g gf hgf).hom.app X = (restrictScalarsComp'App f g gf hgf X).hom

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 N : ModuleCat R₃} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((restrictScalars gf).map φ) (restrictScalarsComp'App f g gf hgf N).hom = CategoryTheory.CategoryStruct.comp (restrictScalarsComp'App f g gf hgf M).hom ((restrictScalars f).map ((restrictScalars g).map φ))

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 N : ModuleCat R₃} (φ : M ⟶ N) {Z : ModuleCat R₁} (h : (restrictScalars f).obj ((restrictScalars g).obj N) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((restrictScalars gf).map φ) (CategoryTheory.CategoryStruct.comp (restrictScalarsComp'App f g gf hgf N).hom h) = CategoryTheory.CategoryStruct.comp (restrictScalarsComp'App f g gf hgf M).hom (CategoryTheory.CategoryStruct.comp ((restrictScalars f).map ((restrictScalars g).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 N : ModuleCat R₃} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((restrictScalars f).map ((restrictScalars g).map φ)) (restrictScalarsComp'App f g gf hgf N).inv = CategoryTheory.CategoryStruct.comp (restrictScalarsComp'App f g gf hgf M).inv ((restrictScalars gf).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 N : ModuleCat R₃} (φ : M ⟶ N) {Z : ModuleCat R₁} (h : (restrictScalars gf).obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp ((restrictScalars f).map ((restrictScalars g).map φ)) (CategoryTheory.CategoryStruct.comp (restrictScalarsComp'App f g gf hgf N).inv h) = CategoryTheory.CategoryStruct.comp (restrictScalarsComp'App f g gf hgf M).inv (CategoryTheory.CategoryStruct.comp ((restrictScalars gf).map φ) h)

@[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₃) : restrictScalars (g.comp f) ≅ (restrictScalars g).comp (restrictScalars f)

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

noncomputable def ModuleCat.restrictScalarsEquivalenceOfRingEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (e : R ≃+* S) : ModuleCat S ≌ ModuleCat R

The equivalence of categories ModuleCat S ≌ ModuleCat R induced by e : R ≃+* S.

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

instance ModuleCat.instAdditiveRestrictScalars {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) : (restrictScalars f).Additive

instance ModuleCat.restrictScalarsEquivalenceOfRingEquiv_additive {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (e : R ≃+* S) : (restrictScalarsEquivalenceOfRingEquiv e).functor.Additive

instance ModuleCat.Algebra.instLinearRestrictScalars {R₀ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S] (f : R →ₐ[R₀] S) : CategoryTheory.Functor.Linear R₀ (restrictScalars f.toRingHom)

instance ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear {R₀ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S] (e : R ≃ₐ[R₀] S) : CategoryTheory.Functor.Linear R₀ (restrictScalarsEquivalenceOfRingEquiv e.toRingEquiv).functor

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

Tensor product of elements along a base change.

This notation is necessary because we need to reason about s ⊗ₜ m where s : S and m : M; without this notation, one needs to work with s : (restrictScalars f).obj ⟨S⟩.

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 turns an R-module into an S-module by M ↦ S ⨂ M

noncomputable def ModuleCat.ExtendScalars.map' {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {M1 M2 : ModuleCat R} (l : M1 ⟶ M2) : obj' f M1 ⟶ 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

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

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

@[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) (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 M' : ModuleCat R} (g : M ⟶ M') (s : S) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendScalars f).map g)) (s ⊗ₜ[R] m) = s ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) m

theorem ModuleCat.ExtendScalars.hom_ext {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] {f : R →+* S} {M : ModuleCat R} {N : ModuleCat S} {α β : (extendScalars f).obj M ⟶ N} (h : ∀ (m : ↑M), (CategoryTheory.ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom β) (1 ⊗ₜ[R] m)) : α = β

theorem ModuleCat.ExtendScalars.hom_ext_iff {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] {f : R →+* S} {M : ModuleCat R} {N : ModuleCat S} {α β : (extendScalars f).obj M ⟶ N} : α = β ↔ ∀ (m : ↑M), (CategoryTheory.ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom β) (1 ⊗ₜ[R] m)

@[implicit_reducible]

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 (↑((restrictScalars f).obj (of S 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)

@[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 : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M) (s' : S) : (s • g) s' = g (s' * s)

@[implicit_reducible]

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 (↑((restrictScalars f).obj (of S S)) →ₗ[R] M)

@[implicit_reducible]

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 (↑((restrictScalars f).obj (of S S)) →ₗ[R] M)

@[implicit_reducible]

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 (↑((restrictScalars f).obj (of S 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).

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)

@[implicit_reducible]

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

noncomputable def ModuleCat.CoextendScalars.map' {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat R} (g : M ⟶ M') : obj' f M ⟶ 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

@[simp]

theorem ModuleCat.CoextendScalars.map'_hom_apply_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat R} (g : M ⟶ M') (h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑M) (a✝ : ↑((restrictScalars f).obj (of S S))) : ((Hom.hom (map' f g)) h) a✝ = (Hom.hom g) (h a✝)

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.

@[implicit_reducible]

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

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

@[simp]

theorem ModuleCat.CoextendScalars.map_apply {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M M' : ModuleCat R} (g : M ⟶ M') (x : ↑((coextendScalars f).obj M)) (s : S) : ((CategoryTheory.ConcreteCategory.hom ((coextendScalars f).map g)) x) s = (CategoryTheory.ConcreteCategory.hom g) (x 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 : (restrictScalars f).obj Y ⟶ X) : Y ⟶ (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))

@[simp]

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

This should be autogenerated by @[simps] but we need to give s the correct type here.

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 ⟶ (coextendScalars f).obj X) : (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

@[simp]

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

This should be autogenerated by @[simps] but we need to give 1 the correct type here.

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

Auxiliary definition for unit', to address timeouts.

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

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

@[simp]

theorem ModuleCat.RestrictionCoextensionAdj.unit'_app {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (Y : ModuleCat S) : (RestrictionCoextensionAdj.unit' f).app Y = ofHom (app' f Y)

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

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

@[simp]

theorem ModuleCat.RestrictionCoextensionAdj.counit'_app {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) (X : ModuleCat R) : (RestrictionCoextensionAdj.counit' f).app X = ofHom { toFun := fun (g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))) => g.toFun 1, map_add' := ⋯, map_smul' := ⋯ }

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

Restriction of scalars is left adjoint to coextension of scalars.

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

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

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 : (extendScalars f).obj X ⟶ Y) : X ⟶ (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).

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_hom_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : (extendScalars f).obj X ⟶ Y) (x : ↑X) : (Hom.hom (toRestrictScalars f g)) x = (CategoryTheory.ConcreteCategory.hom 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 ⟶ (restrictScalars f).obj Y) : have this := Module.compHom (↑Y) f; ↑X →ₗ[R] ↑Y

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

@[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 ⟶ (restrictScalars f).obj Y) (x : ↑X) : (evalAt f s g) x = s • (CategoryTheory.ConcreteCategory.hom 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 ⟶ (restrictScalars f).obj Y) : (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.

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {X : ModuleCat R} {Y : ModuleCat S} (g : X ⟶ (restrictScalars f).obj Y) (z : TensorProduct R ↑((restrictScalars f).obj (of S S)) ↑X) : (Hom.hom (fromExtendScalars f g)) z = (TensorProduct.lift { toFun := fun (s : ↑((restrictScalars f).obj (of S S))) => 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} : ((extendScalars f).obj X ⟶ Y) ≃ (X ⟶ (restrictScalars f).obj Y)

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

@[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 ⟶ (restrictScalars f).obj Y) : (homEquiv f).symm g = 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 ⟶ ((extendScalars f).comp (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

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

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

@[simp]

theorem ModuleCat.ExtendRestrictScalarsAdj.unit_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (x✝ : ModuleCat R) : (unit f).app x✝ = 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} : ((restrictScalars f).comp (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

@[simp]

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

theorem ModuleCat.ExtendRestrictScalarsAdj.Counit.map_apply_one_tmul {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) {Y : ModuleCat S} (y : ↑Y) : (CategoryTheory.ConcreteCategory.hom (map f)) (1 ⊗ₜ[R] y) = y

noncomputable def ModuleCat.ExtendRestrictScalarsAdj.counit {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : (restrictScalars f).comp (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.

@[simp]

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

noncomputable def ModuleCat.extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) : extendScalars f ⊣ 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.

theorem ModuleCat.extendRestrictScalarsAdj_homEquiv_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] {f : R →+* S} {M : ModuleCat R} {N : ModuleCat S} (φ : (extendScalars f).obj M ⟶ N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (((extendRestrictScalarsAdj f).homEquiv M N) φ)) m = (CategoryTheory.ConcreteCategory.hom φ) (1 ⊗ₜ[R] m)

theorem ModuleCat.extendRestrictScalarsAdj_unit_app_apply {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (M : ModuleCat R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendRestrictScalarsAdj f).unit.app M)) m = 1 ⊗ₜ[R] m

@[simp]

theorem ModuleCat.extendRestrictScalarsAdj_counit_app_apply_one_tmul {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (M : ModuleCat S) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendRestrictScalarsAdj f).counit.app M)) (1 ⊗ₜ[R] m) = m

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

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

instance ModuleCat.preservesLimit_restrictScalars {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {J : Type u_3} [CategoryTheory.Category.{v_1, 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 (restrictScalars f)

instance ModuleCat.preservesColimit_restrictScalars {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) {J : Type u_3} [CategoryTheory.Category.{v_1, u_3} J] (F : CategoryTheory.Functor J (ModuleCat S)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat S) AddCommGrpCat))] : CategoryTheory.Limits.PreservesColimit F (restrictScalars f)

noncomputable def ModuleCat.extendScalarsId (R : Type u₁) [CommRing R] : extendScalars (RingHom.id R) ≅ CategoryTheory.Functor.id (ModuleCat R)

The extension of scalars by the identity of a ring is isomorphic to the identity functor.

theorem ModuleCat.extendScalarsId_inv_app_apply {R : Type u₁} [CommRing R] (M : ModuleCat R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendScalarsId R).inv.app M)) m = 1 ⊗ₜ[R] m

theorem ModuleCat.homEquiv_extendScalarsId {R : Type u₁} [CommRing R] (M : ModuleCat R) : ((extendRestrictScalarsAdj (RingHom.id R)).homEquiv M ((CategoryTheory.Functor.id (ModuleCat R)).obj M)) ((extendScalarsId R).hom.app M) = (restrictScalarsId R).inv.app M

theorem ModuleCat.extendScalarsId_hom_app_one_tmul {R : Type u₁} [CommRing R] (M : ModuleCat R) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendScalarsId R).hom.app M)) (1 ⊗ₜ[R] m) = m

noncomputable def ModuleCat.extendScalarsComp {R₁ R₂ R₃ : Type u₁} [CommRing R₁] [CommRing R₂] [CommRing R₃] (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) : extendScalars (f₂₃.comp f₁₂) ≅ (extendScalars f₁₂).comp (extendScalars f₂₃)

The extension of scalars by a composition of commutative ring morphisms identifies to the composition of the extension of scalars functors.

theorem ModuleCat.homEquiv_extendScalarsComp {R₁ R₂ R₃ : Type u₁} [CommRing R₁] [CommRing R₂] [CommRing R₃] (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (M : ModuleCat R₁) : ((extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M (((extendScalars f₁₂).comp (extendScalars f₂₃)).obj M)) ((extendScalarsComp f₁₂ f₂₃).hom.app M) = CategoryTheory.CategoryStruct.comp ((extendRestrictScalarsAdj f₁₂).unit.app M) (CategoryTheory.CategoryStruct.comp ((restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M))) ((restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))))

theorem ModuleCat.extendScalarsComp_hom_app_one_tmul {R₁ R₂ R₃ : Type u₁} [CommRing R₁] [CommRing R₂] [CommRing R₃] (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (M : ModuleCat R₁) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)

theorem ModuleCat.extendScalars_assoc {R₁ R₂ R₃ R₄ : Type u₁} [CommRing R₁] [CommRing R₂] [CommRing R₃] [CommRing R₄] (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (f₃₄ : R₃ →+* R₄) : CategoryTheory.CategoryStruct.comp (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom (CategoryTheory.Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)) = CategoryTheory.CategoryStruct.comp (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom (CategoryTheory.CategoryStruct.comp ((extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom) ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv)

theorem ModuleCat.extendScalars_assoc_assoc {R₁ R₂ R₃ R₄ : Type u₁} [CommRing R₁] [CommRing R₂] [CommRing R₃] [CommRing R₄] (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (f₃₄ : R₃ →+* R₄) {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₄)} (h : ((extendScalars f₁₂).comp (extendScalars f₂₃)).comp (extendScalars f₃₄) ⟶ Z) : CategoryTheory.CategoryStruct.comp (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)) h) = CategoryTheory.CategoryStruct.comp (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom (CategoryTheory.CategoryStruct.comp ((extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom) (CategoryTheory.CategoryStruct.comp ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv h))

theorem ModuleCat.extendScalars_assoc' {R₁ R₂ R₃ R₄ : Type u₁} [CommRing R₁] [CommRing R₂] [CommRing R₃] [CommRing R₄] (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (f₃₄ : R₃ →+* R₄) : CategoryTheory.CategoryStruct.comp (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)) (CategoryTheory.CategoryStruct.comp ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom (CategoryTheory.CategoryStruct.comp ((extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).inv) (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv))) = CategoryTheory.CategoryStruct.id (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

The associativity compatibility for the extension of scalars, in the exact form that is needed in the definition CommRingCat.moduleCatExtendScalarsPseudofunctor in the file Mathlib/Algebra/Category/ModuleCat/Pseudofunctor.lean

theorem ModuleCat.extendScalars_id_comp {R₁ R₂ : Type u₁} [CommRing R₁] [CommRing R₂] (f₁₂ : R₁ →+* R₂) : CategoryTheory.CategoryStruct.comp (extendScalarsComp (RingHom.id R₁) f₁₂).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂)) (extendScalars f₁₂).leftUnitor.hom) = CategoryTheory.CategoryStruct.id (extendScalars (f₁₂.comp (RingHom.id R₁)))

theorem ModuleCat.extendScalars_id_comp_assoc {R₁ R₂ : Type u₁} [CommRing R₁] [CommRing R₂] (f₁₂ : R₁ →+* R₂) {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₂)} (h : extendScalars f₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (extendScalarsComp (RingHom.id R₁) f₁₂).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂)) (CategoryTheory.CategoryStruct.comp (extendScalars f₁₂).leftUnitor.hom h)) = h

theorem ModuleCat.extendScalars_comp_id {R₁ R₂ : Type u₁} [CommRing R₁] [CommRing R₂] (f₁₂ : R₁ →+* R₂) : CategoryTheory.CategoryStruct.comp (extendScalarsComp f₁₂ (RingHom.id R₂)).hom (CategoryTheory.CategoryStruct.comp ((extendScalars f₁₂).whiskerLeft (extendScalarsId R₂).hom) (extendScalars f₁₂).rightUnitor.hom) = CategoryTheory.CategoryStruct.id (extendScalars ((RingHom.id R₂).comp f₁₂))

theorem ModuleCat.extendScalars_comp_id_assoc {R₁ R₂ : Type u₁} [CommRing R₁] [CommRing R₂] (f₁₂ : R₁ →+* R₂) {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₂)} (h : extendScalars f₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (extendScalarsComp f₁₂ (RingHom.id R₂)).hom (CategoryTheory.CategoryStruct.comp ((extendScalars f₁₂).whiskerLeft (extendScalarsId R₂).hom) (CategoryTheory.CategoryStruct.comp (extendScalars f₁₂).rightUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (extendScalars ((RingHom.id R₂).comp f₁₂))) h