Change Of Rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

category_theory.Module.restrict_scalars: given rings R, S and a ring homomorphism R ⟶ S, then restrict_scalars : Module S ⥤ Module R is defined by M ↦ M where M : S-module is seen as R-module by r • m := f r • m and S-linear map l : M ⟶ M' is R-linear as well.
category_theory.Module.extend_scalars: given commutative rings R, S and ring homomorphism f : R ⟶ S, then extend_scalars : Module R ⥤ Module 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'.
category_theory.Module.coextend_scalars: given rings R, S and a ring homomorphism R ⟶ S then coextend_scalars : Module R ⥤ Module S is defined by M ↦ (S →ₗ[R] M) where S is seen as R-module by restriction of scalars and l ↦ l ∘ _.

Main results #

category_theory.Module.extend_restrict_scalars_adj: given commutative rings R, S and a ring homomorphism f : R →+* S, the extension and restriction of scalars by f are adjoint functors.
category_theory.Module.restrict_coextend_scalars_adj: given rings R, S and a ring homomorphism f : R ⟶ S then coextend_scalars f is the right adjoint of restrict_scalars 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.

source

def category_theory.Module.restrict_scalars.obj' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module S) :

Module 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.comp_hom). This is called restriction of scalars.

Equations

category_theory.Module.restrict_scalars.obj' f M = Module.mk ↥M

source

def category_theory.Module.restrict_scalars.map' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module S} (g : M ⟶ M') :

category_theory.Module.restrict_scalars.obj' f M ⟶ category_theory.Module.restrict_scalars.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

category_theory.Module.restrict_scalars.map' f g = {to_fun := g.to_fun, map_add' := _, map_smul' := _}

source

def category_theory.Module.restrict_scalars {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

Module S ⥤ Module 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

category_theory.Module.restrict_scalars f = {obj := category_theory.Module.restrict_scalars.obj' f, map := λ (_x _x_1 : Module S), category_theory.Module.restrict_scalars.map' f, map_id' := _, map_comp' := _}

Instances for category_theory.Module.restrict_scalars

source

@[protected, instance]

def category_theory.Module.restrict_scalars.category_theory.faithful {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

category_theory.faithful (category_theory.Module.restrict_scalars f)

source

@[simp]

theorem category_theory.Module.restrict_scalars.map_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module S} (g : M ⟶ M') (x : ↥((category_theory.Module.restrict_scalars f).obj M)) :

⇑((category_theory.Module.restrict_scalars f).map g) x = ⇑g x

source

@[simp]

theorem category_theory.Module.restrict_scalars.smul_def {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M : Module S} (r : R) (m : ↥((category_theory.Module.restrict_scalars f).obj M)) :

r • m = ⇑f r • m

source

theorem category_theory.Module.restrict_scalars.smul_def' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M : Module S} (r : R) (m : ↥M) :

r • m = ⇑f r • m

source

@[protected, instance]

def category_theory.Module.smul_comm_class_mk {R : Type u₁} {S : Type u₂} [ring R] [comm_ring S] (f : R →+* S) (M : Type v) [add_comm_group M] [module S M] :

smul_comm_class R S M

source

def category_theory.Module.extend_scalars.obj' {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (M : Module R) :

Module S

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

Equations

category_theory.Module.extend_scalars.obj' f M = Module.mk (tensor_product R ↥((category_theory.Module.restrict_scalars f).obj (Module.mk S)) ↥M)

source

def category_theory.Module.extend_scalars.map' {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M1 M2 : Module R} (l : M1 ⟶ M2) :

category_theory.Module.extend_scalars.obj' f M1 ⟶ category_theory.Module.extend_scalars.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

category_theory.Module.extend_scalars.map' f l = linear_map.base_change S l

source

theorem category_theory.Module.extend_scalars.map'_id {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M : Module R} :

category_theory.Module.extend_scalars.map' f (𝟙 M) = 𝟙 (category_theory.Module.extend_scalars.obj' f M)

source

theorem category_theory.Module.extend_scalars.map'_comp {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M₁ M₂ M₃ : Module R} (l₁₂ : M₁ ⟶ M₂) (l₂₃ : M₂ ⟶ M₃) :

category_theory.Module.extend_scalars.map' f (l₁₂ ≫ l₂₃) = category_theory.Module.extend_scalars.map' f l₁₂ ≫ category_theory.Module.extend_scalars.map' f l₂₃

source

def category_theory.Module.extend_scalars {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

Module R ⥤ Module 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

category_theory.Module.extend_scalars f = {obj := λ (M : Module R), category_theory.Module.extend_scalars.obj' f M, map := λ (M1 M2 : Module R) (l : M1 ⟶ M2), category_theory.Module.extend_scalars.map' f l, map_id' := _, map_comp' := _}

Instances for category_theory.Module.extend_scalars

category_theory.Module.extend_scalars.category_theory.is_left_adjoint

source

@[protected, simp]

theorem category_theory.Module.extend_scalars.smul_tmul {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M : Module R} (s s' : S) (m : ↥M) :

s • s' ⊗ₜ[R] m = (s * s') ⊗ₜ[R] m

source

@[simp]

theorem category_theory.Module.extend_scalars.map_tmul {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {M M' : Module R} (g : M ⟶ M') (s : S) (m : ↥M) :

⇑((category_theory.Module.extend_scalars f).map g) (s ⊗ₜ[R] m) = s ⊗ₜ[R] ⇑g m

source

@[protected, instance]

def category_theory.Module.coextend_scalars.has_smul {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [add_comm_monoid M] [module R M] :

has_smul S (↥((category_theory.Module.restrict_scalars f).obj (Module.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

category_theory.Module.coextend_scalars.has_smul f M = {smul := λ (s : S) (g : ↥((category_theory.Module.restrict_scalars f).obj (Module.mk S)) →ₗ[R] M), {to_fun := λ (s' : S), ⇑g (s' * s), map_add' := _, map_smul' := _}}

source

@[simp]

theorem category_theory.Module.coextend_scalars.smul_apply' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [add_comm_monoid M] [module R M] (s : S) (g : ↥((category_theory.Module.restrict_scalars f).obj (Module.mk S)) →ₗ[R] M) (s' : S) :

⇑(s • g) s' = ⇑g (s' * s)

source

@[protected, instance]

def category_theory.Module.coextend_scalars.mul_action {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [add_comm_monoid M] [module R M] :

mul_action S (↥((category_theory.Module.restrict_scalars f).obj (Module.mk S)) →ₗ[R] M)

Equations

category_theory.Module.coextend_scalars.mul_action f M = {to_has_smul := {smul := has_smul.smul (category_theory.Module.coextend_scalars.has_smul f M)}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def category_theory.Module.coextend_scalars.distrib_mul_action {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [add_comm_monoid M] [module R M] :

distrib_mul_action S (↥((category_theory.Module.restrict_scalars f).obj (Module.mk S)) →ₗ[R] M)

Equations

category_theory.Module.coextend_scalars.distrib_mul_action f M = {to_mul_action := {to_has_smul := mul_action.to_has_smul (category_theory.Module.coextend_scalars.mul_action f M), one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}

source

@[protected, instance]

def category_theory.Module.coextend_scalars.is_module {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Type v) [add_comm_monoid M] [module R M] :

module S (↥((category_theory.Module.restrict_scalars f).obj (Module.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

category_theory.Module.coextend_scalars.is_module f M = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action (category_theory.Module.coextend_scalars.distrib_mul_action f M), smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}

source

def category_theory.Module.coextend_scalars.obj' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module R) :

Module 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

category_theory.Module.coextend_scalars.obj' f M = Module.mk (↥((category_theory.Module.restrict_scalars f).obj (Module.mk S)) →ₗ[R] ↥M)

Instances for ↥category_theory.Module.coextend_scalars.obj'

category_theory.Module.coextend_scalars.obj'.has_coe_to_fun

source

@[protected, instance]

def category_theory.Module.coextend_scalars.obj'.has_coe_to_fun {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module R) :

has_coe_to_fun ↥(category_theory.Module.coextend_scalars.obj' f M) (λ (g : ↥(category_theory.Module.coextend_scalars.obj' f M)), S → ↥M)

Equations

category_theory.Module.coextend_scalars.obj'.has_coe_to_fun f M = {coe := λ (g : ↥(category_theory.Module.coextend_scalars.obj' f M)), g.to_fun}

source

@[simp]

theorem category_theory.Module.coextend_scalars.map'_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module R} (g : M ⟶ M') (h : ↥(category_theory.Module.coextend_scalars.obj' f M)) :

⇑(category_theory.Module.coextend_scalars.map' f g) h = linear_map.comp g h

source

def category_theory.Module.coextend_scalars.map' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module R} (g : M ⟶ M') :

category_theory.Module.coextend_scalars.obj' f M ⟶ category_theory.Module.coextend_scalars.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

category_theory.Module.coextend_scalars.map' f g = {to_fun := λ (h : ↥(category_theory.Module.coextend_scalars.obj' f M)), linear_map.comp g h, map_add' := _, map_smul' := _}

source

def category_theory.Module.coextend_scalars {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

Module R ⥤ Module 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

category_theory.Module.coextend_scalars f = {obj := category_theory.Module.coextend_scalars.obj' f, map := λ (_x _x_1 : Module R), category_theory.Module.coextend_scalars.map' f, map_id' := _, map_comp' := _}

Instances for category_theory.Module.coextend_scalars

category_theory.Module.coextend_scalars.category_theory.is_right_adjoint

source

@[protected, instance]

def category_theory.Module.coextend_scalars.obj.has_coe_to_fun {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module R) :

has_coe_to_fun ↥((category_theory.Module.coextend_scalars f).obj M) (λ (g : ↥((category_theory.Module.coextend_scalars f).obj M)), S → ↥M)

Equations

category_theory.Module.coextend_scalars.obj.has_coe_to_fun f M = infer_instance

source

theorem category_theory.Module.coextend_scalars.smul_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (M : Module R) (g : ↥((category_theory.Module.coextend_scalars f).obj M)) (s s' : S) :

⇑(s • g) s' = ⇑g (s' * s)

source

@[simp]

theorem category_theory.Module.coextend_scalars.map_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {M M' : Module R} (g : M ⟶ M') (x : ↥((category_theory.Module.coextend_scalars f).obj M)) (s : S) :

⇑(⇑((category_theory.Module.coextend_scalars f).map g) x) s = ⇑g (⇑x s)

source

@[simp]

theorem category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction_apply_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : (category_theory.Module.restrict_scalars f).obj Y ⟶ X) (y : ↥Y) (s : S) :

⇑(⇑(category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction f g) y) s = ⇑g (s • y)

source

def category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : (category_theory.Module.restrict_scalars f).obj Y ⟶ X) :

Y ⟶ (category_theory.Module.coextend_scalars f).obj X

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

Equations

category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction f g = {to_fun := λ (y : ↥Y), {to_fun := λ (s : S), ⇑g (s • y), map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}

source

@[simp]

theorem category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : Y ⟶ (category_theory.Module.coextend_scalars f).obj X) (y : ↥Y) :

⇑(category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction f g) y = (⇑g y).to_fun 1

source

def category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : Y ⟶ (category_theory.Module.coextend_scalars f).obj X) :

(category_theory.Module.restrict_scalars f).obj Y ⟶ X

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

Equations

category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction f g = {to_fun := λ (y : ↥Y), (⇑g y).to_fun 1, map_add' := _, map_smul' := _}

source

@[simp]

theorem category_theory.Module.restriction_coextension_adj.unit'_app_apply_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (Y : Module S) (y : ↥Y) (s : S) :

⇑(⇑((category_theory.Module.restriction_coextension_adj.unit' f).app Y) y) s = s • y

source

@[protected]

def category_theory.Module.restriction_coextension_adj.unit' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

𝟭 (Module S) ⟶ category_theory.Module.restrict_scalars f ⋙ category_theory.Module.coextend_scalars f

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

Equations

category_theory.Module.restriction_coextension_adj.unit' f = {app := λ (Y : Module S), {to_fun := λ (y : ↥Y), {to_fun := λ (s : S), s • y, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}, naturality' := _}

source

@[simp]

theorem category_theory.Module.restriction_coextension_adj.counit'_app_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (X : Module R) (g : ↥((category_theory.Module.coextend_scalars f ⋙ category_theory.Module.restrict_scalars f).obj X)) :

⇑((category_theory.Module.restriction_coextension_adj.counit' f).app X) g = g.to_fun 1

source

@[protected]

def category_theory.Module.restriction_coextension_adj.counit' {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

category_theory.Module.coextend_scalars f ⋙ category_theory.Module.restrict_scalars f ⟶ 𝟭 (Module R)

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

Equations

category_theory.Module.restriction_coextension_adj.counit' f = {app := λ (X : Module R), {to_fun := λ (g : ↥((category_theory.Module.coextend_scalars f ⋙ category_theory.Module.restrict_scalars f).obj X)), g.to_fun 1, map_add' := _, map_smul' := _}, naturality' := _}

source

@[simp]

theorem category_theory.Module.restrict_coextend_scalars_adj_unit {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

(category_theory.Module.restrict_coextend_scalars_adj f).unit = category_theory.Module.restriction_coextension_adj.unit' f

source

@[simp]

theorem category_theory.Module.restrict_coextend_scalars_adj_counit {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

(category_theory.Module.restrict_coextend_scalars_adj f).counit = category_theory.Module.restriction_coextension_adj.counit' f

source

@[simp]

theorem category_theory.Module.restrict_coextend_scalars_adj_hom_equiv_symm_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (X : Module S) (Y : Module R) (g : X ⟶ (category_theory.Module.coextend_scalars f).obj Y) :

⇑(((category_theory.Module.restrict_coextend_scalars_adj f).hom_equiv X Y).symm) g = category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction f g

source

def category_theory.Module.restrict_coextend_scalars_adj {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

category_theory.Module.restrict_scalars f ⊣ category_theory.Module.coextend_scalars f

Restriction of scalars is left adjoint to coextension of scalars.

Equations

category_theory.Module.restrict_coextend_scalars_adj f = {hom_equiv := λ (X : Module S) (Y : Module R), {to_fun := category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction f X, inv_fun := category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction f X, left_inv := _, right_inv := _}, unit := category_theory.Module.restriction_coextension_adj.unit' f, counit := category_theory.Module.restriction_coextension_adj.counit' f, hom_equiv_unit' := _, hom_equiv_counit' := _}

source

@[simp]

theorem category_theory.Module.restrict_coextend_scalars_adj_hom_equiv_apply {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) (X : Module S) (Y : Module R) (g : (category_theory.Module.restrict_scalars f).obj X ⟶ Y) :

⇑((category_theory.Module.restrict_coextend_scalars_adj f).hom_equiv X Y) g = category_theory.Module.restriction_coextension_adj.hom_equiv.from_restriction f g

source

@[protected, instance]

def category_theory.Module.restrict_scalars.category_theory.is_left_adjoint {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

category_theory.is_left_adjoint (category_theory.Module.restrict_scalars f)

Equations

category_theory.Module.restrict_scalars.category_theory.is_left_adjoint f = {right := category_theory.Module.coextend_scalars f, adj := category_theory.Module.restrict_coextend_scalars_adj f}

source

@[protected, instance]

def category_theory.Module.coextend_scalars.category_theory.is_right_adjoint {R : Type u₁} {S : Type u₂} [ring R] [ring S] (f : R →+* S) :

category_theory.is_right_adjoint (category_theory.Module.coextend_scalars f)

Equations

category_theory.Module.coextend_scalars.category_theory.is_right_adjoint f = {left := category_theory.Module.restrict_scalars f, adj := category_theory.Module.restrict_coextend_scalars_adj f}

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : (category_theory.Module.extend_scalars f).obj X ⟶ Y) (x : ↥X) :

⇑(category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars f g) x = ⇑g (1 ⊗ₜ[R] x)

source

def category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : (category_theory.Module.extend_scalars f).obj X ⟶ Y) :

X ⟶ (category_theory.Module.restrict_scalars f).obj Y

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

Equations

category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars f g = {to_fun := λ (x : ↥X), ⇑g (1 ⊗ₜ[R] x), map_add' := _, map_smul' := _}

source

def category_theory.Module.extend_restrict_scalars_adj.hom_equiv.from_extend_scalars {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : X ⟶ (category_theory.Module.restrict_scalars f).obj Y) :

(category_theory.Module.extend_scalars f).obj X ⟶ Y

Given R-module X and S-module Y and a map X ⟶ (restrict_scalars 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

category_theory.Module.extend_restrict_scalars_adj.hom_equiv.from_extend_scalars f g = let m1 : module R S := module.comp_hom S f, m2 : module R ↥Y := module.comp_hom ↥Y f in {to_fun := λ (z : ↥((category_theory.Module.extend_scalars f).obj X)), ⇑(tensor_product.lift {to_fun := λ (s : ↥((category_theory.Module.restrict_scalars f).obj (Module.mk S))), {to_fun := λ (x : ↥X), s • ⇑g x, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}) z, map_add' := _, map_smul' := _}

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv.from_extend_scalars_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : X ⟶ (category_theory.Module.restrict_scalars f).obj Y) (z : ↥((category_theory.Module.extend_scalars f).obj X)) :

⇑(category_theory.Module.extend_restrict_scalars_adj.hom_equiv.from_extend_scalars f g) z = ⇑(tensor_product.lift {to_fun := λ (s : ↥((category_theory.Module.restrict_scalars f).obj (Module.mk S))), {to_fun := λ (x : ↥X), s • ⇑g x, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}) z

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv_symm_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : X ⟶ (category_theory.Module.restrict_scalars f).obj Y) :

⇑((category_theory.Module.extend_restrict_scalars_adj.hom_equiv f).symm) g = category_theory.Module.extend_restrict_scalars_adj.hom_equiv.from_extend_scalars f g

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.hom_equiv_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} (g : (category_theory.Module.extend_scalars f).obj X ⟶ Y) :

⇑(category_theory.Module.extend_restrict_scalars_adj.hom_equiv f) g = category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars f g

source

def category_theory.Module.extend_restrict_scalars_adj.hom_equiv {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} {Y : Module S} :

((category_theory.Module.extend_scalars f).obj X ⟶ Y) ≃ (X ⟶ (category_theory.Module.restrict_scalars f).obj Y)

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

Equations

category_theory.Module.extend_restrict_scalars_adj.hom_equiv f = {to_fun := category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars f Y, inv_fun := category_theory.Module.extend_restrict_scalars_adj.hom_equiv.from_extend_scalars f Y, left_inv := _, right_inv := _}

source

def category_theory.Module.extend_restrict_scalars_adj.unit.map {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} :

X ⟶ (category_theory.Module.extend_scalars f ⋙ category_theory.Module.restrict_scalars 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

category_theory.Module.extend_restrict_scalars_adj.unit.map f = {to_fun := λ (x : ↥X), 1 ⊗ₜ[R] x, map_add' := _, map_smul' := _}

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.unit.map_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {X : Module R} (x : ↥X) :

⇑(category_theory.Module.extend_restrict_scalars_adj.unit.map f) x = 1 ⊗ₜ[R] x

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.unit_app {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (_x : Module R) :

(category_theory.Module.extend_restrict_scalars_adj.unit f).app _x = category_theory.Module.extend_restrict_scalars_adj.unit.map f

source

def category_theory.Module.extend_restrict_scalars_adj.unit {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

𝟭 (Module R) ⟶ category_theory.Module.extend_scalars f ⋙ category_theory.Module.restrict_scalars f

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

Equations

category_theory.Module.extend_restrict_scalars_adj.unit f = {app := λ (_x : Module R), category_theory.Module.extend_restrict_scalars_adj.unit.map f, naturality' := _}

source

def category_theory.Module.extend_restrict_scalars_adj.counit.map {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {Y : Module S} :

(category_theory.Module.restrict_scalars f ⋙ category_theory.Module.extend_scalars 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

category_theory.Module.extend_restrict_scalars_adj.counit.map f = let m1 : module R S := module.comp_hom S f, m2 : module R ↥Y := module.comp_hom ↥Y f in {to_fun := ⇑(tensor_product.lift {to_fun := λ (s : S), {to_fun := λ (y : ↥Y), s • y, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}), map_add' := _, map_smul' := _}

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.counit.map_apply {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) {Y : Module S} (ᾰ : tensor_product R S ↥Y) :

⇑(category_theory.Module.extend_restrict_scalars_adj.counit.map f) ᾰ = ⇑(tensor_product.lift {to_fun := λ (s : S), {to_fun := λ (y : ↥Y), s • y, map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}) ᾰ

source

def category_theory.Module.extend_restrict_scalars_adj.counit {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

category_theory.Module.restrict_scalars f ⋙ category_theory.Module.extend_scalars f ⟶ 𝟭 (Module S)

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

Equations

category_theory.Module.extend_restrict_scalars_adj.counit f = {app := λ (_x : Module S), category_theory.Module.extend_restrict_scalars_adj.counit.map f, naturality' := _}

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj.counit_app {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (_x : Module S) :

(category_theory.Module.extend_restrict_scalars_adj.counit f).app _x = category_theory.Module.extend_restrict_scalars_adj.counit.map f

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj_hom_equiv {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) (_x : Module R) (_x_1 : Module S) :

(category_theory.Module.extend_restrict_scalars_adj f).hom_equiv _x _x_1 = category_theory.Module.extend_restrict_scalars_adj.hom_equiv f

source

def category_theory.Module.extend_restrict_scalars_adj {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

category_theory.Module.extend_scalars f ⊣ category_theory.Module.restrict_scalars 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

category_theory.Module.extend_restrict_scalars_adj f = {hom_equiv := λ (_x : Module R) (_x_1 : Module S), category_theory.Module.extend_restrict_scalars_adj.hom_equiv f, unit := category_theory.Module.extend_restrict_scalars_adj.unit f, counit := category_theory.Module.extend_restrict_scalars_adj.counit f, hom_equiv_unit' := _, hom_equiv_counit' := _}

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj_unit {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

(category_theory.Module.extend_restrict_scalars_adj f).unit = category_theory.Module.extend_restrict_scalars_adj.unit f

source

@[simp]

theorem category_theory.Module.extend_restrict_scalars_adj_counit {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

(category_theory.Module.extend_restrict_scalars_adj f).counit = category_theory.Module.extend_restrict_scalars_adj.counit f

source

@[protected, instance]

def category_theory.Module.extend_scalars.category_theory.is_left_adjoint {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

category_theory.is_left_adjoint (category_theory.Module.extend_scalars f)

Equations

category_theory.Module.extend_scalars.category_theory.is_left_adjoint f = {right := category_theory.Module.restrict_scalars f, adj := category_theory.Module.extend_restrict_scalars_adj f}

source

@[protected, instance]

def category_theory.Module.restrict_scalars.category_theory.is_right_adjoint {R : Type u₁} {S : Type u₂} [comm_ring R] [comm_ring S] (f : R →+* S) :

category_theory.is_right_adjoint (category_theory.Module.restrict_scalars f)

Equations

category_theory.Module.restrict_scalars.category_theory.is_right_adjoint f = {left := category_theory.Module.extend_scalars f, adj := category_theory.Module.extend_restrict_scalars_adj f}