Theorems · Theorem · commutative algebra
CommRingCat.Limits.isUnit_iff_forall_isUnit
∀ {J : Type u'} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
{c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (r : ↑c.pt),
IsUnit r ↔ ∀ (j : J), IsUnit ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) r)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.SmallCategory
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites41
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- RingHomstatement · cited by 10,189
- CategoryTheory.Functor.mapproof · cited by 8,698
- CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- CommRingCatstatement and proof · cited by 2,333
- mul_commproof · cited by 2,262
Cited by1
Results whose statement or proof uses this declaration.
- CommRingCat.Limits.π_isLocalHomproof · cited by 1