Localization

📁 Source: Mathlib/CategoryTheory/Sites/Localization.lean

Statistics

Metric	Count
Definitions	0
Theorems W_adj_unit_app, W_eq_W_range_sheafToPresheaf_obj, W_eq_inverseImage_isomorphisms, W_eq_inverseImage_isomorphisms_of_adjunction, W_eq_isLocal_range_sheafToPresheaf_obj, W_iff, W_iff_isIso_map_of_adjunction, W_sheafToPresheaf_map_iff_isIso, W_toSheafify, instIsLocalizationFunctorOppositeSheafPresheafToSheafW	10
Total	10

CategoryTheory.GrothendieckTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_adj_unit_app 📖	mathematical	—	W CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.sheafToPresheaf CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit	—	W_eq_isLocal_range_sheafToPresheaf_obj CategoryTheory.ObjectProperty.isLocal_adj_unit_app CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf
W_eq_W_range_sheafToPresheaf_obj 📖	mathematical	—	W CategoryTheory.ObjectProperty.isLocal CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Set Set.instMembership Set.range CategoryTheory.Sheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.sheafToPresheaf	—	W_eq_isLocal_range_sheafToPresheaf_obj
W_eq_inverseImage_isomorphisms 📖	mathematical	—	W CategoryTheory.MorphismProperty.inverseImage CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.MorphismProperty.isomorphisms CategoryTheory.presheafToSheaf	—	W_eq_inverseImage_isomorphisms_of_adjunction
W_eq_inverseImage_isomorphisms_of_adjunction 📖	mathematical	—	W CategoryTheory.MorphismProperty.inverseImage CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.MorphismProperty.isomorphisms	—	W_eq_isLocal_range_sheafToPresheaf_obj CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf
W_eq_isLocal_range_sheafToPresheaf_obj 📖	mathematical	—	W CategoryTheory.ObjectProperty.isLocal CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Set Set.instMembership Set.range CategoryTheory.Sheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.sheafToPresheaf	—	CategoryTheory.Sheaf.cond
W_iff 📖	mathematical	—	W CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.presheafToSheaf CategoryTheory.Functor.map	—	W_iff_isIso_map_of_adjunction
W_iff_isIso_map_of_adjunction 📖	mathematical	—	W CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.map	—	W_eq_isLocal_range_sheafToPresheaf_obj CategoryTheory.ObjectProperty.isLocal_iff_isIso_map CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf
W_sheafToPresheaf_map_iff_isIso 📖	mathematical	—	W CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.sheafToPresheaf CategoryTheory.Functor.map CategoryTheory.IsIso	—	W_eq_isLocal_range_sheafToPresheaf_obj CategoryTheory.ObjectProperty.isLocal_iff_isIso CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf
W_toSheafify 📖	mathematical	—	W CategoryTheory.sheafify CategoryTheory.toSheafify	—	W_adj_unit_app
instIsLocalizationFunctorOppositeSheafPresheafToSheafW 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf CategoryTheory.Functor.category CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.presheafToSheaf W	—	W_eq_inverseImage_isomorphisms CategoryTheory.Adjunction.isLocalization CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf

---

← Back to Index