English
For a pushout configuration with S ⊗ T, the pushout is preserved under left/right symmetry.
Русский
Для пушаутной конфигурации S ⊗ T сохранение пушаута сохраняется слева и справа.
LaTeX
$$Algebra.IsPushout.isPushout$$
Lean4
/-- If `S' = S ⊗[R] R'`, then any pair of `R`-algebra homomorphisms `f : S → A` and `g : R' → A`
such that `f x` and `g y` commutes for all `x, y` descends to a (unique) homomorphism `S' → A`.
-/
@[simps! -isSimp apply]
noncomputable def pushoutDesc [H : Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A] [Algebra R A] (f : S →ₐ[R] A)
(g : R' →ₐ[R] A) (hf : ∀ x y, f x * g y = g y * f x) : S' →ₐ[R] A :=
(Algebra.TensorProduct.lift f g hf).comp ((Algebra.IsPushout.equiv R S R' S').symm.toAlgHom.restrictScalars R)
