Grothendieck

📁 Source: Mathlib/CategoryTheory/Sites/Grothendieck.lean

Statistics

Metric	Count
Definitions Grothendieck, Z, base, g₁, g₂, map, Y, base, f, fromMiddle, fromMiddleHom, map, middle, precomp, precompRelation, toMiddle, toMiddleHom, fst, mk', r, snd, bind, bindToBase, index, instCoeFunForallForallHomProp, instCoeOutSieve, instInhabited, instOrderTop, instSemilatticeInf, multifork, pullback, pullbackComp, pullbackId, shape, toMultiequalizer, Covers, RightOreCondition, atomic, copy, dense, discrete, instCompleteLattice, instDFunLikeSetSieve, instInfSet, instInhabited, instLEGrothendieckTopology, instPartialOrder, instPreorderCover, pullback, pullbackComp, pullbackId, sieves, trivial, Grothendieck	54
Theorems ext, ext_iff, map_Z, map_g₁, map_g₂, w, w_assoc, base_Y, base_f, ext, ext_iff, from_middle_condition, hf, map_Y, map_f, middle_spec, precompRelation_Z, precompRelation_g₁, precompRelation_g₂, precomp_Y, precomp_f, to_middle_condition, ext, ext_iff, mk'_fst, mk'_r, mk'_snd, coe_pullback, condition, ext, ext_iff, index_fst, index_left, index_right, index_snd, shape_L, shape_R, shape_fst, shape_snd, arrow_intersect, arrow_max, arrow_stable, arrow_trans, bindOfArrows, bind_covering, bot_covering, bot_covers, coe_copy, copy_eq, covering_iff_covers_id, covering_of_eq_top, covers_iff, dense_covering, discrete_eq_top, ext, ext_iff, intersection_covering, intersection_covering_iff, isGLB_sInf, le_def, mem_sInf, mem_sieves_iff_coe, pullback_mem_iff_of_isIso, pullback_obj, pullback_stable, pullback_stable', right_ore_of_pullbacks, sieves_copy, superset_covering, top_covering, top_covers, top_mem, top_mem', transitive, transitive', trivial_covering, trivial_eq_bot	77
Total	131

CategoryTheory

Definitions

Name	Category	Theorems
Grothendieck 📖	CompData	118 math math: Grothendieck.base_eqToHom, Grothendieck.ιCompMap_hom_app_fiber, Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj, Grothendieck.map_comp_eq, CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, Grothendieck.pre_comp_map_assoc, Grothendieck.ιNatTrans_app_fiber, Grothendieck.grothendieckTypeToCat_inverse_map_base, Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe, Grothendieck.transportIso_hom_base, Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber, Grothendieck.grothendieckTypeToCatFunctor_obj_snd, Grothendieck.functor_comp_forget, Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, Grothendieck.isoMk_inv_base, Grothendieck.comp_base, Grothendieck.isoMk_inv_fiber, CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor, Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber, Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, Limits.fiberwiseColimitLimitIso_hom_app, CostructuredArrow.ιCompGrothendieckProj_inv_app, Grothendieck.id_fiber, Functor.hasColimit_map_comp_ι_comp_grothendieckProj, Functor.ι_colimitIsoColimitGrothendieck_hom, Limits.fiberwiseColim_obj, CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right, CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base, Grothendieck.ιNatTrans_app_base, Grothendieck.comp_fiber, Grothendieck.map_map, Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base, Grothendieck.ιCompMap_inv_app_fiber, Grothendieck.grothendieckTypeToCat_functor_obj_fst, Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base, CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, Grothendieck.fiber_eqToHom, Limits.preservesLimitsOfShape_colim_grothendieck, Grothendieck.eqToHom_eq, CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left, Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber, Grothendieck.grothendieckTypeToCat_inverse_obj_base, Functor.ι_colimitIsoColimitGrothendieck_hom_assoc, Grothendieck.grothendieckTypeToCatFunctor_map_coe, Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber, Grothendieck.pre_map_fiber, CostructuredArrow.mapCompιCompGrothendieckProj_inv_app, Grothendieck.map_id_eq, Grothendieck.forget_obj, instIsFilteredOrEmptyGrothendieckOfαCategoryObjCat, Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe, Grothendieck.compAsSmallFunctorEquivalence_functor, Grothendieck.id_base, CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso, Limits.fiberwiseColim_map_app, Limits.fiberwiseColimitLimitIso_inv_app, Grothendieck.pre_obj_base, CostructuredArrow.grothendieckProj_map, Grothendieck.grothendieckTypeToCatFunctor_obj_fst, Grothendieck.compAsSmallFunctorEquivalence_inverse, Grothendieck.pre_comp_map, Grothendieck.isoMk_hom_base, CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse, Grothendieck.map_obj_fiber, Grothendieck.final_map, Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base, Grothendieck.transportIso_inv_base, Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base, Grothendieck.ιCompMap_inv_app_base, Limits.fiberwiseColimCompEvaluationIso_hom_app, Grothendieck.pre_comp, Grothendieck.functorFrom_obj, Grothendieck.transportIso_inv_fiber, Grothendieck.map_obj, Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base, Limits.fiberwiseColimCompColimIso_hom_app, CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso, CostructuredArrow.grothendieckProj_obj, Grothendieck.map_obj_base, Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, Grothendieck.final_pre, Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, Grothendieck.compAsSmallFunctorEquivalence_unitIso, Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as, Limits.fiberwiseColimCompColimIso_inv_app, CostructuredArrow.mapCompιCompGrothendieckProj_hom_app, Limits.fiberwiseColimCompEvaluationIso_inv_app, Grothendieck.functorFrom_map, Limits.hasColimitsOfShape_grothendieck, CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, Grothendieck.map_map_fiber, Grothendieck.map_map_base, Grothendieck.ι_obj, CostructuredArrow.grothendieckPrecompFunctorToComma_map_right, Grothendieck.ιCompMap_hom_app_base, Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base, Grothendieck.pre_obj_fiber, Grothendieck.grothendieckTypeToCatInverse_obj_base, CostructuredArrow.ιCompGrothendieckProj_hom_app, Grothendieck.pre_id, Grothendieck.grothendieckTypeToCatInverse_map_base, Grothendieck.grothendieckTypeToCat_functor_map_coe, instIsFilteredGrothendieckOfαCategoryObjCat, Grothendieck.isoMk_hom_fiber, Grothendieck.grothendieckTypeToCat_functor_obj_snd, CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base, Grothendieck.compAsSmallFunctorEquivalence_counitIso, Functor.ι_colimitIsoColimitGrothendieck_inv, Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as, Grothendieck.forget_map, Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom, Grothendieck.transportIso_hom_fiber, Grothendieck.pre_map_base, Grothendieck.ι_map, Grothendieck.faithful_ι

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
Covers 📖	MathDef	7 math math: bot_covers, close_apply, arrow_max, covering_iff_covers_id, covers_iff_mem_of_isClosed, top_covers, covers_iff
RightOreCondition 📖	MathDef	1 math math: right_ore_of_pullbacks
atomic 📖	CompOp	—
copy 📖	CompOp	3 math math: sieves_copy, coe_copy, copy_eq
dense 📖	CompOp	1 math math: dense_covering
discrete 📖	CompOp	1 math math: discrete_eq_top
instCompleteLattice 📖	CompOp	14 math math: CategoryTheory.sheafBotEquivalence_functor, CategoryTheory.Presieve.isSheaf_bot, bot_covers, CategoryTheory.sheafBotEquivalence_inverse_map_val, discrete_eq_top, CategoryTheory.sheafBotEquivalence_unitIso, CategoryTheory.sheafBotEquivalence_inverse_obj_val, trivial_eq_bot, bot_covering, CategoryTheory.Presheaf.isSheaf_bot, CategoryTheory.Pretopology.toGrothendieck_bot, top_covers, CategoryTheory.sheafBotEquivalence_counitIso, top_covering
instDFunLikeSetSieve 📖	CompOp	89 math math: AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, mem_toPretopology, ext_iff, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, OneHypercover.mem₀, CategoryTheory.Functor.OneHypercoverDenseData.mem₁, CategoryTheory.Functor.functorPushforward_imageSieve_mem, CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan, CategoryTheory.Functor.functorPushforward_mem_iff, trivial_covering, intersection_covering_iff, AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, CategoryTheory.Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp, OneHypercover.mem_sieve₁', CategoryTheory.Pretopology.mem_toGrothendieck, Cover.preOneHypercover_sieve₀, CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset, top_mem, CategoryTheory.Functor.IsLocallyFull.functorPushforward_imageSieve_mem, CategoryTheory.Functor.OneHypercoverDenseData.mem₁₀, CategoryTheory.Functor.is_cover_of_isCoverDense, mem_over_iff, CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi, coversTop_iff_of_isTerminal, CategoryTheory.Functor.functorPushforward_equalizer_mem, CategoryTheory.Functor.IsDenseSubsite.equalizer_mem, OneHypercoverFamily.IsSheafIff.fac, close_eq_top_iff_mem, coe_copy, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, le_def, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, Cover.Arrow.hf, CategoryTheory.Precoverage.mem_toGrothendieck_iff, mem_sInf, OneHypercover.IsPreservedBy.mem₁, CategoryTheory.generate_discretePresieve_mem, CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_mem, CategoryTheory.Functor.pushforward_cover_iff_cover_pullback, CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff, CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, CategoryTheory.Presheaf.IsLocallyInjective.equalizerSieve_mem, Cover.condition, CategoryTheory.Functor.inducedTopology_sieves, CategoryTheory.ofGrothendieck_iff, dense_covering, OneHypercover.IsPreservedBy.mem₀, CategoryTheory.Functor.OneHypercoverDenseData.sieve_mem, OneHypercoverFamily.IsSheafIff.fac', CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.Functor.IsLocallyFaithful.functorPushforward_equalizer_mem, OneHypercoverFamily.IsSheafIff.fac'_assoc, bot_covering, mem_sieves_iff_coe, CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem, CategoryTheory.Coverage.mem_toGrothendieck, CategoryTheory.Presheaf.equalizerSieve_mem, CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily, Cover.ext_iff, mem_toPrecoverage_iff, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, pullback_mem_iff_of_isIso, covering_iff_covers_id, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, CategoryTheory.Functor.IsCoverDense.is_cover, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi, Cover.Arrow.to_middle_condition, CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced, AlgebraicGeometry.Scheme.grothendieckTopology_cover, CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, covers_iff, CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering, Cover.Arrow.from_middle_condition, CategoryTheory.Functor.mem_inducedTopology_sieves_iff, CategoryTheory.Pretopology.mem_ofGrothendieck, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, mem_toCoverage_iff, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem, CategoryTheory.Presheaf.imageSieve_mem, Cover.coe_pullback, CategoryTheory.discreteSieve_mem, covering_of_eq_top, OneHypercover.mem₁, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, top_covering
instInfSet 📖	CompOp	5 math math: CategoryTheory.Coverage.toGrothendieck_eq_sInf, mem_sInf, isGLB_sInf, CategoryTheory.Precoverage.toGrothendieck_eq_sInf, CategoryTheory.Pretopology.sInf_ofGrothendieck
instInhabited 📖	CompOp	—
instLEGrothendieckTopology 📖	CompOp	12 math math: CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage, AlgebraicGeometry.Scheme.zariskiTopology_le_etaleTopology, CategoryTheory.Pretopology.toGrothendieck_mono, CategoryTheory.Precoverage.toGrothendieck_mono, CategoryTheory.le_topology_of_closedSieves_isSheaf, AlgebraicGeometry.Scheme.grothendieckTopology_le_grothendieckTopology, le_def, AlgebraicGeometry.Scheme.grothendieckTopology_monotone, isGLB_sInf, CategoryTheory.Sheaf.le_finestTopology, Subcanonical.le_canonical, le_canonical
instPartialOrder 📖	CompOp	—
instPreorderCover 📖	CompOp	47 math math: coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, liftToDiagramLimitObjAux_fac, diagram_obj, liftToDiagramLimitObjAux_fac_assoc, Opens.mayerVietorisSquare_X₃, CondensedMod.isDiscrete_tfae, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, preservesLimitsOfShape_diagramFunctor, diagramCompIso_hom_ι, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, CategoryTheory.Meq.pullback_refine, diagramCompIso_hom_ι_assoc, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, Opens.mayerVietorisSquare_X₂, Opens.coe_mayerVietorisSquare_X₁, diagram_map, diagramPullback_app, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CondensedSet.isDiscrete_tfae, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, diagramFunctor_map, diagramFunctor_obj, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, CategoryTheory.Presheaf.isLocallySurjective_toPlus, diagramNatTrans_app, preservesLimits_diagramFunctor, coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app, CategoryTheory.Meq.refine_apply, Opens.mayerVietorisSquare'_toSquare, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, diagramNatTrans_id, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, diagramNatTrans_zero, preservesLimit_diagramFunctor, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, pullback_obj, diagramNatTrans_comp, Condensed.instAB4CondensedMod, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, CategoryTheory.Meq.pullback_apply
pullback 📖	CompOp	5 math math: CategoryTheory.Meq.pullback_refine, Plus.res_mk_eq_mk_pullback, diagramPullback_app, pullback_obj, CategoryTheory.Meq.pullback_apply
pullbackComp 📖	CompOp	—
pullbackId 📖	CompOp	—
sieves 📖	CompOp	4 math math: CategoryTheory.topologyOfClosureOperator_sieves, CategoryTheory.Functor.inducedTopology_sieves, mem_sieves_iff_coe, top_mem'
trivial 📖	CompOp	2 math math: trivial_covering, trivial_eq_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrow_intersect 📖	mathematical	Covers	CategoryTheory.Sieve SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice	—	CategoryTheory.Sieve.pullback_inter
arrow_max 📖	mathematical	CategoryTheory.Sieve.arrows	Covers	—	Covers.eq_1 CategoryTheory.Sieve.mem_iff_pullback_eq_top top_mem
arrow_stable 📖	mathematical	Covers	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	covers_iff CategoryTheory.Sieve.pullback_comp
arrow_trans 📖	—	Covers	—	—	transitive CategoryTheory.Sieve.pullback_comp
bindOfArrows 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.Sieve.generate	CategoryTheory.Presieve.bindOfArrows	—	superset_covering CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows bind_covering pullback_stable
bind_covering 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	CategoryTheory.Sieve.bind CategoryTheory.Sieve.arrows	—	transitive superset_covering CategoryTheory.Sieve.le_pullback_bind
bot_covering 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Top.top OrderTop.toTop CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop	—	trivial_covering
bot_covers 📖	mathematical	—	Covers Bot.bot CategoryTheory.GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Sieve.arrows	—	covers_iff bot_covering CategoryTheory.Sieve.mem_iff_pullback_eq_top
coe_copy 📖	mathematical	sieves	DFunLike.coe CategoryTheory.GrothendieckTopology Set CategoryTheory.Sieve instDFunLikeSetSieve copy	—	—
copy_eq 📖	mathematical	sieves	copy	—	ext
covering_iff_covers_id 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve Covers CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Sieve.pullback_id
covering_of_eq_top 📖	mathematical	Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	—	top_mem
covers_iff 📖	mathematical	—	Covers CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.pullback	—	—
dense_covering 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve dense CategoryTheory.Sieve.arrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
discrete_eq_top 📖	mathematical	—	discrete Top.top CategoryTheory.GrothendieckTopology OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
ext 📖	—	DFunLike.coe CategoryTheory.GrothendieckTopology Set CategoryTheory.Sieve instDFunLikeSetSieve	—	—	DFunLike.coe_injective
ext_iff 📖	mathematical	—	DFunLike.coe CategoryTheory.GrothendieckTopology Set CategoryTheory.Sieve instDFunLikeSetSieve	—	ext
intersection_covering 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice	—	transitive CategoryTheory.Sieve.pullback_inter CategoryTheory.Sieve.pullback_eq_top_of_mem inf_of_le_right
intersection_covering_iff 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice	—	superset_covering inf_le_left inf_le_right intersection_covering
isGLB_sInf 📖	mathematical	—	IsGLB CategoryTheory.GrothendieckTopology instLEGrothendieckTopology InfSet.sInf instInfSet	—	IsGLB.of_image isGLB_sInf
le_def 📖	mathematical	—	CategoryTheory.GrothendieckTopology instLEGrothendieckTopology Pi.hasLe Set CategoryTheory.Sieve Set.instLE DFunLike.coe instDFunLikeSetSieve	—	—
mem_sInf 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve InfSet.sInf instInfSet	—	Set.iInter_coe_set Set.iInter_congr_Prop Set.iInter_exists Set.biInter_and' Set.iInter_iInter_eq_right
mem_sieves_iff_coe 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership sieves DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	—	—
pullback_mem_iff_of_isIso 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.pullback	—	CategoryTheory.Sieve.pullback_comp CategoryTheory.IsIso.inv_hom_id CategoryTheory.Sieve.pullback_id pullback_stable
pullback_obj 📖	mathematical	—	CategoryTheory.Functor.obj Cover Preorder.smallCategory instPreorderCover pullback Cover.pullback	—	—
pullback_stable 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	CategoryTheory.Sieve.pullback	—	pullback_stable'
pullback_stable' 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership sieves	CategoryTheory.Sieve.pullback	—	—
right_ore_of_pullbacks 📖	mathematical	—	RightOreCondition	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.pullback.condition
sieves_copy 📖	mathematical	sieves	copy	—	—
superset_covering 📖	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	—	—	transitive covering_of_eq_top top_le_iff CategoryTheory.Sieve.pullback_eq_top_of_mem CategoryTheory.Sieve.pullback_monotone
top_covering 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
top_covers 📖	mathematical	—	Covers Top.top CategoryTheory.GrothendieckTopology OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
top_mem 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_mem'
top_mem' 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership sieves Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
transitive 📖	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve CategoryTheory.Sieve.pullback	—	—	transitive'
transitive' 📖	—	CategoryTheory.Sieve Set Set.instMembership sieves CategoryTheory.Sieve.pullback	—	—	—
trivial_covering 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve trivial Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.mem_singleton_iff
trivial_eq_bot 📖	mathematical	—	trivial Bot.bot CategoryTheory.GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—

