Theorems · Theorem · category theory
CategoryTheory.Sheaf.subsingleton_H_of_isZero
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
[inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
[inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F : CategoryTheory.Sheaf J AddCommGrpCat},
CategoryTheory.Limits.IsZero F → ∀ (n : ℕ), Subsingleton (F.H n)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement · cited by 8,081
- CategoryTheory.GrothendieckTopologystatement and proof · cited by 1,415
- CategoryTheory.Presheaf.IsSheafstatement · cited by 991
- CategoryTheory.Sheafstatement and proof · cited by 763
- AddCommGrpCatstatement and proof · cited by 462
- CategoryTheory.Limits.IsZerostatement and proof · cited by 306
- CategoryTheory.HasExtstatement and proof · cited by 218
- CategoryTheory.HasSheafifystatement and proof · cited by 106
- CategoryTheory.Functor.map_isZeroproof · cited by 16
- CategoryTheory.Sheaf.Hstatement · cited by 11
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.