Theorems · Theorem · commutative algebra

CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right

∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr A.hom (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      (CategoryTheory.Under.Hom.right (CommRingCat.tensorProdObjIsoPushoutObj S A).inv) =
    CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom

Defined in: Mathlib.Algebra.Category.Ring.Under.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 88 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.

Cites28

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
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
Algebrastatement and proof · cited by 11,388
CategoryTheory.Iso.invstatement · cited by 6,514
Algebra.algebraMapstatement and proof · cited by 4,706
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
RingHomClass.toRingHomproof · cited by 746
CategoryTheory.Limits.WalkingSpanstatement · cited by 300

Cited by1

Results whose statement or proof uses this declaration.

CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assocproof · cited by 0