Theorems · Definition · category theory
ModuleCat.productConeIsLimit
{R : Type u} →
[inst : Ring R] → {ι : Type v} → (Z : ι → ModuleCat R) → CategoryTheory.Limits.IsLimit (ModuleCat.productCone Z)The concrete product cone is limiting.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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.CategoryStruct.compproof · cited by 17,999
- Ringstatement and proof · cited by 7,463
- CategoryTheory.NatTrans.appproof · cited by 7,406
- CategoryTheory.Discretestatement and proof · cited by 2,447
- ModuleCatstatement and proof · cited by 1,429
- CategoryTheory.Limits.Cone.ptproof · cited by 1,298
- CategoryTheory.Limits.Coneproof · cited by 710
- CategoryTheory.Limits.IsLimitstatement · cited by 664
- CategoryTheory.Discrete.functorstatement and proof · cited by 633
- CategoryTheory.Limits.Cone.πproof · cited by 500
- ModuleCat.Hom.homproof · cited by 341
Cited by3
Results whose statement or proof uses this declaration.
- ModuleCat.piIsoPiproof · cited by 4
- ModuleCat.piIsoPi_hom_ker_subtypeproof · cited by 1
- ModuleCat.piIsoPi_inv_kernel_ιproof · cited by 1