tensorProdIsoPushout — Mathlib

English

There is a natural isomorphism between the tensor product functor R ⊗- S and the pushout construction with the map algebraMap R S; i.e., tensorProd R S ≅ Under.pushout (ofHom (algebraMap R S)).

Русский

Существует естественное тождественное тождество между тензорным произведением и пушаут-конструкцией по отображению algebraMap R S; тождество: tensorProd R S ≅ Under.pushout (ofHom (algebraMap R S)).

LaTeX

$$$\\text{tensorProd} \\ R\\ S \\cong \\Under.pushout\\left(\\text{ofHom}\\left(\\text{algebraMap } R S\\right)\\right)$$$

Lean4

/-- `A ↦ S ⊗[R] A` is naturally isomorphic to `A ↦ pushout A.hom (algebraMap R S)`. -/
def tensorProdIsoPushout : tensorProd R S ≅ Under.pushout (ofHom <| algebraMap R S) :=
  NatIso.ofComponents (fun A ↦ tensorProdObjIsoPushoutObj S A) <|
    by
    intro A B f
    dsimp
    rw [← cancel_epi (tensorProdObjIsoPushoutObj S A).inv]
    ext : 1
    apply pushout.hom_ext
    · rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
      ext x
      simp [mkUnder_right]
    · rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
      ext (x : S)
      simp [mkUnder_right]

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