Theorems · Theorem · linear algebra

Algebra.TensorProduct.map_surjective

∀ {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} {D : Type u_9} [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Ring C] [inst_6 : Ring D]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] [inst_10 : Algebra R D] [inst_11 : Algebra S A]
  [inst_12 : Algebra S B] [inst_13 : IsScalarTower R S A] [inst_14 : IsScalarTower R S B] (f : A →ₐ[S] B)
  (g : C →ₐ[R] D),
  Function.Surjective ⇑f → Function.Surjective ⇑g → Function.Surjective ⇑(Algebra.TensorProduct.map f g)

Defined in

Mathlib.LinearAlgebra.TensorProduct.RightExactness

Cited by

2 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRingAlgebraRingRingRingRingAlgebraAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTower