pushoutCocone — Mathlib

English

The pushout cocone in CommRingCat for the two algebra maps from R to A and to B is given by the tensor product A ⊗_R B with the canonical inl and inr maps.

Русский

Кокон-подпространение в CommRingCat для двух алгебраических отображений из R в A и B задается тензорным произведением A ⊗_R B с каноническими отображениями inl и inr.

LaTeX

$$$\text{pushoutCocone}(R,A,B) \;:\; \big(\text{CommRingCat.ofHom}(\text{algebraMap }R A),\ \text{CommRingCat.ofHom}(\text{algebraMap }R B)\big)$$$

Lean4

/-- The explicit cocone with tensor products as the fibered product in `CommRingCat`. -/
def pushoutCocone : Limits.PushoutCocone (CommRingCat.ofHom (algebraMap R A)) (CommRingCat.ofHom (algebraMap R B)) :=
  by
  fapply Limits.PushoutCocone.mk
  · exact CommRingCat.of (A ⊗[R] B)
  · exact ofHom <| Algebra.TensorProduct.includeLeftRingHom (A := A)
  · exact ofHom <| Algebra.TensorProduct.includeRight.toRingHom (A := B)
  · ext r
    trans algebraMap R (A ⊗[R] B) r
    · exact Algebra.TensorProduct.includeLeft.commutes (R := R) r
    · exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm

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