CategoryTheory.GrothendieckTopology.Cover

Definitions

Name	Category	Theorems
bind 📖	CompOp	2 math math: Arrow.to_middle_condition, Arrow.middle_spec
bindToBase 📖	CompOp	—
index 📖	CompOp	49 math math: index_left, index_fst, CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map', Opens.mayerVietorisSquare_X₃, CondensedMod.isDiscrete_tfae, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac, CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc, multicospanComp_inv_app, CategoryTheory.RanIsSheafOfIsCocontinuous.fac', Opens.mayerVietorisSquare_X₂, Opens.coe_mayerVietorisSquare_X₁, CategoryTheory.Presheaf.isSheaf_iff_multifork, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, multicospanComp_hom_app, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac_assoc, CondensedSet.isDiscrete_tfae, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, CategoryTheory.Presheaf.isLocallySurjective_toPlus, CategoryTheory.RanIsSheafOfIsCocontinuous.fac, index_right, Opens.mayerVietorisSquare'_toSquare, index_snd, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.Meq.equiv_symm_eq_apply, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map, CategoryTheory.Meq.equiv_apply, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map, Condensed.instAB4CondensedMod, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac
instCoeFunForallForallHomProp 📖	CompOp	—
instCoeOutSieve 📖	CompOp	—
instInhabited 📖	CompOp	11 math math: CondensedMod.isDiscrete_tfae, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.instAB4CondensedMod, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat
instOrderTop 📖	CompOp	1 math math: CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk
instSemilatticeInf 📖	CompOp	11 math math: CondensedMod.isDiscrete_tfae, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.instAB4CondensedMod, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat
multifork 📖	CompOp	1 math math: CategoryTheory.Presheaf.isSheaf_iff_multifork
pullback 📖	CompOp	4 math math: Arrow.base_Y, Arrow.base_f, CategoryTheory.GrothendieckTopology.pullback_obj, coe_pullback
pullbackComp 📖	CompOp	—
pullbackId 📖	CompOp	—
shape 📖	CompOp	52 math math: index_left, index_fst, CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map', Opens.mayerVietorisSquare_X₃, shape_snd, CondensedMod.isDiscrete_tfae, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, shape_fst, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac, CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc, multicospanComp_inv_app, CategoryTheory.RanIsSheafOfIsCocontinuous.fac', Opens.mayerVietorisSquare_X₂, Opens.coe_mayerVietorisSquare_X₁, CategoryTheory.Presheaf.isSheaf_iff_multifork, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, multicospanComp_hom_app, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac_assoc, CondensedSet.isDiscrete_tfae, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, CategoryTheory.Presheaf.isLocallySurjective_toPlus, CategoryTheory.RanIsSheafOfIsCocontinuous.fac, index_right, Opens.mayerVietorisSquare'_toSquare, index_snd, Opens.coe_mayerVietorisSquare_X₄, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map, CategoryTheory.Meq.condition, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map, Condensed.instAB4CondensedMod, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, shape_L, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac, shape_R, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac
toMultiequalizer 📖	CompOp	1 math math: CategoryTheory.Presheaf.isSheaf_iff_multiequalizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pullback 📖	mathematical	—	CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
condition 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	—	—
ext 📖	—	CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	—	—	CategoryTheory.Sieve.ext
ext_iff 📖	mathematical	—	CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	—	ext
index_fst 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.fst shape index CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op Arrow.Y CategoryTheory.Limits.MulticospanShape.fst Arrow.Relation.Z Relation.fst Relation.snd Relation.r Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Arrow.Relation.g₁	—	—
index_left 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.left shape index CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op Arrow.Y	—	—
index_right 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.right shape index CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op Arrow.Relation.Z Relation.fst Relation.snd Relation.r	—	—
index_snd 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.snd shape index CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op Arrow.Y CategoryTheory.Limits.MulticospanShape.snd Arrow.Relation.Z Relation.fst Relation.snd Relation.r Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Arrow.Relation.g₂	—	—
shape_L 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.L shape Arrow	—	—
shape_R 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.R shape Relation	—	—
shape_fst 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.fst shape Relation.fst	—	—
shape_snd 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.snd shape Relation.snd	—	—

CategoryTheory.GrothendieckTopology.Cover.Arrow

Definitions

Name	Category	Theorems
Y 📖	CompOp	34 math math: CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, CategoryTheory.GrothendieckTopology.Cover.index_left, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac, CategoryTheory.GrothendieckTopology.Cover.index_fst, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc, precompRelation_Z, ext_iff, base_Y, map_Y, Relation.ext_iff, CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app, hf, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac_assoc, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X, CategoryTheory.GrothendieckTopology.diagramNatTrans_app, CategoryTheory.Meq.mk_apply, CategoryTheory.RanIsSheafOfIsCocontinuous.fac, CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app, precomp_f, CategoryTheory.Meq.refine_apply, CategoryTheory.GrothendieckTopology.Cover.index_snd, to_middle_condition, base_f, precomp_Y, precompRelation_g₁, CategoryTheory.Meq.condition, CategoryTheory.GrothendieckTopology.Plus.toPlus_apply, middle_spec, Relation.w, CategoryTheory.Meq.pullback_apply, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac, Relation.w_assoc
base 📖	CompOp	3 math math: base_Y, CategoryTheory.GrothendieckTopology.diagramPullback_app, base_f
f 📖	CompOp	19 math math: CategoryTheory.Presheaf.IsSheaf.amalgamate_map, ext_iff, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f, map_f, CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc, hf, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac_assoc, CategoryTheory.Presheaf.IsSheaf.amalgamate_map_assoc, CategoryTheory.Meq.mk_apply, CategoryTheory.RanIsSheafOfIsCocontinuous.fac, precomp_f, CategoryTheory.Meq.refine_apply, base_f, CategoryTheory.GrothendieckTopology.Plus.toPlus_apply, middle_spec, Relation.w, CategoryTheory.Meq.pullback_apply, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac, Relation.w_assoc
fromMiddle 📖	CompOp	1 math math: to_middle_condition
fromMiddleHom 📖	CompOp	2 math math: from_middle_condition, middle_spec
map 📖	CompOp	6 math math: map_Y, map_f, Relation.map_g₁, CategoryTheory.GrothendieckTopology.diagram_map, Relation.map_g₂, Relation.map_Z
middle 📖	CompOp	2 math math: from_middle_condition, middle_spec
precomp 📖	CompOp	5 math math: precompRelation_Z, precomp_f, precompRelation_g₂, precomp_Y, precompRelation_g₁
precompRelation 📖	CompOp	3 math math: precompRelation_Z, precompRelation_g₂, precompRelation_g₁
toMiddle 📖	CompOp	—
toMiddleHom 📖	CompOp	2 math math: to_middle_condition, middle_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_Y 📖	mathematical	—	Y base CategoryTheory.GrothendieckTopology.Cover.pullback	—	—
base_f 📖	mathematical	—	f base CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y CategoryTheory.GrothendieckTopology.Cover.pullback	—	—
ext 📖	—	Y Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct f	—	—	—
ext_iff 📖	mathematical	—	Y Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct f	—	ext
from_middle_condition 📖	mathematical	—	CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve middle fromMiddleHom	—	hf
hf 📖	mathematical	—	CategoryTheory.Sieve.arrows CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve Y f	—	—
map_Y 📖	mathematical	—	Y map	—	—
map_f 📖	mathematical	—	f map	—	—
middle_spec 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y CategoryTheory.GrothendieckTopology.Cover.bind middle toMiddleHom fromMiddleHom f	—	hf
precompRelation_Z 📖	mathematical	—	Relation.Z precomp precompRelation Y	—	—
precompRelation_g₁ 📖	mathematical	—	Relation.g₁ precomp precompRelation CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Y	—	—
precompRelation_g₂ 📖	mathematical	—	Relation.g₂ precomp precompRelation	—	—
precomp_Y 📖	mathematical	—	Y precomp	—	—
precomp_f 📖	mathematical	—	f precomp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y	—	—
to_middle_condition 📖	mathematical	—	CategoryTheory.Sieve.arrows Y fromMiddle CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.GrothendieckTopology.Cover.bind toMiddleHom	—	hf

CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation

Definitions

Name	Category	Theorems
Z 📖	CompOp	12 math math: CategoryTheory.GrothendieckTopology.Cover.index_fst, CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_Z, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_Y, ext_iff, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app, CategoryTheory.GrothendieckTopology.Cover.index_right, CategoryTheory.GrothendieckTopology.Cover.index_snd, map_Z, CategoryTheory.Meq.condition, w, w_assoc
base 📖	CompOp	—
g₁ 📖	CompOp	8 math math: CategoryTheory.GrothendieckTopology.Cover.index_fst, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁, ext_iff, map_g₁, CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_g₁, CategoryTheory.Meq.condition, w, w_assoc
g₂ 📖	CompOp	8 math math: CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂, ext_iff, map_g₂, CategoryTheory.GrothendieckTopology.Cover.index_snd, CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_g₂, CategoryTheory.Meq.condition, w, w_assoc
map 📖	CompOp	3 math math: map_g₁, map_g₂, map_Z

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	Z Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Cover.Arrow.Y g₁ g₂	—	—	—
ext_iff 📖	mathematical	—	Z Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Cover.Arrow.Y g₁ g₂	—	ext
map_Z 📖	mathematical	—	Z CategoryTheory.GrothendieckTopology.Cover.Arrow.map map	—	—
map_g₁ 📖	mathematical	—	g₁ CategoryTheory.GrothendieckTopology.Cover.Arrow.map map	—	—
map_g₂ 📖	mathematical	—	g₂ CategoryTheory.GrothendieckTopology.Cover.Arrow.map map	—	—
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Z CategoryTheory.GrothendieckTopology.Cover.Arrow.Y g₁ CategoryTheory.GrothendieckTopology.Cover.Arrow.f g₂	—	—
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Z CategoryTheory.GrothendieckTopology.Cover.Arrow.Y g₁ CategoryTheory.GrothendieckTopology.Cover.Arrow.f g₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

