Theorems · Definition · category theory

CommRingCat.Under.equalizerForkTensorProdIso

{R S : CommRingCat} →
  [inst : Algebra ↑R ↑S] →
    [Module.Flat ↑R ↑S] →
      {A B : CategoryTheory.Under R} →
        (f g : A ⟶ B) →
          CommRingCat.Under.tensorProdEqualizer f g ≅
            CommRingCat.Under.equalizerFork' (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom f))
              (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (CommRingCat.toAlgHom g))

If S is R-flat, S ⊗[R] eq(f, g) is isomorphic to eq(𝟙 ⊗[R] f, 𝟙 ⊗[R] g).

Defined in

Mathlib.Algebra.Category.Ring.Under.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraModule.Flat