Right-exactness properties of tensor product #

Modules #

LinearMap.rTensor_surjective asserts that when one tensors a surjective map on the right, one still gets a surjective linear map. More generally, LinearMap.rTensor_range computes the range of LinearMap.rTensor
LinearMap.lTensor_surjective asserts that when one tensors a surjective map on the left, one still gets a surjective linear map. More generally, LinearMap.lTensor_range computes the range of LinearMap.lTensor
TensorProduct.rTensor_exact says that when one tensors a short exact sequence on the right, one still gets a short exact sequence (right-exactness of TensorProduct.rTensor), and rTensor.equiv gives the LinearEquiv that follows from this combined with LinearMap.rTensor_surjective.
TensorProduct.lTensor_exact says that when one tensors a short exact sequence on the left, one still gets a short exact sequence (right-exactness of TensorProduct.rTensor) and lTensor.equiv gives the LinearEquiv that follows from this combined with LinearMap.lTensor_surjective.
For N : Submodule R M, LinearMap.exact_subtype_mkQ N says that the inclusion of the submodule and the quotient map form an exact pair, and lTensor_mkQ compute ker (lTensor Q (N.mkQ)) and similarly for rTensor_mkQ
TensorProduct.map_ker computes the kernel of TensorProduct.map f g' in the presence of two short exact sequences.

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

Algebras #

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

Algebra.TensorProduct.ker_map computes the kernel of Algebra.TensorProduct.map f g
Algebra.TensorProduct.lTensor_ker and Algebra.TensorProduct.rTensor_ker compute the kernels of Algebra.TensorProduct.map f id and Algebra.TensorProduct.map id g

Note on implementation #

All kernels are computed by applying the first isomorphism theorem and establishing some isomorphisms.
The proofs are essentially done twice, once for lTensor and then for rTensor. It is possible to apply TensorProduct.flip to deduce one of them from the other. However, this approach will lead to different isomorphisms, and it is not quicker.
The proofs of Ideal.map_includeLeft_eq and Ideal.map_includeRight_eq could be easier if I ⊗[R] B was naturally an A ⊗[R] B module, and the map to A ⊗[R] B was known to be linear. This depends on the B-module structure on a tensor product whose use rapidly conflicts with everything…

TODO #

Treat the noncommutative case
Treat the case of modules over semirings (For a possible definition of an exact sequence of commutative semigroups, see [Grillet-1969b], Pierre-Antoine Grillet, The tensor product of commutative semigroups, Trans. Amer. Math. Soc. 138 (1969), 281-293, doi:10.1090/S0002-9947-1969-0237688-1 .)

source

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) :

LinearMap.range g ≤ Submodule.comap ((TensorProduct.mk R Q P) q) (LinearMap.range (LinearMap.lTensor Q g))

source

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) :

LinearMap.range g ≤ Submodule.comap ((TensorProduct.mk R P Q).flip q) (LinearMap.range (LinearMap.rTensor Q g))

source

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) :

Function.Surjective ⇑(LinearMap.lTensor Q g)

If g is surjective, then lTensor Q g is surjective

source

theorem LinearMap.lTensor_range {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} :

LinearMap.range (LinearMap.lTensor Q g) = LinearMap.range (LinearMap.lTensor Q (LinearMap.range g).subtype)

source

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) :

Function.Surjective ⇑(LinearMap.rTensor Q g)

If g is surjective, then rTensor Q g is surjective

source

theorem LinearMap.rTensor_range {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} :

LinearMap.range (LinearMap.rTensor Q g) = LinearMap.range (LinearMap.rTensor Q (LinearMap.range g).subtype)

source

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

source

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) :

Function.Exact ⇑f ⇑(LinearMap.range f).mkQ

source

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

source

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) :

TensorProduct R Q N ⧸ LinearMap.range (LinearMap.lTensor Q f) →ₗ[R] TensorProduct R Q P

The direct map in lTensor.equiv

Equations

lTensor.toFun Q hfg = (LinearMap.range (LinearMap.lTensor Q f)).liftQ (LinearMap.lTensor Q g) ⋯

Instances For

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) :

TensorProduct R Q P →ₗ[R] TensorProduct R Q N ⧸ LinearMap.range (LinearMap.lTensor Q f)

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

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) (y : TensorProduct R Q N) :

(lTensor.inverse_of_rightInverse Q hfg hgh) ((LinearMap.lTensor Q g) y) = Submodule.Quotient.mk y

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) :

lTensor.inverse_of_rightInverse Q hfg hgh ∘ₗ LinearMap.lTensor Q g = (LinearMap.range (LinearMap.lTensor Q f)).mkQ

source

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) :

TensorProduct R Q P →ₗ[R] TensorProduct R Q N ⧸ LinearMap.range (LinearMap.lTensor Q f)

The inverse map in lTensor.equiv

Equations

lTensor.inverse Q hfg hg = lTensor.inverse_of_rightInverse Q hfg ⋯

Instances For

source

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) :

(lTensor.inverse Q hfg hg) ((LinearMap.lTensor Q g) y) = Submodule.Quotient.mk y

source

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) :

lTensor.inverse Q hfg hg ∘ₗ LinearMap.lTensor Q g = (LinearMap.range (LinearMap.lTensor Q f)).mkQ

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) :

