Algebra.TensorProduct.ext

theorem 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

This theorem, `Algebra.TensorProduct.ext`, states that for any two algebra homomorphisms `f` and `g` from the tensor product of two algebras `A` and `B` over a commutative semiring `R` into another algebra `C` over another commutative semiring `S`, if the composition of `f` and the inclusion of `A` into the tensor product is equal to the composition of `g` and the same inclusion, and also the composition of `f` restricted to scalars from `R` and the inclusion of `B` into the tensor product is equal to the composition of `g` restricted to scalars from `R` and the same inclusion, then `f` and `g` are equal. In simpler words, this theorem is essentially a uniqueness condition for algebra homomorphisms between tensor products of algebras. It's particularly useful when dealing with nested tensor products, as it allows the `ext` tactic to apply specific lemmas for algebra homomorphisms.

More concisely: Given commutative semirings R and S, if two algebra homomorphisms f and g from the tensor product of algebras A and B over R into algebra C over S satisfy the conditions f (a ⊗ b) = g (a ⊗ b) for all a in A and b in B, and f (r) = g (r) for all r in R, then f = g.