OneHypercoverDense

📁 Source: Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean

Statistics

Metric	Count
Definitions IsOneHypercoverDense, OneHypercoverDenseData, SieveStruct, i₀, q, presheaf, presheafMap, presheafObj, presheafObjIsLimit, presheafObjMultifork, presheafObjπ, restriction, res, isLimit, liftAux, sieve, toOneHypercover, toPreOneHypercoverDenseData, PreOneHypercoverDenseData, I₀, I₁, I₁', X, Y, f, multicospanIndex, multicospanMap, multicospanMapIso, multicospanShape, p₁, p₂, sieve₁₀, toPreOneHypercover, oneHypercoverDenseData	34
Theorems nonempty_oneHypercoverDenseData, of_hasPullbacks, fac, fac_assoc, presheafMap_comp, presheafMap_comp_assoc, presheafMap_id, presheafMap_restriction, presheafMap_restriction_assoc, presheafMap_π, presheafMap_π_assoc, presheafObj_condition, presheafObj_condition_assoc, presheafObj_hom_ext, presheafObj_hom_ext_iff, presheafObj_mapPreimage_condition, presheaf_map, presheaf_obj, res_eq_res, restriction_eq_of_fac, restriction_map, isSheaf_iff, fac, fac_assoc, hom_ext, liftAux_fac, lift_map, lift_map_assoc, mem₀, mem₁, mem₁₀, sieve_apply, sieve_mem, toOneHypercover_toPreOneHypercover, multicospanIndex_fst, multicospanIndex_left, multicospanIndex_right, multicospanIndex_snd, multicospanMapIso_hom, multicospanMapIso_inv, multicospanMap_app, multicospanShape_L, multicospanShape_R, multicospanShape_fst, multicospanShape_snd, sieve₁₀_apply, toPreOneHypercover_I₀, toPreOneHypercover_I₁, toPreOneHypercover_X, toPreOneHypercover_Y, toPreOneHypercover_f, toPreOneHypercover_p₁, toPreOneHypercover_p₂, w, w_assoc, isDenseSubsite_of_isOneHypercoverDense	56
Total	90

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsOneHypercoverDense 📖	CompData	1 math math: IsOneHypercoverDense.of_hasPullbacks
OneHypercoverDenseData 📖	CompData	1 math math: IsOneHypercoverDense.nonempty_oneHypercoverDenseData
PreOneHypercoverDenseData 📖	CompData	—
oneHypercoverDenseData 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDenseSubsite_of_isOneHypercoverDense 📖	mathematical	CategoryTheory.Sieve obj Set Set.instMembership CategoryTheory.GrothendieckTopology.sieves CategoryTheory.Sieve.functorPushforward	IsDenseSubsite	—	CategoryTheory.GrothendieckTopology.superset_covering OneHypercoverDenseData.mem₀

CategoryTheory.Functor.IsOneHypercoverDense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_oneHypercoverDenseData 📖	mathematical	—	CategoryTheory.Functor.OneHypercoverDenseData	—	—
of_hasPullbacks 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Functor.obj	CategoryTheory.Functor.IsOneHypercoverDense	—	CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.Functor.map_preimage CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition CategoryTheory.Functor.IsDenseSubsite.isCoverDense CategoryTheory.Functor.functorPushforward_mem_iff CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.eq_whisker CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Limits.pullback.lift_fst CategoryTheory.Limits.pullback.lift_snd CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering CategoryTheory.Functor.IsLocallyFull.of_full

CategoryTheory.Functor.OneHypercoverDenseData

Definitions

Name	Category	Theorems
SieveStruct 📖	CompData	1 math math: sieve_apply
sieve 📖	CompOp	2 math math: sieve_apply, sieve_mem
toOneHypercover 📖	CompOp	2 math math: isSheaf_iff, toOneHypercover_toPreOneHypercover
toPreOneHypercoverDenseData 📖	CompOp	11 math math: essSurj.presheafMap_π_assoc, essSurj.presheafObj_condition_assoc, SieveStruct.fac, mem₀, essSurj.presheafObj_condition, SieveStruct.fac_assoc, essSurj.presheafObj_hom_ext_iff, essSurj.presheafMap_π, toOneHypercover_toPreOneHypercover, isSheaf_iff.lift_map, isSheaf_iff.lift_map_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_iff 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Limits.IsLimit CategoryTheory.Limits.WalkingMulticospan CategoryTheory.PreOneHypercover.multicospanShape CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover toOneHypercover CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.PreOneHypercover.multicospanIndex CategoryTheory.PreOneHypercover.multifork	—	CategoryTheory.Functor.op_comp_isSheaf CategoryTheory.Functor.IsDenseSubsite.instIsContinuous CategoryTheory.Presheaf.isSheaf_iff_multifork
mem₀ 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreZeroHypercover.sieve₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover toPreOneHypercoverDenseData	—	—
mem₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X toPreOneHypercoverDenseData CategoryTheory.Functor.PreOneHypercoverDenseData.f	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreOneHypercover.sieve₁ CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover	—	CategoryTheory.Functor.IsDenseSubsite.isCoverDense CategoryTheory.Presieve.BindStruct.hf CategoryTheory.Presieve.BindStruct.hg CategoryTheory.Presieve.FunctorPushforwardStructure.cover CategoryTheory.GrothendieckTopology.bind_covering CategoryTheory.Functor.is_cover_of_isCoverDense CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Functor.functorPushforward_mem_iff CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem mem₁₀ CategoryTheory.Category.assoc CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Functor.map_comp Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Presieve.FunctorPushforwardStructure.fac CategoryTheory.Presieve.CoverByImageStructure.fac_assoc CategoryTheory.Presieve.BindStruct.fac_assoc
mem₁₀ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X toPreOneHypercoverDenseData CategoryTheory.Functor.map CategoryTheory.Functor.PreOneHypercoverDenseData.f	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀	—	—
sieve_apply 📖	mathematical	—	CategoryTheory.Sieve.arrows sieve SieveStruct	—	—
sieve_mem 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve sieve	—	CategoryTheory.Functor.IsDenseSubsite.isCoverDense CategoryTheory.Functor.IsDenseSubsite.isLocallyFull CategoryTheory.Functor.functorPushforward_mem_iff CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Sieve.ofArrows.fac CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Presieve.CoverByImageStructure.fac_assoc CategoryTheory.GrothendieckTopology.bind_covering CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.GrothendieckTopology.OneHypercover.mem₀ CategoryTheory.Functor.is_cover_of_isCoverDense CategoryTheory.Functor.functorPushforward_imageSieve_mem
toOneHypercover_toPreOneHypercover 📖	mathematical	—	CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover toOneHypercover CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover toPreOneHypercoverDenseData	—	—

CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct

Definitions

Name	Category	Theorems
i₀ 📖	CompOp	2 math math: fac, fac_assoc
q 📖	CompOp	2 math math: fac, fac_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData i₀ q CategoryTheory.Functor.PreOneHypercoverDenseData.f CategoryTheory.Functor.map	—	—
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData i₀ q CategoryTheory.Functor.PreOneHypercoverDenseData.f CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac

CategoryTheory.Functor.OneHypercoverDenseData.essSurj

Definitions

Name	Category	Theorems
presheaf 📖	CompOp	2 math math: presheaf_obj, presheaf_map
presheafMap 📖	CompOp	8 math math: presheafMap_π_assoc, presheafMap_restriction_assoc, presheafMap_comp, presheafMap_comp_assoc, presheaf_map, presheafMap_id, presheafMap_restriction, presheafMap_π
presheafObj 📖	CompOp	14 math math: presheaf_obj, presheafMap_π_assoc, presheafObj_mapPreimage_condition, presheafMap_restriction_assoc, presheafMap_comp, presheafObj_condition_assoc, presheafMap_comp_assoc, presheafMap_id, presheafObj_condition, presheafMap_restriction, presheafObj_hom_ext_iff, presheafMap_π, restriction_map, restriction_eq_of_fac
presheafObjIsLimit 📖	CompOp	—
presheafObjMultifork 📖	CompOp	—
presheafObjπ 📖	CompOp	8 math math: presheafMap_π_assoc, presheafObj_mapPreimage_condition, presheafObj_condition_assoc, presheafObj_condition, presheafObj_hom_ext_iff, presheafMap_π, restriction_map, restriction_eq_of_fac
restriction 📖	CompOp	6 math math: presheafMap_π_assoc, presheafMap_restriction_assoc, presheafMap_restriction, presheafMap_π, restriction_map, restriction_eq_of_fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presheafMap_comp 📖	mathematical	—	presheafMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj	—	presheafObj_hom_ext CategoryTheory.Category.assoc presheafMap_π presheafMap_restriction
presheafMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj presheafMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafMap_comp
presheafMap_id 📖	mathematical	—	presheafMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct presheafObj	—	presheafObj_hom_ext presheafMap_π CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp restriction_eq_of_fac CategoryTheory.Functor.IsDenseSubsite.mapPreimage_id
presheafMap_restriction 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op presheafMap restriction	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Sheaf.cond CategoryTheory.GrothendieckTopology.bind_covering CategoryTheory.Functor.cover_lift CategoryTheory.Functor.IsDenseSubsite.instIsCocontinuous CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Functor.OneHypercoverDenseData.mem₀ CategoryTheory.Sieve.ofArrows.fac CategoryTheory.Category.assoc CategoryTheory.op_comp restriction_map presheafMap_π_assoc CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac CategoryTheory.Functor.map_comp CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map
presheafMap_restriction_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj presheafMap CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op restriction	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafMap_restriction
presheafMap_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafMap presheafObjπ restriction CategoryTheory.Functor.PreOneHypercoverDenseData.f	—	CategoryTheory.Limits.Multiequalizer.lift_ι
presheafMap_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj presheafMap CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafObjπ restriction CategoryTheory.Functor.PreOneHypercoverDenseData.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafMap_π
presheafObj_condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.PreOneHypercoverDenseData.Y presheafObjπ CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.PreOneHypercoverDenseData.p₁ CategoryTheory.Functor.PreOneHypercoverDenseData.p₂	—	CategoryTheory.Limits.Multiequalizer.condition CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
presheafObj_condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafObjπ CategoryTheory.Functor.PreOneHypercoverDenseData.Y CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.PreOneHypercoverDenseData.p₁ CategoryTheory.Functor.PreOneHypercoverDenseData.p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafObj_condition
presheafObj_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafObjπ	—	—	CategoryTheory.Limits.Multiequalizer.hom_ext
presheafObj_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafObjπ	—	presheafObj_hom_ext
presheafObj_mapPreimage_condition 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.PreOneHypercoverDenseData.f	presheafObj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Sheaf.cond CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem CategoryTheory.Functor.OneHypercoverDenseData.mem₁₀ CategoryTheory.Category.assoc CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac CategoryTheory.Functor.map_comp presheafObj_condition_assoc
presheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite presheaf presheafMap Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
presheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite presheaf presheafObj Opposite.unop	—	—
restriction_eq_of_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.PreOneHypercoverDenseData.f	restriction presheafObj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id restriction_map CategoryTheory.Category.id_comp
restriction_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.PreOneHypercoverDenseData.f CategoryTheory.Functor.map	presheafObj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val Opposite.op restriction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.Sheaf.cond CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.Presheaf.IsSheaf.amalgamate_map presheafObj_mapPreimage_condition CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction

Definitions

Name	Category	Theorems
res 📖	CompOp	1 math math: res_eq_res

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
res_eq_res 📖	mathematical	—	res	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Sheaf.cond CategoryTheory.GrothendieckTopology.intersection_covering CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem CategoryTheory.Functor.OneHypercoverDenseData.mem₁₀ CategoryTheory.Category.assoc CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition

CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff

Definitions

Name	Category	Theorems
isLimit 📖	CompOp	—
liftAux 📖	CompOp	3 math math: lift_map, lift_map_assoc, liftAux_fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y lift CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Limits.Multifork.IsLimit.hom_ext CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Functor.cover_lift CategoryTheory.Functor.IsDenseSubsite.instIsCocontinuous CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Functor.OneHypercoverDenseData.mem₀ CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem CategoryTheory.Category.assoc CategoryTheory.Sieve.downward_closed CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.Functor.map_comp lift_map_assoc CategoryTheory.op_comp liftAux_fac CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Limits.Multifork.condition
fac_assoc 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite.op lift CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
hom_ext 📖	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f	—	—	CategoryTheory.Limits.Multifork.IsLimit.hom_ext CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Functor.cover_lift CategoryTheory.Functor.IsDenseSubsite.instIsCocontinuous CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Category.assoc
liftAux_fac 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.map CategoryTheory.Functor.PreOneHypercoverDenseData.f	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index Opposite.op liftAux Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Presheaf.IsSheaf.amalgamate_map
lift_map 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData lift CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.PreOneHypercoverDenseData.f liftAux	—	CategoryTheory.Limits.Multifork.IsLimit.fac
lift_map_assoc 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite.op lift CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.PreOneHypercoverDenseData.f liftAux	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_map

CategoryTheory.Functor.PreOneHypercoverDenseData

Definitions

