Theorems · Definition · commutative algebra

CommRingCat.pushoutCocone

(R A B : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing A] →
      [inst_2 : CommRing B] →
        [inst_3 : Algebra R A] →
          [inst_4 : Algebra R B] →
            CategoryTheory.Limits.PushoutCocone (CommRingCat.ofHom (algebraMap R A))
              (CommRingCat.ofHom (algebraMap R B))

The explicit cocone with tensor products as the fibered product in CommRingCat.

Defined in

Mathlib.Algebra.Category.Ring.Constructions

Cited by

9 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingAlgebraAlgebra