Theorems · Definition · commutative algebra

CommRingCat.tensorProdObjIsoPushoutObj

{R : CommRingCat} →
  (S : CommRingCat) →
    [inst : Algebra ↑R ↑S] →
      (A : CategoryTheory.Under R) →
        S.mkUnder (TensorProduct ↑R ↑S ↑A.right) ≅
          (CategoryTheory.Under.pushout (CommRingCat.ofHom (algebraMap ↑R ↑S))).obj A

The natural isomorphism S ⊗[R] A ≅ pushout A.hom (algebraMap R S) in Under S.

Defined in: Mathlib.Algebra.Category.Ring.Under.Basic
Cited by: 5 results in Mathlib
Foundations: Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites18

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
CategoryTheory.Functor.objstatement · cited by 19,642
Algebrastatement and proof · cited by 11,388
Algebra.algebraMapstatement · cited by 4,706
CategoryTheory.Isostatement · cited by 3,963
TensorProductstatement · cited by 2,545
CommRingCatstatement and proof · cited by 2,333
CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
CommRingCat.carrierstatement and proof · cited by 1,096
CategoryTheory.Limits.WalkingSpanstatement · cited by 300
CategoryTheory.Limits.spanstatement · cited by 294
CategoryTheory.Understatement and proof · cited by 276

Cited by6

Results whose statement or proof uses this declaration.

CommRingCat.tensorProdIsoPushoutproof · cited by 3
CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_rightstatement · cited by 1
CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_rightstatement · cited by 1
CommRingCat.tensorProdIsoPushout_appstatement · cited by 0
CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assocstatement and proof · cited by 0
CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assocstatement and proof · cited by 0