Theorems · Theorem · commutative algebra

Algebra.TensorProduct.ext

∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : CommSemiring S] [inst_8 : Algebra S A] [inst_9 : Algebra R S] [inst_10 : Algebra S C]
  [inst_11 : IsScalarTower R S A] [inst_12 : IsScalarTower R S C] ⦃f g : TensorProduct R A B →ₐ[S] C⦄,
  f.comp Algebra.TensorProduct.includeLeft = g.comp Algebra.TensorProduct.includeLeft →
    (AlgHom.restrictScalars R f).comp Algebra.TensorProduct.includeRight =
        (AlgHom.restrictScalars R g).comp Algebra.TensorProduct.includeRight →
      f = g

A version of TensorProduct.ext for AlgHom. Using this as the @[ext] lemma instead of Algebra.TensorProduct.ext' allows ext to apply lemmas specific to A →ₐ[S] _ and B →ₐ[R] _; notably this allows recursion into nested tensor products of algebras. See note [partially-applied ext lemmas].

Defined in

Mathlib.RingTheory.TensorProduct.Basic

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraSemiringAlgebraSemiringAlgebraCommSemiringAlgebraAlgebraAlgebraIsScalarTowerIsScalarTower