Tensor products and finitely generated submodules

Various results about how tensor products of arbitrary modules are direct limits of tensor products of finitely-generated modules.

Main definitions

• Submodule.FG.directedSystem, the directed system of finitely generated submodules of a module.

• Submodule.FG.directLimit proves that a module is the direct limit of its finitely generated submodules, with respect to the inclusion maps

• DirectedSystem.rTensor, the directed system deduced from a directed system of modules by applying rTensor.

• Submodule.FG.rTensor.directSystem, the directed system of modules P ⊗[R] N, for all finitely generated submodules P, with respect to the maps deduced from the inclusions

• Submodule.FG.rTensor.directLimit : a tensor product M ⊗[R] N is the direct limit of the modules P ⊗[R] N, where P ranges over all finitely generated submodules of M, as a linear equivalence.

• DirectedSystem.lTensor, the directed system deduced from a directed system of modules by applying lTensor.

• Submodule.FG.lTensor.directSystem, the directed system of modules M ⊗[R] Q, for all finitely generated submodules Q, with respect to the maps deduced from the inclusions

• Submodule.FG.lTensor.directLimit : a tensor product M ⊗[R] N is the direct limit of the modules M ⊗[R] Q, where Q ranges over all finitely generated submodules of N, as a linear equivalence.

instance Submodule.FG.directedSystem {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] : DirectedSystem (fun (P : { P : Submodule R M // P.FG }) => ↥↑P) fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) => ⇑(inclusion h)

The directed system of finitely generated submodules of M

noncomputable def Submodule.FG.directLimit (R : Type u) [Semiring R] (M : Type u_1) [AddCommMonoid M] [Module R M] [DecidableEq { P : Submodule R M // P.FG }] : (Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) => ↥↑P) fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) => inclusion h) ≃ₗ[R] M

Any module is the direct limit of its finitely generated submodules

Equations

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

theorem DirectedSystem.rTensor (R : Type u) (N : Type u_2) [CommSemiring R] [AddCommMonoid N] [Module R N] {ι : Type u_3} [Preorder ι] {F : ι → Type u_4} [(i : ι) → AddCommMonoid (F i)] [(i : ι) → Module R (F i)] {f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j} (D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f h)) : DirectedSystem (fun (i : ι) => TensorProduct R (F i) N) fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(LinearMap.rTensor N (f h))

Given a directed system of R-modules, tensoring it on the right gives a directed system

theorem Submodule.FG.rTensor.directedSystem (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : DirectedSystem (fun (P : { P : Submodule R M // P.FG }) => TensorProduct R (↥↑P) N) fun ⦃x x_1 : { P : Submodule R M // P.FG }⦄ (h : x ≤ x_1) => ⇑(LinearMap.rTensor N (inclusion h))

When P ranges over finitely generated submodules of M, the modules of the form P ⊗[R] N form a directed system.

noncomputable def Submodule.FG.rTensor.directLimit (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq { P : Submodule R M // P.FG }] : (Module.DirectLimit (fun (P : { P : Submodule R M // P.FG }) => TensorProduct R (↥↑P) N) fun ⦃P Q : { P : Submodule R M // P.FG }⦄ (h : P ≤ Q) => LinearMap.rTensor N (inclusion h)) ≃ₗ[R] TensorProduct R M N

A tensor product M ⊗[R] N is the direct limit of the modules P ⊗[R] N, where P ranges over all finitely generated submodules of M, as a linear equivalence.

Equations

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

theorem Submodule.FG.rTensor.directLimit_apply (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq { P : Submodule R M // P.FG }] {P : { P : Submodule R M // P.FG }} (u : TensorProduct R (↥↑P) N) : (directLimit R M N) ((Module.DirectLimit.of R { P : Submodule R M // P.FG } (fun (P : { P : Submodule R M // P.FG }) => TensorProduct R (↥↑P) N) (fun ⦃x x_1 : { P : Submodule R M // P.FG }⦄ (h : x ≤ x_1) => LinearMap.rTensor N (inclusion h)) P) u) = (LinearMap.rTensor N (↑P).subtype) u

theorem Submodule.FG.rTensor.directLimit_apply' (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq { P : Submodule R M // P.FG }] {P : Submodule R M} (hP : P.FG) (u : TensorProduct R (↥P) N) : (directLimit R M N) ((Module.DirectLimit.of R { P : Submodule R M // P.FG } (fun (P : { P : Submodule R M // P.FG }) => TensorProduct R (↥↑P) N) (fun ⦃x x_1 : { P : Submodule R M // P.FG }⦄ (h : x ≤ x_1) => LinearMap.rTensor N (inclusion h)) ⟨P, hP⟩) u) = (LinearMap.rTensor N P.subtype) u

An alternative version to Submodule.FG.rTensor.directLimit_apply.

theorem DirectedSystem.lTensor (R : Type u) (M : Type u_1) [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [Preorder ι] {F : ι → Type u_4} [(i : ι) → AddCommMonoid (F i)] [(i : ι) → Module R (F i)] {f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j} (D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f h)) : DirectedSystem (fun (i : ι) => TensorProduct R M (F i)) fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(LinearMap.lTensor M (f h))

Given a directed system of R-modules, tensoring it on the left gives a directed system

theorem Submodule.FG.lTensor.directedSystem (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : DirectedSystem (fun (Q : { Q : Submodule R N // Q.FG }) => TensorProduct R M ↥↑Q) fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) => ⇑(LinearMap.lTensor M (inclusion hPQ))

When Q ranges over finitely generated submodules of N, the modules of the form M ⊗[R] Q form a directed system.

noncomputable def Submodule.FG.lTensor.directLimit (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq { Q : Submodule R N // Q.FG }] : (Module.DirectLimit (fun (Q : { Q : Submodule R N // Q.FG }) => TensorProduct R M ↥↑Q) fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) => LinearMap.lTensor M (inclusion hPQ)) ≃ₗ[R] TensorProduct R M N

A tensor product M ⊗[R] N is the direct limit of the modules M ⊗[R] Q, where Q ranges over all finitely generated submodules of N, as a linear equivalence.

Equations

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

theorem Submodule.FG.lTensor.directLimit_apply (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq { P : Submodule R N // P.FG }] (Q : { Q : Submodule R N // Q.FG }) (u : TensorProduct R M ↥↑Q) : (directLimit R M N) ((Module.DirectLimit.of R { Q : Submodule R N // Q.FG } (fun (Q : { Q : Submodule R N // Q.FG }) => TensorProduct R M ↥↑Q) (fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) => LinearMap.lTensor M (inclusion hPQ)) Q) u) = (LinearMap.lTensor M (↑Q).subtype) u

theorem Submodule.FG.lTensor.directLimit_apply' (R : Type u) (M : Type u_1) (N : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [DecidableEq { Q : Submodule R N // Q.FG }] (Q : Submodule R N) (hQ : Q.FG) (u : TensorProduct R M ↥Q) : (directLimit R M N) ((Module.DirectLimit.of R { Q : Submodule R N // Q.FG } (fun (Q : { Q : Submodule R N // Q.FG }) => TensorProduct R M ↥↑Q) (fun (x x_1 : { Q : Submodule R N // Q.FG }) (hPQ : x ≤ x_1) => LinearMap.lTensor M (inclusion hPQ)) ⟨Q, hQ⟩) u) = (LinearMap.lTensor M Q.subtype) u

theorem TensorProduct.exists_of_fg {R : Type u} {M : Type u_1} {N : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (u : TensorProduct R M N) [DecidableEq { P : Submodule R M // P.FG }] : ∃ (P : Submodule R M), P.FG ∧ u ∈ LinearMap.range (LinearMap.rTensor N P.subtype)

theorem TensorProduct.eq_of_fg_of_subtype_eq {R : Type u} {M : Type u_1} {N : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {P : Submodule R M} (hP : P.FG) {t t' : TensorProduct R (↥P) N} (h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P.subtype) t') : ∃ (Q : Submodule R M) (hPQ : P ≤ Q), Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hPQ)) t'

theorem TensorProduct.eq_zero_of_fg_of_subtype_eq_zero {R : Type u} {M : Type u_1} {N : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {P : Submodule R M} (hP : P.FG) {t : TensorProduct R (↥P) N} (h : (LinearMap.rTensor N P.subtype) t = 0) : ∃ (Q : Submodule R M) (hPQ : P ≤ Q), Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = 0

theorem TensorProduct.eq_of_fg_of_subtype_eq' {R : Type u} {M : Type u_1} {N : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {P : Submodule R M} (hP : P.FG) {t : TensorProduct R (↥P) N} {P' : Submodule R M} (hP' : P'.FG) {t' : TensorProduct R (↥P') N} (h : (LinearMap.rTensor N P.subtype) t = (LinearMap.rTensor N P'.subtype) t') : ∃ (Q : Submodule R M) (hPQ : P ≤ Q) (hP'Q : P' ≤ Q), Q.FG ∧ (LinearMap.rTensor N (Submodule.inclusion hPQ)) t = (LinearMap.rTensor N (Submodule.inclusion hP'Q)) t'

theorem TensorProduct.Algebra.exists_of_fg {R : Type u_1} {S : Type u_2} {N : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid N] [Module R N] (u : TensorProduct R S N) [DecidableEq { P : Submodule R S // P.FG }] : ∃ (A : Subalgebra R S), A.FG ∧ u ∈ LinearMap.range (LinearMap.rTensor N A.val.toLinearMap)

theorem TensorProduct.Algebra.eq_of_fg_of_subtype_eq {R : Type u_1} {S : Type u_2} {N : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid N] [Module R N] {A : Subalgebra R S} (hA : A.FG) {t t' : TensorProduct R (↥A) N} (h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A.val.toLinearMap) t') : ∃ (B : Subalgebra R S) (hAB : A ≤ B), B.FG ∧ (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t'

theorem TensorProduct.Algebra.eq_of_fg_of_subtype_eq' {R : Type u_1} {S : Type u_2} {N : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid N] [Module R N] {A : Subalgebra R S} (hA : A.FG) {t : TensorProduct R (↥A) N} {A' : Subalgebra R S} (hA' : A'.FG) {t' : TensorProduct R (↥A') N} (h : (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t') : ∃ (B : Subalgebra R S) (hAB : A ≤ B) (hA'B : A' ≤ B), B.FG ∧ (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

theorem Submodule.exists_fg_of_baseChange_eq_zero {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {t : TensorProduct R S M} (ht : (LinearMap.baseChange S f) t = 0) : ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct R (↥A) M), (LinearMap.baseChange (↥A) f) u = 0 ∧ (LinearMap.rTensor M A.val.toLinearMap) u = t

Lift an element that maps to 0