Theorems · Theorem · commutative algebra

PiTensorProduct.algHom_ext

∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] {S : Type u_5} [Finite ι] [inst_4 : DecidableEq ι] [inst_5 : Semiring S]
  [inst_6 : Algebra R S] ⦃f g : (PiTensorProduct R fun i => A i) →ₐ[R] S⦄,
  (∀ (i : ι), f.comp (PiTensorProduct.singleAlgHom i) = g.comp (PiTensorProduct.singleAlgHom i)) → f = g

To show two algebra morphisms from finite tensor products are equal, it suffices to show that they agree on elements of the form $1 ⊗ ⋯ ⊗ a ⊗ 1 ⊗ ⋯$.

Defined in

Mathlib.RingTheory.PiTensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraFiniteDecidableEqSemiringAlgebra