English
If T is flat, there is an algebra equivalence between T ⊗ AlgHom.equalizer f g and AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g).
Русский
Если T плоский, существует алгебра-соответствие между T ⊗ AlgHom.equalizer f g и AlgHom.equalizer (Algebra.TensorProduct.map ...) (Algebra.TensorProduct.map ...).
LaTeX
$$tensorEqualizerEquiv [Module.Flat R T] : T ⊗_R AlgHom.equalizer f g ≃_A[S] AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g)$$
Lean4
/-- If `T` is `R`-flat, the canonical map
`T ⊗[R] eq(f, g) →ₐ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g)` is an isomorphism. -/
def tensorEqualizerEquiv [Module.Flat R T] :
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) :=
AlgEquiv.ofLinearEquiv (LinearMap.tensorEqLocusEquiv S T f.toLinearMap g.toLinearMap) rfl
(AlgHom.tensorEqualizerAux_mul S T f g)
