Theorems · Theorem · category theory
CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical]
(P : CategoryTheory.Functor Cᵒᵖ (Type w)) [P.IsRepresentable], CategoryTheory.Presieve.IsSheaf J PIf J is subcanonical, then any representable is a J-sheaf.
- Defined in
- Mathlib.CategoryTheory.Sites.Canonical
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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 and proof · cited by 16,252
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.GrothendieckTopologystatement and proof · cited by 1,415
- CategoryTheory.Presieve.IsSheafstatement · cited by 66
- CategoryTheory.GrothendieckTopology.Subcanonicalstatement and proof · cited by 55
- CategoryTheory.Functor.IsRepresentablestatement and proof · cited by 24
- CategoryTheory.Presieve.isSheaf_of_leproof · cited by 4
- CategoryTheory.GrothendieckTopology.le_canonicalproof · cited by 2
- CategoryTheory.Sheaf.isSheaf_of_isRepresentableproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphismsproof · cited by 2
- CategoryTheory.Precoverage.ZeroHypercover.hom_extproof · cited by 1
- AlgebraicGeometry.isSheaf_zariskiTopology_continuousMapPresheafproof · cited by 1
- CategoryTheory.GrothendieckTopology.subcanonical_of_full_of_faithfulproof · cited by 0
- CategoryTheory.GrothendieckTopology.Subcanonical.of_leproof · cited by 0