Theorems · Definition · commutative algebra
CommRingCat.tensorProd
(R S : CommRingCat) → [Algebra ↑R ↑S] → CategoryTheory.Functor (CategoryTheory.Under R) (CategoryTheory.Under S)
The base change functor A ↦ S ⊗[R] A.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Algebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- Algebrastatement and proof · cited by 11,388
- TensorProductproof · cited by 2,545
- CommRingCatstatement and proof · cited by 2,333
- CommRingCat.carrierstatement and proof · cited by 1,096
- CategoryTheory.Understatement and proof · cited by 276
- AlgHom.idproof · cited by 196
- CategoryTheory.Under.rightproof · cited by 128
- Algebra.TensorProduct.mapproof · cited by 97
- CommRingCat.mkUnderproof · cited by 24
- CommRingCat.toAlgHomproof · cited by 13
Cited by12
Results whose statement or proof uses this declaration.
- CommRingCat.tensorProdIsoPushoutstatement · cited by 3
- RingHom.HasStableEqualizers.preservesLimit_parallelPair_tensorProdstatement · cited by 1
- CommRingCat.Under.tensorProdEqualizerstatement and proof · cited by 1
- CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijectivestatement and proof · cited by 1
- RingHom.HasStableEqualizers.preservesEqualizers_pushoutproof · cited by 1
- CommRingCat.Under.piFanTensorProductIsLimitstatement and proof · cited by 0
- CommRingCat.Under.tensorProdEqualizer_ιstatement · cited by 0
- CommRingCat.Under.tensorProdMapEqualizerForkIsLimitstatement and proof · cited by 0
- CommRingCat.tensorProdIsoPushout_appstatement · cited by 0
- CommRingCat.tensorProd_map_rightstatement and proof · cited by 0
- CommRingCat.tensorProd_obj_rightstatement and proof · cited by 0
- CommRingCat.Under.equalizerForkTensorProdIsostatement · cited by 0