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, comp_of_W_map_of_adjunction, W_shrinkFunctor_ι_of_mem	12
Total	12

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.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit	—	W_eq_isLocal_range_sheafToPresheaf_obj CategoryTheory.ObjectProperty.isLocal_adj_unit_app CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
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.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.MorphismProperty.isomorphisms	—	W_eq_isLocal_range_sheafToPresheaf_obj CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
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.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf	—	CategoryTheory.ObjectProperty.FullSubcategory.property
W_iff 📖	mathematical	—	W CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.presheafToSheaf CategoryTheory.Functor.map	—	W_iff_isIso_map_of_adjunction
W_iff_isIso_map_of_adjunction 📖	mathematical	—	W CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	W_eq_isLocal_range_sheafToPresheaf_obj CategoryTheory.ObjectProperty.isLocal_iff_isIso_map CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
W_sheafToPresheaf_map_iff_isIso 📖	mathematical	—	W CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
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.ObjectProperty.FullSubcategory.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.presheafToSheaf W	—	W_eq_inverseImage_isomorphisms CategoryTheory.Adjunction.isLocalization CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι

CategoryTheory.Presieve.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_of_W_map_of_adjunction 📖	mathematical	CategoryTheory.GrothendieckTopology.W CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.shrinkYoneda CategoryTheory.Sieve.shrinkFunctor CategoryTheory.Functor.map CategoryTheory.Subfunctor.ι CategoryTheory.Presieve.IsSheaf	CategoryTheory.Presieve.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op	—	CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp CategoryTheory.Functor.whiskeringLeft_obj_obj CategoryTheory.Adjunction.map_comp_bijective_iff CategoryTheory.isSheaf_iff_isSheaf_of_type

CategoryTheory.Sieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_shrinkFunctor_ι_of_mem 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.GrothendieckTopology.W CategoryTheory.types CategoryTheory.Subfunctor.toFunctor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shrinkYoneda shrinkFunctor CategoryTheory.Subfunctor.ι	—	CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp CategoryTheory.isSheaf_iff_isSheaf_of_type

---

← Back to Index