instIsPushoutPolynomial — Mathlib

English

The square of algebras R → S and R → R[X], S → S[X] is a pushout; equivalently, S[X] ≅ S ⊗_R R[X].

Русский

Квадрат алгебр R → S и R → R[X], S → S[X] является пуш-аута; эквивалентно S[X] ≅ S ⊗_R R[X].

LaTeX

$$$\text{Algebra.IsPushout } R S R[X] S[X]\quad\Longleftrightarrow\quad S[X] \cong_R S \otimes_R R[X].$$$

Lean4

instance : Algebra.IsPushout R S R[X] S[X] where
  out := .of_equiv (polyEquivTensor' R S).symm fun _ ↦ (polyEquivTensor_symm_apply_tmul_eq_smul ..).trans <| one_smul ..

Похожие утверждения