tensorProdObjIsoPushoutObj — Mathlib

English

Let R be a ring, S an R-algebra, and A an object of Under R. Then there is a canonical isomorphism between the object obtained by extending A along the tensor product with S and the pushout object of A along the algebra map R → S. In symbols, mkUnder S (S ⊗R A) ≅ Under.pushout (ofHom (algebraMap R S)).obj A.

Русский

Пусть R — кольцо, S — R-алгебра, и A — объект в Under R. Существует каноническое изоморфизмом между объектом S ⊗R A (расширение по S) в Under S и пушаут-объектом A по отображению алгебраической карты R → S. Обозначим: mkUnder S (S ⊗R A) ≅ Under.pushout (ofHom (algebraMap R S)).obj A.

LaTeX

$$$mkUnder\ S\ (S \\otimes_R A) \\cong Under.pushout\\left( ofHom\\left( \\mathrm{algebraMap}\\, R\\, S \\right) \\right).obj A$$$

Lean4

/-- The natural isomorphism `S ⊗[R] A ≅ pushout A.hom (algebraMap R S)` in `Under S`. -/
def tensorProdObjIsoPushoutObj (A : Under R) : mkUnder S (S ⊗[R] A) ≅ (Under.pushout (ofHom <| algebraMap R S)).obj A :=
  Under.isoMk (CommRingCat.isPushout_tensorProduct R S A).flip.isoPushout <|
    by
    simp only [Functor.const_obj_obj, Under.pushout_obj, Functor.id_obj, Under.mk_right, mkUnder_hom,
      AlgHom.toRingHom_eq_coe, IsPushout.inr_isoPushout_hom, Under.mk_hom]
    rfl

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