(TensorProduct R Q N ⧸ LinearMap.range (LinearMap.lTensor Q f)) ≃ₗ[R] TensorProduct R Q P

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

lTensor.linearEquiv_of_rightInverse Q hfg hgh = { toLinearMap := lTensor.toFun Q hfg, invFun := ⇑(lTensor.inverse_of_rightInverse Q hfg hgh), left_inv := ⋯, right_inv := ⋯ }

Instances For

source

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) :

(TensorProduct R Q N ⧸ LinearMap.range (LinearMap.lTensor Q f)) ≃ₗ[R] TensorProduct R Q P

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

Equations

lTensor.equiv Q hfg hg = lTensor.linearEquiv_of_rightInverse Q hfg ⋯

Instances For

source

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) :

Function.Exact ⇑(LinearMap.lTensor Q f) ⇑(LinearMap.lTensor Q g)

Tensoring an exact pair on the left gives an exact pair

source

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) :

LinearMap.ker (LinearMap.lTensor Q N.mkQ) = LinearMap.range (LinearMap.lTensor Q N.subtype)

Right-exactness of tensor product

source

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) :

TensorProduct R N Q ⧸ LinearMap.range (LinearMap.rTensor Q f) →ₗ[R] TensorProduct R P Q

The direct map in rTensor.equiv

Equations

rTensor.toFun Q hfg = (LinearMap.range (LinearMap.rTensor Q f)).liftQ (LinearMap.rTensor Q g) ⋯

Instances For

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) :

TensorProduct R P Q →ₗ[R] TensorProduct R N Q ⧸ LinearMap.range (LinearMap.rTensor Q f)

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

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) (y : TensorProduct R N Q) :

(rTensor.inverse_of_rightInverse Q hfg hgh) ((LinearMap.rTensor Q g) y) = Submodule.Quotient.mk y

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) :

rTensor.inverse_of_rightInverse Q hfg hgh ∘ₗ LinearMap.rTensor Q g = (LinearMap.range (LinearMap.rTensor Q f)).mkQ

source

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) :

TensorProduct R P Q →ₗ[R] TensorProduct R N Q ⧸ LinearMap.range (LinearMap.rTensor Q f)

The inverse map in rTensor.equiv

Equations

rTensor.inverse Q hfg hg = rTensor.inverse_of_rightInverse Q hfg ⋯

Instances For

source

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) :

(rTensor.inverse Q hfg hg) ((LinearMap.rTensor Q g) y) = Submodule.Quotient.mk y

source

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) :

rTensor.inverse Q hfg hg ∘ₗ LinearMap.rTensor Q g = (LinearMap.range (LinearMap.rTensor Q f)).mkQ

source

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 : P → N} (hgh : Function.RightInverse h ⇑g) :

(TensorProduct R N Q ⧸ LinearMap.range (LinearMap.rTensor Q f)) ≃ₗ[R] TensorProduct R P Q

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

rTensor.linearEquiv_of_rightInverse Q hfg hgh = { toLinearMap := rTensor.toFun Q hfg, invFun := ⇑(rTensor.inverse_of_rightInverse Q hfg hgh), left_inv := ⋯, right_inv := ⋯ }

Instances For

source

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) :

(TensorProduct R N Q ⧸ LinearMap.range (LinearMap.rTensor Q f)) ≃ₗ[R] TensorProduct R P Q

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

Equations

rTensor.equiv Q hfg hg = rTensor.linearEquiv_of_rightInverse Q hfg ⋯

Instances For

source

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) :

Function.Exact ⇑(LinearMap.rTensor Q f) ⇑(LinearMap.rTensor Q g)

Tensoring an exact pair on the right gives an exact pair

source

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) :

LinearMap.ker (LinearMap.rTensor Q N.mkQ) = LinearMap.range (LinearMap.rTensor Q N.subtype)

Right-exactness of tensor product (rTensor)

source

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') :

Function.Surjective ⇑(TensorProduct.map g g')

source

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') :

LinearMap.ker (TensorProduct.map g g') = LinearMap.range (LinearMap.lTensor N f') ⊔ LinearMap.range (LinearMap.rTensor N' f)

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

source

noncomputable def 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

quotTensorEquivQuotSMul M I = (rTensor.equiv M ⋯ ⋯).symm.trans (Submodule.Quotient.equiv (LinearMap.range (LinearMap.rTensor M (Submodule.subtype I))) (I • ⊤) (TensorProduct.lid R M) ⋯)

Instances For

source

noncomputable def 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

tensorQuotEquivQuotSMul M I = (TensorProduct.comm R M (R ⧸ I)).trans (quotTensorEquivQuotSMul M I)

Instances For

source

@[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) :

(quotTensorEquivQuotSMul M I) ((Ideal.Quotient.mk I) r ⊗ₜ[R] x) = Submodule.Quotient.mk (r • x)

source

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)

source

@[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) :

(quotTensorEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = 1 ⊗ₜ[R] x

source

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

source

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

source

@[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) :

(tensorQuotEquivQuotSMul M I) (x ⊗ₜ[R] (Ideal.Quotient.mk I) r) = Submodule.Quotient.mk (r • x)

source

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)

source

@[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) :

(tensorQuotEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = x ⊗ₜ[R] 1

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.LinearAlgebra.TensorProduct.RightExactness

Right-exactness properties of tensor product #

Modules #

Algebras #

Note on implementation #

TODO #