Theorems · Theorem · category theory
CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
(A : Type u_2) [inst_1 : CategoryTheory.Category.{v_2, u_2} A] [inst_2 : CategoryTheory.HasWeakSheafify J A],
J.W =
(CategoryTheory.MorphismProperty.isomorphisms (CategoryTheory.Sheaf J A)).inverseImage
(CategoryTheory.presheafToSheaf J A)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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.MorphismPropertystatement · cited by 2,179
- CategoryTheory.GrothendieckTopologystatement and proof · cited by 1,415
- CategoryTheory.Presheaf.IsSheafstatement · cited by 991
- CategoryTheory.Sheafstatement · cited by 763
- CategoryTheory.HasWeakSheafifystatement and proof · cited by 221
- CategoryTheory.MorphismProperty.inverseImagestatement · cited by 83
- CategoryTheory.MorphismProperty.isomorphismsstatement · cited by 66
- CategoryTheory.presheafToSheafstatement · cited by 57
- CategoryTheory.GrothendieckTopology.Wstatement · cited by 35
Cited by1
Results whose statement or proof uses this declaration.
- PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphismsproof · cited by 0