Documentation

Mathlib.LinearAlgebra.TensorProduct.Quotient

Interaction between Quotients and Tensor Products #

This file contains constructions that relate quotients and tensor products. Let M, N be R-modules, m ≤ M and n ≤ N be an R-submodules and I ≤ R an ideal. We prove the following isomorphisms:

Main results #

Tags #

Quotient, Tensor Product

Let M, N be R-modules, m ≤ M and n ≤ N be an R-submodules. Then we have a linear isomorphism between tensor products of the quotients and the quotient of the tensor product: (M ⧸ m) ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N ⊔ M ⊗ n).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable def TensorProduct.quotientTensorEquiv {R : Type u_1} {M : Type u_2} (N : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) :

    Let M, N be R-modules, m ≤ M be an R-submodule. Then we have a linear isomorphism between tensor products of the quotient and the quotient of the tensor product: (M ⧸ m) ⊗[R] N ≃ₗ[R] (M ⊗[R] N) ⧸ (m ⊗ N).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      noncomputable def TensorProduct.tensorQuotientEquiv {R : Type u_1} (M : Type u_2) {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : Submodule R N) :

      Let M, N be R-modules, n ≤ N be an R-submodule. Then we have a linear isomorphism between tensor products of the quotient and the quotient of the tensor product: M ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (M ⊗ n).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        noncomputable def TensorProduct.quotTensorEquivQuotSMul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :

        Left tensoring a module with a quotient of the ring is the same as quotienting that module by the corresponding submodule.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def TensorProduct.tensorQuotEquivQuotSMul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :

          Right tensoring a module with a quotient of the ring is the same as quotienting that module by the corresponding submodule.

          Equations
          Instances For
            @[simp]
            theorem TensorProduct.quotTensorEquivQuotSMul_comp_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
            (quotTensorEquivQuotSMul M I) ∘ₗ (mk R (R I) M) 1 = (I ).mkQ
            @[simp]
            theorem TensorProduct.tensorQuotEquivQuotSMul_comp_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
            (tensorQuotEquivQuotSMul M I) ∘ₗ (mk R M (R I)).flip 1 = (I ).mkQ
            noncomputable def Ideal.qoutMapEquivTensorQout {R : Type u_1} [CommRing R] (S : Type u_4) [CommRing S] [Algebra R S] {I : Ideal R} :
            (S map (algebraMap R S) I) ≃ₗ[S] TensorProduct R S (R I)

            Let R be a commutative ring, S be an R-algebra, I is be ideal of R, then S ⧸ IS is isomorphic to S ⊗[R] (R ⧸ I) as S modules.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def TensorProduct.tensorQuotMapSMulEquivTensorQuot {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_4) [CommRing S] [Algebra R S] (I : Ideal R) :

              Let R be a commutative ring, S be an R-algebra, I is be ideal of R, then S ⊗[R] M ⧸ I(S ⊗[R] M) is isomorphic to S ⊗[R] (M ⧸ IM) as S modules.

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