Documentation

Mathlib.RingTheory.Finiteness.TensorProduct

Finiteness of the tensor product of (sub)modules #

TODO: this file can probably be merged with RingTheory.TensorProduct.Finite, although the two files are currently incomparable in the import graph: we will need further cleanup of the lemmas involved before we can do this.

source
theorem Submodule.exists_fg_le_eq_rTensor_inclusion {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [AddCommGroup 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 (Submodule.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
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
Instances For
    source
    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)
    Equations
    • ⋯ = ⋯
    source
    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)
    Equations
    • ⋯ = ⋯
    source
    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
    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
    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)
    Equations
    • ⋯ = ⋯