Documentation

Mathlib.RingTheory.TensorProduct.Finite

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.

source
šŸ“ coverage
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.

source
šŸ“ coverage
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.rTensor M J.subtype).range
source
šŸ“ coverage
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.

source
šŸ“ coverage
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.rTensor M (inclusion hle)).range
source
šŸ“ coverage
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)
source
šŸ“ coverage
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)
source
šŸ“ coverage
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
source
šŸ“ coverage
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
source
šŸ“ coverage
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)
source
šŸ“ coverage
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)
source
šŸ“ coverage
theorem RingHom.Finite.tensorProductMap {R : Type u_1} {S : Type u_2} {S' : Type u_3} {T : Type u_4} {T' : Type u_5} [CommRing R] [CommRing S] [CommRing T] [CommRing S'] [CommRing T'] [Algebra R S] [Algebra R T] [Algebra R S'] [Algebra R T'] {f : S ā†’ā‚[R] S'} (Hf : f.Finite) {g : T ā†’ā‚[R] T'} (Hg : g.Finite) :
(Algebra.TensorProduct.map f g).Finite