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 [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.

• 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 [Gri69a], 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 .)

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

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

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

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)

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

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)

theorem LinearMap.rTensor_exact_iff_lTensor_exact {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} (Q : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {f : M →ₗ[R] N} {g : N →ₗ[R] P} : Function.Exact ⇑(LinearMap.rTensor Q f) ⇑(LinearMap.rTensor Q g) ↔ Function.Exact ⇑(LinearMap.lTensor Q f) ⇑(LinearMap.lTensor Q g)

theorem TensorProduct.map_surjective {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [AddCommMonoid P] [Module R N] [Module R P] {g : N →ₗ[R] P} (hg : Function.Surjective ⇑g) {N' : Type u_6} {P' : Type u_7} [AddCommMonoid N'] [AddCommMonoid P'] [Module R N'] [Module R P'] {g' : N' →ₗ[R] P'} (hg' : Function.Surjective ⇑g') : Function.Surjective ⇑(TensorProduct.map g g')

theorem TensorProduct.mk_surjective (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (S : Type u_8) [Semiring S] [Algebra R S] (h : Function.Surjective ⇑(algebraMap R S)) : Function.Surjective ⇑((TensorProduct.mk R S M) 1)

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

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] {h : P → N} (hfg : Function.Exact ⇑f ⇑g) (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.

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

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

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 ⋯

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

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

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 := ⋯ }

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 ⋯

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

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

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

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] {h : P → N} (hfg : Function.Exact ⇑f ⇑g) (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.

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

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

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 ⋯

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

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

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 := ⋯ }

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 ⋯

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

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)

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)

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