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

source
noncomputable def TensorProduct.quotientTensorQuotientEquiv {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) (n : Submodule R N) :
TensorProduct R (M ⧸ m) (N ⧸ n) ≃ₗ[R] TensorProduct R M N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range

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
    source
    @[simp]
    theorem TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk {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) (n : Submodule R N) (x : M) (y : N) :
    (quotientTensorQuotientEquiv m n) (Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
    source
    @[simp]
    theorem TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul {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) (n : Submodule R N) (x : M) (y : N) :
    (quotientTensorQuotientEquiv m n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y
    source
    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) :
    TensorProduct R (M ⧸ m) N ≃ₗ[R] TensorProduct R M N ⧸ (map m.subtype LinearMap.id).range

    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
      source
      @[simp]
      theorem TensorProduct.quotientTensorEquiv_apply_tmul_mk {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) (x : M) (y : N) :
      (quotientTensorEquiv N m) (Submodule.Quotient.mk x ⊗ₜ[R] y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
      source
      @[simp]
      theorem TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul {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) (x : M) (y : N) :
      (quotientTensorEquiv N m).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = Submodule.Quotient.mk x ⊗ₜ[R] y
      source
      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) :
      TensorProduct R M (N ⧸ n) ≃ₗ[R] TensorProduct R M N ⧸ (map LinearMap.id n.subtype).range

      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
        source
        @[simp]
        theorem TensorProduct.tensorQuotientEquiv_apply_mk_tmul {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) (x : M) (y : N) :
        (tensorQuotientEquiv M n) (x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
        source
        @[simp]
        theorem TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk {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) (x : M) (y : N) :
        (tensorQuotientEquiv M n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = x ⊗ₜ[R] Submodule.Quotient.mk y
        source
        noncomputable def TensorProduct.quotTensorEquivQuotSMul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
        TensorProduct R (R ⧸ I) M ≃ₗ[R] M ⧸ I • ⊤

        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
          source
          noncomputable def TensorProduct.tensorQuotEquivQuotSMul {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
          TensorProduct R M (R ⧸ I) ≃ₗ[R] M ⧸ I • ⊤

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

          Equations
          Instances For
            source
            @[simp]
            theorem TensorProduct.quotTensorEquivQuotSMul_mk_tmul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (r : R) (x : M) :
            (quotTensorEquivQuotSMul M I) ((Ideal.Quotient.mk I) r ⊗ₜ[R] x) = Submodule.Quotient.mk (r • x)
            source
            @[simp]
            theorem TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) :
            (quotTensorEquivQuotSMul M I) (1 ⊗ₜ[R] x) = Submodule.Quotient.mk x
            source
            theorem TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
            ↑(quotTensorEquivQuotSMul M I) ∘ₗ LinearMap.rTensor M (Submodule.mkQ I) = (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.lid R M)
            source
            @[simp]
            theorem TensorProduct.quotTensorEquivQuotSMul_symm_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) :
            (quotTensorEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = 1 ⊗ₜ[R] x
            source
            theorem TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
            ↑(quotTensorEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (mk R (R ⧸ I) M) 1
            source
            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
            source
            @[simp]
            theorem TensorProduct.tensorQuotEquivQuotSMul_tmul_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) (r : R) :
            (tensorQuotEquivQuotSMul M I) (x ⊗ₜ[R] (Ideal.Quotient.mk I) r) = Submodule.Quotient.mk (r • x)
            source
            theorem TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
            ↑(tensorQuotEquivQuotSMul M I) ∘ₗ LinearMap.lTensor M (Submodule.mkQ I) = (I • ⊤).mkQ ∘ₗ ↑(TensorProduct.rid R M)
            source
            @[simp]
            theorem TensorProduct.tensorQuotEquivQuotSMul_symm_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) :
            (tensorQuotEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = x ⊗ₜ[R] 1
            source
            theorem TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
            ↑(tensorQuotEquivQuotSMul M I).symm ∘ₗ (I • ⊤).mkQ = (mk R M (R ⧸ I)).flip 1
            source
            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
            source
            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
              source
              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) :
              (TensorProduct R S M ⧸ Ideal.map (algebraMap R S) I • ⊤) ≃ₗ[S] TensorProduct R S (M ⧸ I • ⊤)

              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
                source
                noncomputable def TensorProduct.AlgebraTensorModule.tensorQuotientEquiv {R : Type u_1} (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (M : Type u_4) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] {N : Type u_5} [AddCommGroup N] [Module R N] [Module B N] [IsScalarTower R B N] (n : Submodule B N) :
                TensorProduct R M (N ⧸ n) ≃ₗ[A] TensorProduct R M N ⧸ ((lTensor A M) (↑R n.subtype)).range

                More linear version of TensorProduct.tensorQuotientEquiv.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_apply_tmul {R : Type u_1} (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (M : Type u_4) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] {N : Type u_5} [AddCommGroup N] [Module R N] [Module B N] [IsScalarTower R B N] (n : Submodule B N) (x : M) (y : N) :
                  (tensorQuotientEquiv A B M n) (x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
                  source
                  @[simp]
                  theorem TensorProduct.AlgebraTensorModule.tensorQuotientEquiv_symm_apply_mk_tmul {R : Type u_1} (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (M : Type u_4) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] {N : Type u_5} [AddCommGroup N] [Module R N] [Module B N] [IsScalarTower R B N] (n : Submodule B N) (x : M) (y : N) :
                  (tensorQuotientEquiv A B M n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = x ⊗ₜ[R] Submodule.Quotient.mk y