Theorems · Theorem · category theory

CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective

∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] {A B : CategoryTheory.Under R} {f g : A ⟶ B},
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))

Defined in

Mathlib.Algebra.Category.Ring.Under.Property

Cited by

1 results in Mathlib

Foundations

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

Assumes

Algebra