Theorems · Definition · category theory
CategoryTheory.Limits.productUniqueIso
{β : Type w} →
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : Unique β] → (f : β → C) → ∏ᶜ f ≅ f defaultA product over an index type with exactly one term is just the object over that term.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Isostatement · cited by 3,963
- CategoryTheory.Discrete.functorproof · cited by 633
- Uniquestatement and proof · cited by 400
- CategoryTheory.Limits.piObjstatement · cited by 237
- CategoryTheory.Limits.limit.isLimitproof · cited by 146
- CategoryTheory.Limits.LimitCone.isLimitproof · cited by 58
- CategoryTheory.Limits.IsLimit.conePointUniqueUpToIsoproof · cited by 57
- CategoryTheory.Limits.limitConeOfUniqueproof · cited by 4
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.productUniqueIso_inv_πstatement and proof · cited by 2
- CategoryTheory.Limits.productUniqueIso_homstatement · cited by 0
- CategoryTheory.Limits.productUniqueIso_invstatement · cited by 0
- CategoryTheory.Limits.productUniqueIso_inv_π_assocstatement and proof · cited by 0
- CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheafΓNatIsoIdproof · cited by 0