Map

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

Statistics

Metric	Count
Definitions isColimitPresheafFiberMapCocone, map, presheafFiberMapCocone, presheafFiberMapIso, presheafFiberMapObjIso, sheafFiberMapIso, toPresheafFiberMap	7
Theorems map_aux, presheafFiberMapCocone_pt, presheafFiberMapCocone_ι_app, presheafFiberMapIso_hom_app, presheafFiberMapIso_inv_app, presheafFiberMap_hom_ext, presheafFiberMap_hom_ext_iff, toPresheafFiberMap_naturality, toPresheafFiberMap_naturality_apply, toPresheafFiberMap_naturality_assoc, toPresheafFiberMap_presheafFiberMapObjIso_hom, toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc, toPresheafFiberMap_w, toPresheafFiberMap_w_assoc, toPresheafFiber_presheafFiberMapObjIso_inv, toPresheafFiber_presheafFiberMapObjIso_inv_assoc	16
Total	23

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
isColimitPresheafFiberMapCocone 📖	CompOp	—
map 📖	CompOp	14 math math: toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc, toPresheafFiberMap_naturality_assoc, toPresheafFiberMap_w, presheafFiberMapCocone_pt, toPresheafFiberMap_presheafFiberMapObjIso_hom, toPresheafFiberMap_naturality_apply, presheafFiberMapCocone_ι_app, toPresheafFiberMap_w_assoc, toPresheafFiber_presheafFiberMapObjIso_inv_assoc, presheafFiberMapIso_inv_app, presheafFiberMap_hom_ext_iff, toPresheafFiber_presheafFiberMapObjIso_inv, presheafFiberMapIso_hom_app, toPresheafFiberMap_naturality
presheafFiberMapCocone 📖	CompOp	2 math math: presheafFiberMapCocone_pt, presheafFiberMapCocone_ι_app
presheafFiberMapIso 📖	CompOp	2 math math: presheafFiberMapIso_inv_app, presheafFiberMapIso_hom_app
presheafFiberMapObjIso 📖	CompOp	6 math math: toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc, toPresheafFiberMap_presheafFiberMapObjIso_hom, toPresheafFiber_presheafFiberMapObjIso_inv_assoc, presheafFiberMapIso_inv_app, toPresheafFiber_presheafFiberMapObjIso_inv, presheafFiberMapIso_hom_app
sheafFiberMapIso 📖	CompOp	—
toPresheafFiberMap 📖	CompOp	11 math math: toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc, toPresheafFiberMap_naturality_assoc, toPresheafFiberMap_w, toPresheafFiberMap_presheafFiberMapObjIso_hom, toPresheafFiberMap_naturality_apply, presheafFiberMapCocone_ι_app, toPresheafFiberMap_w_assoc, toPresheafFiber_presheafFiberMapObjIso_inv_assoc, presheafFiberMap_hom_ext_iff, toPresheafFiber_presheafFiberMapObjIso_inv, toPresheafFiberMap_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_aux 📖	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.Elements fiber CategoryTheory.categoryOfElements CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	jointly_surjective CategoryTheory.Functor.cover_lift CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Category.id_comp
presheafFiberMapCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.CategoryOfElements.π presheafFiberMapCocone CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map	—	—
presheafFiberMapCocone_ι_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 map CategoryTheory.Limits.Cocone.ι presheafFiberMapCocone toPresheafFiberMap CategoryTheory.types Opposite.unop	—	—
presheafFiberMapIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber map CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.Iso.hom presheafFiberMapIso presheafFiberMapObjIso	—	—
presheafFiberMapIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op presheafFiber map CategoryTheory.Iso.inv presheafFiberMapIso presheafFiberMapObjIso	—	—
presheafFiberMap_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map toPresheafFiberMap	—	—	CategoryTheory.Limits.IsColimit.hom_ext
presheafFiberMap_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 map toPresheafFiberMap	—	presheafFiberMap_hom_ext
toPresheafFiberMap_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map toPresheafFiberMap CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	toPresheafFiberOfIsCofiltered_naturality initiallySmall isCofiltered map_aux
toPresheafFiberMap_naturality_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber map CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Opposite.op toPresheafFiberMap CategoryTheory.NatTrans.app	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toPresheafFiberMap_naturality
toPresheafFiberMap_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map toPresheafFiberMap CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiberMap_naturality
toPresheafFiberMap_presheafFiberMapObjIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map CategoryTheory.Functor.comp CategoryTheory.Functor.op toPresheafFiberMap CategoryTheory.Iso.hom presheafFiberMapObjIso toPresheafFiber	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
toPresheafFiberMap_presheafFiberMapObjIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map toPresheafFiberMap CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Iso.hom presheafFiberMapObjIso toPresheafFiber	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiberMap_presheafFiberMapObjIso_hom
toPresheafFiberMap_w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver toPresheafFiberMap CategoryTheory.types fiber	—	toPresheafFiberOfIsCofiltered_w initiallySmall isCofiltered map_aux
toPresheafFiberMap_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 map toPresheafFiberMap CategoryTheory.types fiber	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiberMap_w
toPresheafFiber_presheafFiberMapObjIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber map toPresheafFiber CategoryTheory.Iso.inv presheafFiberMapObjIso toPresheafFiberMap	—	CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.eq_whisker toPresheafFiberMap_presheafFiberMapObjIso_hom
toPresheafFiber_presheafFiberMapObjIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.Functor.comp toPresheafFiber map CategoryTheory.Iso.inv presheafFiberMapObjIso toPresheafFiberMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_presheafFiberMapObjIso_inv

---

← Back to Index