OneHypercoverDense

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

Statistics

Metric	Count
Definitions IsOneHypercoverDense, OneHypercoverDenseData, SieveStruct, i₀, q, compPresheafIso, presheaf, presheafMap, presheafObj, presheafObjIsLimit, presheafObjMultifork, presheafObjObjIso, hom, inv, presheafObjπ, restriction, res, sheaf, sheafIso, isLimit, liftAux, sieve, toOneHypercover, toPreOneHypercoverDenseData, PreOneHypercoverDenseData, I₀, I₁, I₁', X, Y, f, multicospanIndex, multicospanMap, multicospanMapIso, multicospanShape, p₁, p₂, sieve₁₀, toPreOneHypercover, oneHypercoverDenseData	40
Theorems nonempty_oneHypercoverDenseData, of_hasPullbacks, fac, fac_assoc, essSurj, isSheaf, presheafMap_comp, presheafMap_comp_assoc, presheafMap_id, presheafMap_presheafObjObjIso_hom, presheafMap_presheafObjObjIso_hom_assoc, presheafMap_restriction, presheafMap_restriction_assoc, presheafMap_π, presheafMap_π_assoc, hom_map, hom_mapPreimage, hom_mapPreimage_assoc, hom_map_assoc, inv_restriction, inv_restriction_assoc, inv_π, inv_π_assoc, presheafObjObjIso_inv_naturality, presheafObjObjIso_inv_naturality_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, isEquivalence, 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, isEquivalence_of_isOneHypercoverDense	72
Total	112

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₀
isEquivalence_of_isOneHypercoverDense 📖	mathematical	—	IsEquivalence CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite category CategoryTheory.Presheaf.IsSheaf sheafPushforwardContinuous IsDenseSubsite.instIsContinuous	—	OneHypercoverDenseData.isEquivalence

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	25 math math: mem₁, essSurj.presheafMap_π_assoc, essSurj.presheafObjObjIso.inv_π, essSurj.presheafObj_mapPreimage_condition, essSurj.presheafObjObjIso.inv_π_assoc, essSurj.presheafObjObjIso.hom_map_assoc, mem₁₀, essSurj.presheafObj_condition_assoc, essSurj.presheafObjObjIso.hom_mapPreimage, essSurj.presheafMap_presheafObjObjIso_hom, essSurj.presheafObjObjIso.hom_mapPreimage_assoc, essSurj.presheafMap_presheafObjObjIso_hom_assoc, SieveStruct.fac, mem₀, essSurj.presheafObj_condition, SieveStruct.fac_assoc, essSurj.presheafObj_hom_ext_iff, essSurj.presheafMap_π, toOneHypercover_toPreOneHypercover, essSurj.presheafObjObjIso.hom_map, essSurj.restriction_map, essSurj.restriction_eq_of_fac, isSheaf_iff.lift_map, isSheaf_iff.lift_map_assoc, isSheaf_iff.liftAux_fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essSurj 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Functor.IsDenseSubsite.instIsContinuous	—	CategoryTheory.Functor.IsDenseSubsite.instIsContinuous
isEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Functor.IsDenseSubsite.instIsContinuous	—	CategoryTheory.Functor.IsDenseSubsite.instIsContinuous CategoryTheory.Functor.IsDenseSubsite.faithful_sheafPushforwardContinuous CategoryTheory.Functor.IsDenseSubsite.full_sheafPushforwardContinuous essSurj
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 toPreOneHypercoverDenseData	—	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₁₀ toPreOneHypercoverDenseData	—	—
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
compPresheafIso 📖	CompOp	—
presheaf 📖	CompOp	15 math math: presheaf_obj, presheafObjObjIso.inv_π, presheafObjObjIso.inv_π_assoc, presheafObjObjIso.hom_map_assoc, presheafObjObjIso_inv_naturality, presheafObjObjIso.hom_mapPreimage, isSheaf, presheafMap_presheafObjObjIso_hom, presheaf_map, presheafObjObjIso.hom_mapPreimage_assoc, presheafMap_presheafObjObjIso_hom_assoc, presheafObjObjIso.inv_restriction, presheafObjObjIso_inv_naturality_assoc, presheafObjObjIso.hom_map, presheafObjObjIso.inv_restriction_assoc
presheafMap 📖	CompOp	12 math math: presheafMap_π_assoc, presheafMap_restriction_assoc, presheafMap_comp, presheafObjObjIso_inv_naturality, presheafMap_comp_assoc, presheafMap_presheafObjObjIso_hom, presheaf_map, presheafMap_id, presheafMap_presheafObjObjIso_hom_assoc, presheafMap_restriction, presheafObjObjIso_inv_naturality_assoc, presheafMap_π
presheafObj 📖	CompOp	21 math math: presheaf_obj, presheafMap_π_assoc, presheafObj_mapPreimage_condition, presheafMap_restriction_assoc, presheafObjObjIso.hom_map_assoc, presheafMap_comp, presheafObj_condition_assoc, presheafObjObjIso_inv_naturality, presheafObjObjIso.hom_mapPreimage, presheafMap_comp_assoc, presheafMap_presheafObjObjIso_hom, presheafMap_id, presheafObjObjIso.hom_mapPreimage_assoc, presheafMap_presheafObjObjIso_hom_assoc, presheafObj_condition, presheafMap_restriction, presheafObj_hom_ext_iff, presheafMap_π, presheafObjObjIso.hom_map, restriction_map, restriction_eq_of_fac
presheafObjIsLimit 📖	CompOp	—
presheafObjMultifork 📖	CompOp	—
presheafObjObjIso 📖	CompOp	4 math math: presheafObjObjIso_inv_naturality, presheafMap_presheafObjObjIso_hom, presheafMap_presheafObjObjIso_hom_assoc, presheafObjObjIso_inv_naturality_assoc
presheafObjπ 📖	CompOp	16 math math: presheafMap_π_assoc, presheafObjObjIso.inv_π, presheafObj_mapPreimage_condition, presheafObjObjIso.inv_π_assoc, presheafObjObjIso.hom_map_assoc, presheafObj_condition_assoc, presheafObjObjIso.hom_mapPreimage, presheafMap_presheafObjObjIso_hom, presheafObjObjIso.hom_mapPreimage_assoc, presheafMap_presheafObjObjIso_hom_assoc, presheafObj_condition, presheafObj_hom_ext_iff, presheafMap_π, presheafObjObjIso.hom_map, restriction_map, restriction_eq_of_fac
restriction 📖	CompOp	8 math math: presheafMap_π_assoc, presheafMap_restriction_assoc, presheafMap_restriction, presheafObjObjIso.inv_restriction, presheafMap_π, restriction_map, restriction_eq_of_fac, presheafObjObjIso.inv_restriction_assoc
sheaf 📖	CompOp	—
sheafIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf presheaf	—	CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff CategoryTheory.Presheaf.isSheaf_of_iso_iff CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.NatTrans.naturality presheafMap_presheafObjObjIso_hom CategoryTheory.Category.id_comp
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_presheafObjObjIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op presheafMap CategoryTheory.Functor.PreOneHypercoverDenseData.f CategoryTheory.Iso.hom presheaf presheafObjObjIso presheafObjπ	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id presheafObj_hom_ext presheafMap_π presheafObjObjIso.eq_1 presheafObjObjIso.inv_π restriction_eq_of_fac
presheafMap_presheafObjObjIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafMap CategoryTheory.Functor.PreOneHypercoverDenseData.f Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Iso.hom presheaf presheafObjObjIso presheafObjπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafMap_presheafObjObjIso_hom
presheafMap_restriction 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op presheafMap restriction	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.ObjectProperty.FullSubcategory.property 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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_π
presheafObjObjIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op presheaf CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv presheafObjObjIso presheafObj presheafMap Opposite.unop	—	presheafObj_hom_ext CategoryTheory.Category.assoc presheafObjObjIso.inv_π presheafMap_π presheafObjObjIso.inv_restriction CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map
presheafObjObjIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver presheaf CategoryTheory.Iso.inv presheafObjObjIso presheafMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafObjObjIso_inv_naturality
presheafObj_condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.ObjectProperty.FullSubcategory.property 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 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData 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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct presheafObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op restriction CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Presheaf.IsSheaf.amalgamate_map presheafObj_mapPreimage_condition CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac

CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso

Definitions

Name	Category	Theorems
hom 📖	CompOp	4 math math: hom_map_assoc, hom_mapPreimage, hom_mapPreimage_assoc, hom_map
inv 📖	CompOp	4 math math: inv_π, inv_π_assoc, inv_restriction, inv_restriction_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf Opposite.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Presheaf.IsSheaf.amalgamate_map CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition CategoryTheory.Sieve.ofArrows.fac
hom_mapPreimage 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.PreOneHypercoverDenseData.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf Opposite.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf hom CategoryTheory.Functor.IsDenseSubsite.mapPreimage CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem CategoryTheory.Category.assoc CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map CategoryTheory.Functor.IsDenseSubsite.mapPreimage.congr_simp CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map hom_map
hom_mapPreimage_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.PreOneHypercoverDenseData.f	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf Opposite.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf hom CategoryTheory.Functor.IsDenseSubsite.mapPreimage CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_mapPreimage
hom_map_assoc 📖	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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf Opposite.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_map
inv_restriction 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf inv CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction Opposite.unop CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Functor.cover_lift CategoryTheory.Functor.IsDenseSubsite.instIsCocontinuous CategoryTheory.Functor.OneHypercoverDenseData.mem₀ CategoryTheory.Category.assoc CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_comp_assoc inv_π_assoc CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map
inv_restriction_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf inv CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction CategoryTheory.Functor.IsDenseSubsite.mapPreimage	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_restriction
inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData inv CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage CategoryTheory.Functor.PreOneHypercoverDenseData.f	—	CategoryTheory.Limits.Multiequalizer.lift_ι
inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf Opposite.op CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf inv CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ CategoryTheory.Functor.IsDenseSubsite.mapPreimage CategoryTheory.Functor.PreOneHypercoverDenseData.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_π

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.ObjectProperty.FullSubcategory.property 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 CategoryTheory.Category.opposite 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 CategoryTheory.Category.opposite 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.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 CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.PreOneHypercoverDenseData.X CategoryTheory.Functor.OneHypercoverDenseData.toPreOneHypercoverDenseData liftAux CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Multifork.ι CategoryTheory.Functor.PreOneHypercoverDenseData.f	—	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 CategoryTheory.Category.opposite 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 CategoryTheory.Category.opposite 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	31 math math: w_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π, toPreOneHypercover_p₂, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_map_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_mapPreimage, w, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_mapPreimage_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom_assoc, 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.essSurj.presheafObjObjIso.hom_map, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac, 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	14 math math: w_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π_assoc, w, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom_assoc, 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, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac
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