Theorems · Theorem · linear algebra

Algebra.TensorProduct.rTensor_ker

∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A : Type u_6}
  {B : Type u_7} {C : Type u_8} [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Ring C] [inst_6 : Algebra R A]
  [inst_7 : Algebra R B] [inst_8 : Algebra R C] [inst_9 : Algebra S A] [inst_10 : Algebra S B]
  [inst_11 : IsScalarTower R S A] [inst_12 : IsScalarTower R S B] (f : A →ₐ[S] B),
  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

Defined in

Mathlib.LinearAlgebra.TensorProduct.RightExactness

Cited by

1 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraRingRingRingAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTower