Documentation

Mathlib.LinearAlgebra.TensorProduct.RightExactness

Right-exactness properties of tensor product #

Modules #

The proofs are those of [Bou98a] (chap. 2, §3, n°6)

Algebras #

In the case of a tensor product of algebras, these results can be particularized to compute some kernels.

Note on implementation #

TODO #

theorem le_comap_range_lTensor {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) (q : Q) :
theorem le_comap_range_rTensor {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) (q : Q) :
theorem LinearMap.lTensor_surjective {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} (Q : Type u_5) [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] {g : N →ₗ[R] P} (hg : Function.Surjective g) :

If g is surjective, then lTensor Q g is surjective

theorem LinearMap.rTensor_surjective {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} (Q : Type u_5) [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] {g : N →ₗ[R] P} (hg : Function.Surjective g) :

If g is surjective, then rTensor Q g is surjective

theorem LinearMap.exact_subtype_mkQ {R : Type u_1} {N : Type u_3} [CommRing R] [AddCommGroup N] [Module R N] (Q : Submodule R N) :
Function.Exact Q.subtype Q.mkQ
theorem LinearMap.exact_map_mkQ_range {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] N) :
theorem LinearMap.exact_subtype_ker_map {R : Type u_1} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup N] [AddCommGroup P] [Module R N] [Module R P] (g : N →ₗ[R] P) :
Function.Exact (LinearMap.ker g).subtype g
noncomputable def lTensor.toFun {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) :

The direct map in lTensor.equiv

