Basic

📁 Source: Mathlib/CategoryTheory/Sites/Point/Basic.lean

Statistics

Metric	Count
Definitions fiber, isColimitPresheafFiberCocone, isTerminalFiberObj, presheafFiber, presheafFiberCocone, presheafFiberCompIso, presheafFiberDesc, sheafFiber, sheafFiberCompIso, sheafToPresheafCompPresheafFiberIso, shrinkYonedaCompPresheafFiberIso, toPresheafFiber, toPresheafFiberNatTrans, uniqueFiberObj	14
Theorems W_isInvertedBy_presheafFiber', fiber_map_injective_of_mono, initiallySmall, instHasColimitsOfShapeOppositeElementsFiber, instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits, instIsSiftedOppositeElementsFiber, instPreservesColimitsOfShapeOppositeElementsFiberForget, instPreservesColimitsOfSizeFunctorOppositePresheafFiber, instPreservesFiniteLimitsFiber, instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, isCofiltered, jointly_surjective, presheafFiberCocone_pt, presheafFiberCocone_ι_app, presheafFiber_hom_ext, presheafFiber_hom_ext_iff, presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app, sheafFiberCompIso_hom_app, sheafFiberCompIso_inv_app, shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber, subsingleton_fiber_obj, toPresheafFiberNatTrans_app, toPresheafFiber_eq_iff', toPresheafFiber_jointly_surjective, toPresheafFiber_jointly_surjective₂, toPresheafFiber_map_bijective, toPresheafFiber_map_injective, toPresheafFiber_map_surjective, toPresheafFiber_naturality, toPresheafFiber_naturality_apply, toPresheafFiber_naturality_assoc, toPresheafFiber_presheafFiberCompIso_hom_app, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, toPresheafFiber_presheafFiberDesc, toPresheafFiber_presheafFiberDesc_assoc, toPresheafFiber_w, toPresheafFiber_w_apply, toPresheafFiber_w_assoc	39
Total	53

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
fiber 📖	CompOp	48 math math: toPresheafFiber_skyscraperPresheafHomEquiv_symm, Hom.presheafFiber_app, skyscraperPresheafFunctor_map_app, toPresheafFiber_eq_iff', comap_fiber, id_hom, ofIsCofiltered_fiber, toPresheafFiber_jointly_surjective, skyscraperPresheafHomEquiv_apply_app, fiber_map_injective_of_mono, toPresheafFiber_w, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over, toPresheafFiberMap_w, presheafFiberMapCocone_pt, toPresheafFiber_w_apply, jointly_surjective, skyscraperPresheafHomEquiv_symm_apply, instIsSiftedOppositeElementsFiber, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem_of_small, comp_hom, subsingleton_fiber_obj, skyscraperPresheafFunctor_obj_map, presheafFiberMapCocone_ι_app, instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits, instHasColimitsOfShapeOppositeElementsFiber, instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor, toPresheafFiberMap_w_assoc, toPresheafFiber_w_assoc, comp_hom_assoc, presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app, skyscraperPresheafHomEquiv_app_π_assoc, instPreservesFiniteLimitsFiber, instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor, toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc, toPresheafFiber_jointly_surjective₂, instPreservesColimitsOfShapeOppositeElementsFiberForget, shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber, map_aux, presheafFiberCocone_ι_app, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem, skyscraperPresheafFunctor_obj_obj, skyscraperPresheafHomEquiv_app_π, isCofiltered, Opens.instSubsingletonObjOpensFiber, over_fiber, CategoryTheory.GrothendieckTopology.pointBot_fiber, initiallySmall, presheafFiberCocone_pt
isColimitPresheafFiberCocone 📖	CompOp	—
isTerminalFiberObj 📖	CompOp	—
presheafFiber 📖	CompOp	83 math math: toPresheafFiber_skyscraperPresheafHomEquiv_symm, Hom.presheafFiber_app, skyscraperPresheafAdjunction_homEquiv_symm_apply, toPresheafFiber_presheafFiberDesc, toPresheafFiberOfIsCofiltered_w_assoc, toPresheafFiber_eq_iff', skyscraperPresheafHomEquiv_naturality_left_symm, skyscraperPresheafHomEquiv_naturality_left_assoc, Hom.presheafFiber_comp, toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc, toPresheafFiber_naturality_assoc, presheafFiberOfIsCofilteredCocone_ι_app, toPresheafFiber_jointly_surjective, tensorHom_comp_toPresheafFiber_μ_assoc, instPreservesColimitsOfSizeFunctorOppositePresheafFiber, W_isInvertedBy_presheafFiber', skyscraperPresheafHomEquiv_apply_app, toPresheafFiber_naturality_apply, toPresheafFiberOfIsCofiltered_naturality, toPresheafFiberMap_naturality_assoc, skyscraperPresheafHomEquiv_naturality_right_assoc, toPresheafFiber_w, Hom.presheafFiber_comp_assoc, skyscraperSheafAdjunction_homEquiv_symm_apply, toPresheafFiberMap_w, presheafFiberMapCocone_pt, presheafFiberOfIsCofilteredCocone_pt, instIsIsoδFunctorOppositePresheafFiber, tensorHom_comp_toPresheafFiber_μ, toPresheafFiber_δ_assoc, toPresheafFiberOfIsCofiltered_naturality_assoc, W_isInvertedBy_presheafFiber, skyscraperPresheafHomEquiv_naturality_left_symm_assoc, toPresheafFiber_map_bijective, instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso, skyscraperPresheafHomEquiv_naturality_right, toPresheafFiber_w_apply, CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso_inv, instIsIsoMapFunctorOppositePresheafFiberToSheafify, Hom.presheafFiber_id, toPresheafFiberMap_presheafFiberMapObjIso_hom, toPresheafFiber_δ, skyscraperPresheafHomEquiv_symm_apply, toPresheafFiberMap_naturality_apply, presheafFiberMapCocone_ι_app, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff, toPresheafFiberMap_w_assoc, skyscraperPresheafAdjunction_homEquiv_apply, toPresheafFiber_w_assoc, instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, toPresheafFiber_η, toPresheafFiber_presheafFiberMapObjIso_inv_assoc, presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app, skyscraperPresheafHomEquiv_app_π_assoc, toPresheafFiber_presheafFiberDesc_assoc, skyscraperSheafAdjunction_homEquiv_apply_val, presheafFiberMapIso_inv_app, toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc, CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId, toPresheafFiber_map_injective, toPresheafFiber_jointly_surjective₂, shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber, presheafFiberCocone_ι_app, toPresheafFiber_map_surjective, toPresheafFiber_naturality, instIsIsoηFunctorOppositePresheafFiber, toPresheafFiberNatTrans_app, toPresheafFiberOfIsCofiltered_w, presheafFiberMap_hom_ext_iff, presheafFiber_hom_ext_iff, toPresheafFiber_presheafFiberMapObjIso_inv, sheafFiberCompIso_hom_app, presheafFiberMapIso_hom_app, toPresheafFiber_ε, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, skyscraperPresheafHomEquiv_app_π, skyscraperSheafAdjunction_homEquiv_apply_hom, sheafFiberCompIso_inv_app, toPresheafFiber_presheafFiberCompIso_hom_app, toPresheafFiberMap_naturality, toPresheafFiber_η_assoc, skyscraperPresheafHomEquiv_naturality_left, presheafFiberCocone_pt
presheafFiberCocone 📖	CompOp	2 math math: presheafFiberCocone_ι_app, presheafFiberCocone_pt
presheafFiberCompIso 📖	CompOp	4 math math: sheafFiberCompIso_hom_app, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, sheafFiberCompIso_inv_app, toPresheafFiber_presheafFiberCompIso_hom_app
presheafFiberDesc 📖	CompOp	4 math math: Hom.presheafFiber_app, toPresheafFiber_presheafFiberDesc, skyscraperPresheafHomEquiv_symm_apply, toPresheafFiber_presheafFiberDesc_assoc
sheafFiber 📖	CompOp	19 math math: instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, Hom.sheafFiber_comp_assoc, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms, skyscraperSheafAdjunction_homEquiv_symm_apply, Hom.sheafFiber_comp, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type, instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso, instIsLeftAdjointSheafSheafFiber, sheafFiberComapIso_hom_app, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful, Hom.sheafFiber_id, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, skyscraperSheafAdjunction_homEquiv_apply_val, sheafFiberComapIso_inv_app, sheafFiberCompIso_hom_app, instPreservesFiniteColimitsSheafSheafFiber, skyscraperSheafAdjunction_homEquiv_apply_hom, sheafFiberCompIso_inv_app, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms
sheafFiberCompIso 📖	CompOp	2 math math: sheafFiberCompIso_hom_app, sheafFiberCompIso_inv_app
sheafToPresheafCompPresheafFiberIso 📖	CompOp	—
shrinkYonedaCompPresheafFiberIso 📖	CompOp	2 math math: presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app, shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber
toPresheafFiber 📖	CompOp	35 math math: toPresheafFiber_skyscraperPresheafHomEquiv_symm, Hom.presheafFiber_app, toPresheafFiber_presheafFiberDesc, toPresheafFiber_eq_iff', toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc, toPresheafFiber_naturality_assoc, toPresheafFiber_jointly_surjective, tensorHom_comp_toPresheafFiber_μ_assoc, skyscraperPresheafHomEquiv_apply_app, toPresheafFiber_naturality_apply, toPresheafFiber_w, tensorHom_comp_toPresheafFiber_μ, toPresheafFiber_δ_assoc, toPresheafFiber_w_apply, toPresheafFiberMap_presheafFiberMapObjIso_hom, toPresheafFiber_δ, toPresheafFiber_w_assoc, toPresheafFiber_η, toPresheafFiber_presheafFiberMapObjIso_inv_assoc, presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app, skyscraperPresheafHomEquiv_app_π_assoc, toPresheafFiber_presheafFiberDesc_assoc, toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc, toPresheafFiber_jointly_surjective₂, shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber, presheafFiberCocone_ι_app, toPresheafFiber_naturality, toPresheafFiberNatTrans_app, presheafFiber_hom_ext_iff, toPresheafFiber_presheafFiberMapObjIso_inv, toPresheafFiber_ε, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, skyscraperPresheafHomEquiv_app_π, toPresheafFiber_presheafFiberCompIso_hom_app, toPresheafFiber_η_assoc
toPresheafFiberNatTrans 📖	CompOp	3 math math: CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso_inv, CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId, toPresheafFiberNatTrans_app
uniqueFiberObj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_isInvertedBy_presheafFiber' 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.W presheafFiber	—	CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.isIso_iff_bijective toPresheafFiber_map_bijective
fiber_map_injective_of_mono 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types fiber CategoryTheory.Functor.map	—	CategoryTheory.mono_iff_injective CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsFiber
initiallySmall 📖	mathematical	—	CategoryTheory.InitiallySmall CategoryTheory.Functor.Elements fiber CategoryTheory.categoryOfElements	—	—
instHasColimitsOfShapeOppositeElementsFiber 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements	—	CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall
instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements instHasColimitsOfShapeOppositeElementsFiber	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.hasExactColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel CategoryTheory.AB5OfSize.ofShape
instIsSiftedOppositeElementsFiber 📖	mathematical	—	CategoryTheory.IsSifted Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements	—	CategoryTheory.IsFiltered.isSifted CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered
instPreservesColimitsOfShapeOppositeElementsFiberForget 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.forget	—	CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel
instPreservesColimitsOfSizeFunctorOppositePresheafFiber 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber	—	instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.comp_preservesColimitsOfShape CategoryTheory.whiskeringLeft_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Limits.instIsLeftAdjointFunctorColim
instPreservesFiniteLimitsFiber 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.types fiber	—	CategoryTheory.Limits.preservesFiniteLimits_of_natIso CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Limits.comp_preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.instPreservesLimitsOfSizeFunctorOppositeTypeShrinkYoneda instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits CategoryTheory.Limits.Types.hasLimitsOfSize CategoryTheory.Limits.instAB5Type
instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.Limits.comp_preservesFiniteLimits instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.instPreservesFiniteLimitsFunctorObjWhiskeringLeftOfHasFiniteLimits CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits
instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf sheafFiber	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.Limits.comp_preservesFiniteLimits CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize
isCofiltered 📖	mathematical	—	CategoryTheory.IsCofiltered CategoryTheory.Functor.Elements fiber CategoryTheory.categoryOfElements	—	—
jointly_surjective 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sieve.arrows CategoryTheory.Functor.obj CategoryTheory.types fiber CategoryTheory.Functor.map	—	—
presheafFiberCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π presheafFiberCocone CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber	—	—
presheafFiberCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const presheafFiber CategoryTheory.Limits.Cocone.ι presheafFiberCocone toPresheafFiber CategoryTheory.types Opposite.unop	—	—
presheafFiber_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber	—	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber
presheafFiber_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber	—	presheafFiber_hom_ext
presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category presheafFiber CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Functor.obj CategoryTheory.shrinkYoneda CategoryTheory.NatTrans.app fiber CategoryTheory.Functor.comp CategoryTheory.Iso.inv shrinkYonedaCompPresheafFiberIso toPresheafFiber DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.shrinkYonedaObjObjEquiv	—	CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber toPresheafFiber_naturality_apply CategoryTheory.Category.id_comp CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm
sheafFiberCompIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.sheafCompose sheafFiber CategoryTheory.Iso.hom sheafFiberCompIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj presheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.whiskeringRight presheafFiberCompIso CategoryTheory.CategoryStruct.id	—	—
sheafFiberCompIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp sheafFiber CategoryTheory.sheafCompose CategoryTheory.Iso.inv sheafFiberCompIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj presheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.CategoryStruct.id CategoryTheory.Functor.whiskeringRight presheafFiberCompIso	—	—
shrinkYonedaCompPresheafFiberIso_inv_app_toPresheafFiber 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types fiber CategoryTheory.Functor.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.shrinkYoneda presheafFiber CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self CategoryTheory.Iso.inv shrinkYonedaCompPresheafFiberIso toPresheafFiber CategoryTheory.Functor.obj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.shrinkYonedaObjObjEquiv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self
subsingleton_fiber_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types fiber	—	fiber_map_injective_of_mono Unique.instSubsingleton
toPresheafFiberNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.evaluation Opposite.op presheafFiber toPresheafFiberNatTrans toPresheafFiber	—	—
toPresheafFiber_eq_iff' 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.types fiber CategoryTheory.Functor.map Quiver.Hom.op	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty isCofiltered CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOppositeElementsFiberForget
toPresheafFiber_jointly_surjective 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types fiber CategoryTheory.ToType Opposite CategoryTheory.Category.opposite Opposite.op DFunLike.coe CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOppositeElementsFiberForget
toPresheafFiber_jointly_surjective₂ 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types fiber CategoryTheory.ToType Opposite CategoryTheory.Category.opposite Opposite.op DFunLike.coe CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimit₂ CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty isCofiltered CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOppositeElementsFiberForget
toPresheafFiber_map_bijective 📖	mathematical	—	Function.Bijective CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	toPresheafFiber_map_injective toPresheafFiber_map_surjective
toPresheafFiber_map_injective 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	jointly_surjective CategoryTheory.Presheaf.equalizerSieve_mem toPresheafFiber_jointly_surjective₂ toPresheafFiber_naturality_apply toPresheafFiber_w_apply
toPresheafFiber_map_surjective 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	toPresheafFiber_jointly_surjective jointly_surjective CategoryTheory.Presheaf.imageSieve_mem toPresheafFiber_naturality_apply CategoryTheory.comp_apply
toPresheafFiber_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.naturality
toPresheafFiber_naturality_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Opposite.op toPresheafFiber CategoryTheory.NatTrans.app	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toPresheafFiber_naturality
toPresheafFiber_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_naturality
toPresheafFiber_presheafFiberCompIso_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.NatTrans.app CategoryTheory.Functor.whiskeringRight CategoryTheory.Iso.hom presheafFiberCompIso CategoryTheory.Functor.map	—	CategoryTheory.ι_preservesColimitIso_inv CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber
toPresheafFiber_presheafFiberCompIso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.Functor.comp toPresheafFiber CategoryTheory.NatTrans.app CategoryTheory.Functor.whiskeringRight CategoryTheory.Iso.hom presheafFiberCompIso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_presheafFiberCompIso_hom_app
toPresheafFiber_presheafFiberDesc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber presheafFiberDesc	—	CategoryTheory.Limits.colimit.ι_desc
toPresheafFiber_presheafFiberDesc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber presheafFiberDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_presheafFiberDesc
toPresheafFiber_w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver toPresheafFiber CategoryTheory.types fiber	—	CategoryTheory.Limits.colimit.w CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber
toPresheafFiber_w_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.types fiber	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toPresheafFiber_w
toPresheafFiber_w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.types fiber	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_w

---

← Back to Index