isPushout_tensorProduct — Mathlib

English

The pushout of the two algebra maps is realized by the algebra A ⊗_R B with the canonical maps from A and B into the tensor product.

Русский

Пуш-аут двух алгебраических отображений реализуется через алгебру $A\\otimes_R B$ с каноническими отображениями из A и B.

LaTeX

$$$\\text{IsPushout}(\\text{ofHom}(\\text{algebraMap }R S),\\ldots)$ with tensor product structure$$

Lean4

theorem isPushout_tensorProduct (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] :
    IsPushout (ofHom <| algebraMap R A) (ofHom <| algebraMap R B)
      (ofHom (S := A ⊗[R] B) <| Algebra.TensorProduct.includeLeftRingHom)
      (ofHom (S := A ⊗[R] B) <| Algebra.TensorProduct.includeRight.toRingHom)
    where
  w := by
    ext
    simp
  isColimit' := ⟨pushoutCoconeIsColimit R A B⟩

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