English
Let f,g: A ⊗_R B →_S C be algebra homomorphisms. If f and g agree after precomposition with includeLeft and after restricting scalars and precomposition with includeRight, then f = g.
Русский
Пусть f,g: A ⊗_R B →_S C — алгебра-гомоморфизмы. Если они совпадают после пред-ограничения includeLeft и после ограничения скаляров и пред-ограничения includeRight, то f = g.
LaTeX
$$$f,g: A\otimes_R B \to_S C\quad\text{AlgHom}\quad
(f\circ i_L)=(g\circ i_L)\ \land\ ((f|_R)\circ i_R=(g|_R)\circ i_R)\ \Rightarrow\ f=g.$$$
Lean4
/-- 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]. -/
@[ext high]
theorem ext ⦃f g : (A ⊗[R] B) →ₐ[S] C⦄ (ha : f.comp includeLeft = g.comp includeLeft)
(hb : (f.restrictScalars R).comp includeRight = (g.restrictScalars R).comp includeRight) : f = g :=
by
apply AlgHom.toLinearMap_injective
ext a b
have := congr_arg₂ HMul.hMul (AlgHom.congr_fun ha a) (AlgHom.congr_fun hb b)
dsimp at *
rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this
