Flatness and tensor products of algebra homomorphisms

Mathlib's TensorProduct.map_injective_of_flat_flat shows that the tensor product of two injective linear maps is injective when the codomain of the first and the domain of the second are flat. This file records the same statement for Algebra.TensorProduct.map of algebra homomorphisms, so that it applies without first passing to the underlying linear maps. It also identifies the kernel after tensoring an algebra map with a flat algebra, the analogue of Mathlib's Algebra.TensorProduct.lTensor_ker with flatness in place of surjectivity.

Main results

• Algebra.TensorProduct.map_injective_of_flat_flat: the tensor product of two injective algebra homomorphisms is injective under the flatness hypotheses of TensorProduct.map_injective_of_flat_flat.
• Algebra.TensorProduct.lTensor_ker_of_flat: tensoring with a flat algebra carries kernels to their images under the right tensor inclusion.

theorem Algebra.TensorProduct.map_injective_of_flat_flat {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [Algebra S A] [Algebra S B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B) (g : C →ₐ[R] D) [Module.Flat R B] [Module.Flat R C] (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Function.Injective ⇑(map f g)

The tensor product of two injective algebra homomorphisms is injective when the codomain of the first and the domain of the second are flat.

theorem Algebra.TensorProduct.lTensor_ker_of_flat {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] [Module.Flat R A] (f : B →ₐ[R] C) : RingHom.ker (map (AlgHom.id R A) f) = Ideal.map includeRight (RingHom.ker f)

Tensoring an algebra map with a flat algebra carries its kernel to the ideal generated by its image under the right tensor inclusion.