Finiteness of the tensor product of (sub)modules

In this file we show that the supremum of two subalgebras that are finitely generated as modules, is again finitely generated.

theorem Submodule.exists_fg_le_eq_rTensor_subtype {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R N M) : ∃ (J : Submodule R N) (_ : J.FG) (y : TensorProduct R (↥J) M), x = (LinearMap.rTensor M J.subtype) y

Every x : N ⊗ M is the image of some y : J ⊗ M, where J is a finitely generated submodule of N, under the tensor product of the inclusion J → N and the identity M → M.

theorem Submodule.exists_fg_le_subset_range_rTensor_subtype {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (s : Set (TensorProduct R N M)) (hs : s.Finite) : ∃ (J : Submodule R N) (_ : J.FG), s ⊆ ↑(LinearMap.range (LinearMap.rTensor M J.subtype))

theorem Submodule.exists_fg_le_eq_rTensor_inclusion {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {I : Submodule R N} (x : TensorProduct R (↥I) M) : ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : TensorProduct R (↥J) M), x = (LinearMap.rTensor M (inclusion hle)) y

Every x : I ⊗ M is the image of some y : J ⊗ M, where J ≤ I is finitely generated, under the tensor product of J.inclusion ‹J ≤ I› : J → I and the identity M → M.

theorem Submodule.exists_fg_le_subset_range_rTensor_inclusion {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {I : Submodule R N} (s : Set (TensorProduct R (↥I) M)) (hs : s.Finite) : ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I), s ⊆ ↑(LinearMap.range (LinearMap.rTensor M (inclusion hle)))

noncomputable def instModuleTensorProduct (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : Module A (TensorProduct R A M)

Porting note: reminding Lean about this instance for Module.Finite.base_change

Equations

• instModuleTensorProduct R A M = TensorProduct.leftModule

instance Module.Finite.base_change (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [h : Module.Finite R M] : Module.Finite A (TensorProduct R A M)

instance Module.Finite.tensorProduct (R : Type u_1) (M : Type u_4) (N : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [hM : Module.Finite R M] [hN : Module.Finite R N] : Module.Finite R (TensorProduct R M N)

theorem Module.exists_isPrincipal_quotient_of_finite (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : ∃ (N : Submodule R M), N ≠ ⊤ ∧ ⊤.IsPrincipal

theorem Module.exists_surjective_quotient_of_finite (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I), I ≠ ⊤ ∧ Function.Surjective ⇑f

instance instNontrivialTensorProduct (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] : Nontrivial (TensorProduct R M M)

theorem Subalgebra.finite_sup {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] [Algebra K L] (E1 E2 : Subalgebra K L) [Module.Finite K ↥E1] [Module.Finite K ↥E2] : Module.Finite K ↥(E1 ⊔ E2)

theorem RingHom.surjective_of_tmul_eq_tmul_of_finite {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] (h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s) : Function.Surjective ⇑(algebraMap R S)