Name	Category	Theorems
I₀ 📖	CompOp	8 math math: multicospanShape_L, multicospanShape_fst, multicospanShape_snd, multicospanMap_app, toPreOneHypercover_I₀, multicospanIndex_right, multicospanIndex_fst, multicospanIndex_snd
I₁ 📖	CompOp	8 math math: toPreOneHypercover_I₁, multicospanShape_fst, multicospanShape_snd, multicospanMap_app, multicospanIndex_right, multicospanIndex_fst, multicospanIndex_snd, sieve₁₀_apply
I₁' 📖	CompOp	1 math math: multicospanShape_R
X 📖	CompOp	19 math math: w_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc, toPreOneHypercover_p₂, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc, w, multicospanMap_app, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition, toPreOneHypercover_X, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac_assoc, multicospanIndex_fst, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext_iff, multicospanIndex_left, multicospanIndex_snd, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π, sieve₁₀_apply, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc, toPreOneHypercover_p₁
Y 📖	CompOp	12 math math: w_assoc, toPreOneHypercover_p₂, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc, w, multicospanMap_app, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition, multicospanIndex_right, multicospanIndex_fst, multicospanIndex_snd, toPreOneHypercover_Y, sieve₁₀_apply, toPreOneHypercover_p₁
f 📖	CompOp	9 math math: w_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc, w, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac, toPreOneHypercover_f, CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc
multicospanIndex 📖	CompOp	7 math math: multicospanMap_app, multicospanMapIso_inv, multicospanIndex_right, multicospanIndex_fst, multicospanIndex_left, multicospanIndex_snd, multicospanMapIso_hom
multicospanMap 📖	CompOp	3 math math: multicospanMap_app, multicospanMapIso_inv, multicospanMapIso_hom
multicospanMapIso 📖	CompOp	2 math math: multicospanMapIso_inv, multicospanMapIso_hom
multicospanShape 📖	CompOp	11 math math: multicospanShape_L, multicospanShape_fst, multicospanShape_snd, multicospanMap_app, multicospanMapIso_inv, multicospanIndex_right, multicospanIndex_fst, multicospanIndex_left, multicospanIndex_snd, multicospanShape_R, multicospanMapIso_hom
p₁ 📖	CompOp	7 math math: w_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc, w, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition, multicospanIndex_fst, sieve₁₀_apply, toPreOneHypercover_p₁
p₂ 📖	CompOp	7 math math: w_assoc, toPreOneHypercover_p₂, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc, w, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition, multicospanIndex_snd, sieve₁₀_apply
sieve₁₀ 📖	CompOp	2 math math: CategoryTheory.Functor.OneHypercoverDenseData.mem₁₀, sieve₁₀_apply
toPreOneHypercover 📖	CompOp	10 math math: CategoryTheory.Functor.OneHypercoverDenseData.mem₁, toPreOneHypercover_p₂, toPreOneHypercover_I₁, toPreOneHypercover_I₀, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, toPreOneHypercover_X, toPreOneHypercover_f, CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover_toPreOneHypercover, toPreOneHypercover_Y, toPreOneHypercover_p₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multicospanIndex_fst 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.fst multicospanShape multicospanIndex CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op X CategoryTheory.Limits.MulticospanShape.fst Y I₀ I₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct p₁	—	—
multicospanIndex_left 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.left multicospanShape multicospanIndex CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op X	—	—
multicospanIndex_right 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.right multicospanShape multicospanIndex CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op Y I₀ I₁	—	—
multicospanIndex_snd 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.snd multicospanShape multicospanIndex CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op X CategoryTheory.Limits.MulticospanShape.snd Y I₀ I₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct p₂	—	—
multicospanMapIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Limits.WalkingMulticospan multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Functor.category CategoryTheory.Limits.MulticospanIndex.multicospan multicospanIndex multicospanMapIso multicospanMap Opposite CategoryTheory.Category.opposite	—	—
multicospanMapIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Limits.WalkingMulticospan multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Functor.category CategoryTheory.Limits.MulticospanIndex.multicospan multicospanIndex multicospanMapIso multicospanMap Opposite CategoryTheory.Category.opposite	—	—
multicospanMap_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMulticospan multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan multicospanIndex multicospanMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op X Y I₀ I₁	—	—
multicospanShape_L 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.L multicospanShape I₀	—	—
multicospanShape_R 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.R multicospanShape I₁'	—	—
multicospanShape_fst 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.fst multicospanShape I₀ I₁	—	—
multicospanShape_snd 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.snd multicospanShape I₀ I₁	—	—
sieve₁₀_apply 📖	mathematical	—	CategoryTheory.Sieve.arrows sieve₁₀ I₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Y X CategoryTheory.CategoryStruct.comp p₁ p₂	—	—
toPreOneHypercover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover I₀	—	—
toPreOneHypercover_I₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.I₁ toPreOneHypercover I₁	—	—
toPreOneHypercover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.Functor.obj X	—	—
toPreOneHypercover_Y 📖	mathematical	—	CategoryTheory.PreOneHypercover.Y toPreOneHypercover CategoryTheory.Functor.obj Y	—	—
toPreOneHypercover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover f	—	—
toPreOneHypercover_p₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.p₁ toPreOneHypercover CategoryTheory.Functor.map Y X p₁	—	—
toPreOneHypercover_p₂ 📖	mathematical	—	CategoryTheory.PreOneHypercover.p₂ toPreOneHypercover CategoryTheory.Functor.map Y X p₂	—	—
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Y X CategoryTheory.Functor.map p₁ f p₂	—	—
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Y X CategoryTheory.Functor.map p₁ f p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

---

← Back to Index