English
The tensor equalizer map from T ⊗ AlgHom.equalizer f g to the equalizer of the tensor maps is well-defined and linear.
Русский
Тензорное равноположение между T ⊗ AlgHom.equalizer f g и равноположением тензорных отображений корректно и линейно.
LaTeX
$$$\text{tensorEqualizer} : T ⊗_R AlgHom.equalizer f g \to_A[S] AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g)$$$
Lean4
/-- The canonical map `T ⊗[R] eq(f, g) →ₐ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g)`. -/
def tensorEqualizer :
T ⊗[R] AlgHom.equalizer f g →ₐ[S]
AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g) :=
AlgHom.ofLinearMap (AlgHom.tensorEqualizerAux S T f g) rfl (AlgHom.tensorEqualizerAux_mul S T f g)