Equations
Instances For
    noncomputable def lTensor.inverse_of_rightInverse {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) :

    The inverse map in lTensor.equiv_of_rightInverse (computably, given a right inverse)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem lTensor.inverse_of_rightInverse_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) (y : TensorProduct R Q N) :
      theorem lTensor.inverse_of_rightInverse_comp_lTensor {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) :
      noncomputable def lTensor.inverse {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :

      The inverse map in lTensor.equiv

      Equations
      Instances For
        theorem lTensor.inverse_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) (y : TensorProduct R Q N) :
        theorem lTensor.inverse_comp_lTensor {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :
        noncomputable def lTensor.linearEquiv_of_rightInverse {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) :

        For a surjective f : N →ₗ[R] P, the natural equivalence between Q ⊗ N ⧸ (image of ker f) to Q ⊗ P (computably, given a right inverse)

        Equations
        Instances For
          noncomputable def lTensor.equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :

          For a surjective f : N →ₗ[R] P, the natural equivalence between Q ⊗ N ⧸ (image of ker f) to Q ⊗ P

          Equations
          Instances For
            theorem lTensor_exact {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :

            Tensoring an exact pair on the left gives an exact pair

            theorem lTensor_mkQ {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : Type u_5) [AddCommGroup Q] [Module R Q] (N : Submodule R M) :

            Right-exactness of tensor product

            noncomputable def rTensor.toFun {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) :

            The direct map in rTensor.equiv

            Equations
            Instances For
              noncomputable def rTensor.inverse_of_rightInverse {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) :

              The inverse map in rTensor.equiv_of_rightInverse (computably, given a right inverse)

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem rTensor.inverse_of_rightInverse_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) (y : TensorProduct R N Q) :
                theorem rTensor.inverse_of_rightInverse_comp_rTensor {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) :
                noncomputable def rTensor.inverse {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :

                The inverse map in rTensor.equiv

                Equations
                Instances For
                  theorem rTensor.inverse_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) (y : TensorProduct R N Q) :
                  theorem rTensor.inverse_comp_rTensor {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :
                  noncomputable def rTensor.linearEquiv_of_rightInverse {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) {h : PN} (hgh : Function.RightInverse h g) :

                  For a surjective f : N →ₗ[R] P, the natural equivalence between N ⊗[R] Q ⧸ (range (rTensor Q f)) and P ⊗[R] Q (computably, given a right inverse)

                  Equations
                  Instances For
                    noncomputable def rTensor.equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :

                    For a surjective f : N →ₗ[R] P, the natural equivalence between N ⊗[R] Q ⧸ (range (rTensor Q f)) and P ⊗[R] Q

                    Equations
                    Instances For
                      theorem rTensor_exact {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [AddCommGroup Q] [Module R Q] (hfg : Function.Exact f g) (hg : Function.Surjective g) :

                      Tensoring an exact pair on the right gives an exact pair

                      theorem rTensor_mkQ {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : Type u_5) [AddCommGroup Q] [Module R Q] (N : Submodule R M) :

                      Right-exactness of tensor product (rTensor)

                      theorem TensorProduct.map_surjective {R : Type u_1} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup N] [AddCommGroup P] [Module R N] [Module R P] {g : N →ₗ[R] P} (hg : Function.Surjective g) {N' : Type u_7} {P' : Type u_8} [AddCommGroup N'] [AddCommGroup P'] [Module R N'] [Module R P'] {g' : N' →ₗ[R] P'} (hg' : Function.Surjective g') :
                      theorem TensorProduct.map_ker {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact f g) (hg : Function.Surjective g) {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [AddCommGroup M'] [AddCommGroup N'] [AddCommGroup P'] [Module R M'] [Module R N'] [Module R P'] {f' : M' →ₗ[R] N'} {g' : N' →ₗ[R] P'} (hfg' : Function.Exact f' g') (hg' : Function.Surjective g') :

                      Kernel of a product map (right-exactness of tensor product)

                      theorem TensorProduct.mk_surjective (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_9) [Semiring S] [Algebra R S] (h : Function.Surjective (algebraMap R S)) :
                      noncomputable def 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
                      Instances For
                        noncomputable def 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 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) :
                          theorem 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)
                          @[simp]
                          theorem quotTensorEquivQuotSMul_symm_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) :
                          theorem 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 = (TensorProduct.mk R (R I) M) 1
                          theorem quotTensorEquivQuotSMul_comp_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
                          (quotTensorEquivQuotSMul M I) ∘ₗ (TensorProduct.mk R (R I) M) 1 = (I ).mkQ
                          @[simp]
                          theorem 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) :
                          theorem 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)
                          @[simp]
                          theorem tensorQuotEquivQuotSMul_symm_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (x : M) :
                          theorem 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 = (TensorProduct.mk R M (R I)).flip 1
                          theorem tensorQuotEquivQuotSMul_comp_mk {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) :
                          (tensorQuotEquivQuotSMul M I) ∘ₗ (TensorProduct.mk R M (R I)).flip 1 = (I ).mkQ
                          theorem Ideal.map_includeLeft_eq {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal A) :
                          Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeLeft I) = LinearMap.range (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype)

                          The ideal of A ⊗[R] B generated by I is the image of I ⊗[R] B

                          theorem Ideal.map_includeRight_eq {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (I : Ideal B) :
                          Submodule.restrictScalars R (Ideal.map Algebra.TensorProduct.includeRight I) = LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype)

                          The ideal of A ⊗[R] B generated by I is the image of A ⊗[R] I

                          theorem Algebra.TensorProduct.lTensor_ker {R : Type u_4} [CommRing R] {A : Type u_5} {C : Type u_7} {D : Type u_8} [Ring A] [Ring C] [Ring D] [Algebra R A] [Algebra R C] [Algebra R D] (g : C →ₐ[R] D) (hg : Function.Surjective g) :
                          RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) g) = Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)

                          If g is surjective, then the kernel of (id A) ⊗ g is generated by the kernel of g

                          theorem Algebra.TensorProduct.rTensor_ker {R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (hf : Function.Surjective f) :
                          RingHom.ker (Algebra.TensorProduct.map f (AlgHom.id R C)) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f)

                          If f is surjective, then the kernel of f ⊗ (id B) is generated by the kernel of f

                          theorem Algebra.TensorProduct.map_ker {R : Type u_4} [CommRing R] {A : Type u_5} {B : Type u_6} {C : Type u_7} {D : Type u_8} [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) (hf : Function.Surjective f) (hg : Function.Surjective g) :
                          RingHom.ker (Algebra.TensorProduct.map f g) = Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)

                          If f and g are surjective morphisms of algebras, then the kernel of Algebra.TensorProduct.map f g is generated by the kernels of f and g