CategoryTheory.GrothendieckTopology.Cover.Relation

Definitions

Name	Category	Theorems
fst 📖	CompOp	9 math math: CategoryTheory.GrothendieckTopology.Cover.index_fst, CategoryTheory.GrothendieckTopology.Cover.shape_fst, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app, ext_iff, CategoryTheory.GrothendieckTopology.Cover.index_right, CategoryTheory.GrothendieckTopology.Cover.index_snd, CategoryTheory.Meq.condition, mk'_fst
mk' 📖	CompOp	3 math math: mk'_snd, mk'_r, mk'_fst
r 📖	CompOp	8 math math: CategoryTheory.GrothendieckTopology.Cover.index_fst, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app, mk'_r, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app, ext_iff, CategoryTheory.GrothendieckTopology.Cover.index_right, CategoryTheory.GrothendieckTopology.Cover.index_snd, CategoryTheory.Meq.condition
snd 📖	CompOp	9 math math: CategoryTheory.GrothendieckTopology.Cover.index_fst, CategoryTheory.GrothendieckTopology.Cover.shape_snd, mk'_snd, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app, CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app, ext_iff, CategoryTheory.GrothendieckTopology.Cover.index_right, CategoryTheory.GrothendieckTopology.Cover.index_snd, CategoryTheory.Meq.condition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	fst snd CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation r	—	—	—
ext_iff 📖	mathematical	—	fst snd CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation r	—	ext
mk'_fst 📖	mathematical	—	fst mk'	—	—
mk'_r 📖	mathematical	—	r mk'	—	—
mk'_snd 📖	mathematical	—	snd mk'	—	—

CategoryTheory.Pseudofunctor

Definitions

Name	Category	Theorems
Grothendieck 📖	CompData	15 math math: Grothendieck.map_id_eq, Grothendieck.map_id_map, Grothendieck.categoryStruct_id_fiber, Grothendieck.map_obj_fiber, Grothendieck.forget_map, Grothendieck.map_comp_forget, Grothendieck.categoryStruct_id_base, Grothendieck.Hom.congr, Grothendieck.map_comp_eq, Grothendieck.map_map_fiber, Grothendieck.categoryStruct_comp_base, Grothendieck.forget_obj, Grothendieck.map_obj_base, Grothendieck.categoryStruct_comp_fiber, Grothendieck.map_map_base

---

← Back to Index