Skyscraper

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

Statistics

Metric	Count
Definitions instLiftingFunctorOppositeSheafPresheafToSheafWPresheafFiberSheafFiber, presheafToSheafCompSheafFiber, presheafToSheafCompSheafFiberIso, skyscraperPresheaf, skyscraperPresheafAdjunction, skyscraperPresheafFunctor, skyscraperPresheafHomEquiv, skyscraperSheaf, skyscraperSheafAdjunction, skyscraperSheafFunctor	10
Theorems W_isInvertedBy_presheafFiber, instIsIsoMapFunctorOppositePresheafFiberToSheafify, instIsLeftAdjointSheafSheafFiber, instIsRightAdjointSheafSkyscraperSheafFunctor, instPreservesFiniteColimitsSheafSheafFiber, isSheaf_skyscraperPresheaf, skyscraperPresheafAdjunction_homEquiv_apply, skyscraperPresheafAdjunction_homEquiv_symm_apply, skyscraperPresheafFunctor_map_app, skyscraperPresheafFunctor_obj_map, skyscraperPresheafFunctor_obj_obj, skyscraperPresheafHomEquiv_app_π, skyscraperPresheafHomEquiv_app_π_assoc, skyscraperPresheafHomEquiv_apply_app, skyscraperPresheafHomEquiv_naturality_left, skyscraperPresheafHomEquiv_naturality_left_assoc, skyscraperPresheafHomEquiv_naturality_left_symm, skyscraperPresheafHomEquiv_naturality_left_symm_assoc, skyscraperPresheafHomEquiv_naturality_right, skyscraperPresheafHomEquiv_naturality_right_assoc, skyscraperPresheafHomEquiv_symm_apply, skyscraperSheafAdjunction_homEquiv_apply_hom, skyscraperSheafAdjunction_homEquiv_apply_val, skyscraperSheafAdjunction_homEquiv_symm_apply, skyscraperSheafFunctor_map_hom, skyscraperSheafFunctor_obj_obj, toPresheafFiber_skyscraperPresheafHomEquiv_symm, toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc	28
Total	38

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
instLiftingFunctorOppositeSheafPresheafToSheafWPresheafFiberSheafFiber 📖	CompOp	—
presheafToSheafCompSheafFiber 📖	CompOp	—
presheafToSheafCompSheafFiberIso 📖	CompOp	1 math math: instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso
skyscraperPresheaf 📖	CompOp	20 math math: toPresheafFiber_skyscraperPresheafHomEquiv_symm, skyscraperPresheafAdjunction_homEquiv_symm_apply, skyscraperSheafFunctor_obj_obj, skyscraperPresheafHomEquiv_naturality_left_symm, skyscraperPresheafHomEquiv_naturality_left_assoc, skyscraperPresheafHomEquiv_apply_app, isSheaf_skyscraperPresheaf, skyscraperPresheafHomEquiv_naturality_right_assoc, skyscraperSheafAdjunction_homEquiv_symm_apply, skyscraperSheafFunctor_map_hom, skyscraperPresheafHomEquiv_naturality_left_symm_assoc, skyscraperPresheafHomEquiv_naturality_right, skyscraperPresheafHomEquiv_symm_apply, skyscraperPresheafAdjunction_homEquiv_apply, skyscraperPresheafHomEquiv_app_π_assoc, skyscraperSheafAdjunction_homEquiv_apply_val, toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc, skyscraperPresheafHomEquiv_app_π, skyscraperSheafAdjunction_homEquiv_apply_hom, skyscraperPresheafHomEquiv_naturality_left
skyscraperPresheafAdjunction 📖	CompOp	2 math math: skyscraperPresheafAdjunction_homEquiv_symm_apply, skyscraperPresheafAdjunction_homEquiv_apply
skyscraperPresheafFunctor 📖	CompOp	8 math math: skyscraperPresheafAdjunction_homEquiv_symm_apply, skyscraperPresheafFunctor_map_app, skyscraperPresheafHomEquiv_naturality_right_assoc, skyscraperSheafFunctor_map_hom, skyscraperPresheafHomEquiv_naturality_right, skyscraperPresheafFunctor_obj_map, skyscraperPresheafAdjunction_homEquiv_apply, skyscraperPresheafFunctor_obj_obj
skyscraperPresheafHomEquiv 📖	CompOp	17 math math: toPresheafFiber_skyscraperPresheafHomEquiv_symm, skyscraperPresheafAdjunction_homEquiv_symm_apply, skyscraperPresheafHomEquiv_naturality_left_symm, skyscraperPresheafHomEquiv_naturality_left_assoc, skyscraperPresheafHomEquiv_apply_app, skyscraperPresheafHomEquiv_naturality_right_assoc, skyscraperSheafAdjunction_homEquiv_symm_apply, skyscraperPresheafHomEquiv_naturality_left_symm_assoc, skyscraperPresheafHomEquiv_naturality_right, skyscraperPresheafHomEquiv_symm_apply, skyscraperPresheafAdjunction_homEquiv_apply, skyscraperPresheafHomEquiv_app_π_assoc, skyscraperSheafAdjunction_homEquiv_apply_val, toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc, skyscraperPresheafHomEquiv_app_π, skyscraperSheafAdjunction_homEquiv_apply_hom, skyscraperPresheafHomEquiv_naturality_left
skyscraperSheaf 📖	CompOp	1 math math: skyscraperSheafAdjunction_homEquiv_symm_apply
skyscraperSheafAdjunction 📖	CompOp	5 math math: skyscraperSheafAdjunction_homEquiv_symm_apply, sheafFiberComapIso_hom_app, skyscraperSheafAdjunction_homEquiv_apply_val, sheafFiberComapIso_inv_app, skyscraperSheafAdjunction_homEquiv_apply_hom
skyscraperSheafFunctor 📖	CompOp	8 math math: skyscraperSheafFunctor_obj_obj, skyscraperSheafAdjunction_homEquiv_symm_apply, skyscraperSheafFunctor_map_hom, sheafFiberComapIso_hom_app, instIsRightAdjointSheafSkyscraperSheafFunctor, skyscraperSheafAdjunction_homEquiv_apply_val, sheafFiberComapIso_inv_app, skyscraperSheafAdjunction_homEquiv_apply_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_isInvertedBy_presheafFiber 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.W presheafFiber	—	CategoryTheory.isIso_iff_coyoneda_map_bijective Function.Bijective.of_comp_iff' Equiv.bijective skyscraperPresheafHomEquiv_naturality_left Function.Bijective.comp isSheaf_skyscraperPresheaf
instIsIsoMapFunctorOppositePresheafFiberToSheafify 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber CategoryTheory.sheafify CategoryTheory.Functor.map CategoryTheory.toSheafify	—	W_isInvertedBy_presheafFiber CategoryTheory.GrothendieckTopology.W_toSheafify
instIsLeftAdjointSheafSheafFiber 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf sheafFiber	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointSheafSkyscraperSheafFunctor 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf skyscraperSheafFunctor	—	CategoryTheory.Adjunction.isRightAdjoint
instPreservesFiniteColimitsSheafSheafFiber 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf sheafFiber	—	CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint instIsLeftAdjointSheafSheafFiber CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits
isSheaf_skyscraperPresheaf 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Presheaf.IsSheaf skyscraperPresheaf	—	CategoryTheory.Presheaf.isSheaf_iff_isLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.Pi.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.Pi.map'_comp_π CategoryTheory.Category.comp_id jointly_surjective
skyscraperPresheafAdjunction_homEquiv_apply 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber skyscraperPresheafFunctor EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv skyscraperPresheafAdjunction skyscraperPresheaf skyscraperPresheafHomEquiv	—	skyscraperPresheafHomEquiv_naturality_left_symm skyscraperPresheafHomEquiv_naturality_right CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
skyscraperPresheafAdjunction_homEquiv_symm_apply 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj skyscraperPresheafFunctor presheafFiber EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv skyscraperPresheafAdjunction skyscraperPresheaf skyscraperPresheafHomEquiv	—	skyscraperPresheafHomEquiv_naturality_left_symm skyscraperPresheafHomEquiv_naturality_right CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
skyscraperPresheafFunctor_map_app 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.op fiber CategoryTheory.Functor.flip CategoryTheory.Limits.piFunctor CategoryTheory.Functor.map skyscraperPresheafFunctor CategoryTheory.Limits.Pi.map Opposite.unop Opposite.op	—	—
skyscraperPresheafFunctor_obj_map 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category skyscraperPresheafFunctor CategoryTheory.Limits.Pi.map' CategoryTheory.types fiber Opposite.unop Opposite.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
skyscraperPresheafFunctor_obj_obj 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category skyscraperPresheafFunctor CategoryTheory.Limits.piObj CategoryTheory.types fiber Opposite.unop Opposite.op	—	—
skyscraperPresheafHomEquiv_app_π 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op skyscraperPresheaf CategoryTheory.NatTrans.app DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber EquivLike.toFunLike Equiv.instEquivLike skyscraperPresheafHomEquiv CategoryTheory.Limits.Pi.π CategoryTheory.types fiber CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor toPresheafFiber	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.limit.lift_π
skyscraperPresheafHomEquiv_app_π_assoc 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op skyscraperPresheaf CategoryTheory.NatTrans.app DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber EquivLike.toFunLike Equiv.instEquivLike skyscraperPresheafHomEquiv CategoryTheory.Limits.Pi.π CategoryTheory.types fiber CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor toPresheafFiber	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' skyscraperPresheafHomEquiv_app_π
skyscraperPresheafHomEquiv_apply_app 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite skyscraperPresheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber EquivLike.toFunLike Equiv.instEquivLike skyscraperPresheafHomEquiv CategoryTheory.Limits.Pi.lift Opposite.unop CategoryTheory.types CategoryTheory.Functor.op fiber CategoryTheory.CategoryStruct.comp toPresheafFiber	—	—
skyscraperPresheafHomEquiv_naturality_left 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber skyscraperPresheaf EquivLike.toFunLike Equiv.instEquivLike skyscraperPresheafHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	Equiv.injective Equiv.symm_apply_apply skyscraperPresheafHomEquiv_naturality_left_symm
skyscraperPresheafHomEquiv_naturality_left_assoc 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category skyscraperPresheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj presheafFiber EquivLike.toFunLike Equiv.instEquivLike skyscraperPresheafHomEquiv CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' skyscraperPresheafHomEquiv_naturality_left
skyscraperPresheafHomEquiv_naturality_left_symm 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category skyscraperPresheaf CategoryTheory.Functor.obj presheafFiber EquivLike.toFunLike Equiv.instEquivLike Equiv.symm skyscraperPresheafHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	presheafFiber_hom_ext toPresheafFiber_skyscraperPresheafHomEquiv_symm CategoryTheory.Category.assoc toPresheafFiber_naturality_assoc
skyscraperPresheafHomEquiv_naturality_left_symm_assoc 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver skyscraperPresheaf EquivLike.toFunLike Equiv.instEquivLike Equiv.symm skyscraperPresheafHomEquiv CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' skyscraperPresheafHomEquiv_naturality_left_symm
skyscraperPresheafHomEquiv_naturality_right 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber skyscraperPresheaf EquivLike.toFunLike Equiv.instEquivLike skyscraperPresheafHomEquiv CategoryTheory.CategoryStruct.comp skyscraperPresheafFunctor CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.Pi.hom_ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape skyscraperPresheafHomEquiv_app_π CategoryTheory.Category.assoc CategoryTheory.Limits.Pi.map_π skyscraperPresheafHomEquiv_app_π_assoc
skyscraperPresheafHomEquiv_naturality_right_assoc 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category skyscraperPresheaf DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj presheafFiber EquivLike.toFunLike Equiv.instEquivLike skyscraperPresheafHomEquiv CategoryTheory.Functor.map skyscraperPresheafFunctor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' skyscraperPresheafHomEquiv_naturality_right
skyscraperPresheafHomEquiv_symm_apply 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category skyscraperPresheaf CategoryTheory.Functor.obj presheafFiber EquivLike.toFunLike Equiv.instEquivLike Equiv.symm skyscraperPresheafHomEquiv presheafFiberDesc CategoryTheory.CategoryStruct.comp Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Limits.Pi.π CategoryTheory.types fiber	—	—
skyscraperSheafAdjunction_homEquiv_apply_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category skyscraperSheafFunctor DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct presheafFiber EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv sheafFiber skyscraperSheafAdjunction skyscraperPresheaf skyscraperPresheafHomEquiv	—	CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
skyscraperSheafAdjunction_homEquiv_apply_val 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category skyscraperSheafFunctor DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct presheafFiber EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv sheafFiber skyscraperSheafAdjunction skyscraperPresheaf skyscraperPresheafHomEquiv	—	skyscraperSheafAdjunction_homEquiv_apply_hom
skyscraperSheafAdjunction_homEquiv_symm_apply 📖	mathematical	CategoryTheory.Limits.HasProducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj skyscraperSheafFunctor presheafFiber CategoryTheory.ObjectProperty.FullSubcategory.obj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv sheafFiber skyscraperSheafAdjunction skyscraperPresheaf skyscraperPresheafHomEquiv CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory skyscraperSheaf	—	CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
skyscraperSheafFunctor_map_hom 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj skyscraperPresheaf isSheaf_skyscraperPresheaf CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category skyscraperSheafFunctor skyscraperPresheafFunctor	—	isSheaf_skyscraperPresheaf
skyscraperSheafFunctor_obj_obj 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category skyscraperSheafFunctor skyscraperPresheaf	—	—
toPresheafFiber_skyscraperPresheafHomEquiv_symm 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver skyscraperPresheaf EquivLike.toFunLike Equiv.instEquivLike Equiv.symm skyscraperPresheafHomEquiv CategoryTheory.NatTrans.app CategoryTheory.Limits.Pi.π CategoryTheory.types fiber CategoryTheory.Functor.op	—	toPresheafFiber_presheafFiberDesc
toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver skyscraperPresheaf EquivLike.toFunLike Equiv.instEquivLike Equiv.symm skyscraperPresheafHomEquiv CategoryTheory.NatTrans.app CategoryTheory.Limits.Pi.π CategoryTheory.types fiber CategoryTheory.Functor.op	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_skyscraperPresheafHomEquiv_symm

---

← Back to Index