Sheaf

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

Statistics

Metric	Count
Definitions IsSeparated, IsSheaf', amalgamate, amalgamateOfArrows, isLimitMultifork, conesEquivSieveCompatibleFamily, firstMap, firstObj, forkMap, homEquivAmalgamation, isLimitOfIsSheaf, isSheafForIsSheafFor', secondMap, secondObj, cone, Sheaf, mk, homEquiv, isTerminalOfBotCover, isTerminalOfEqTop, isTerminalTerminal, terminal, val, fullyFaithfulSheafToPresheaf, instInhabitedSheafBotGrothendieckTopologyType, sheafBotEquivalence, sheafOver, sheafSections, sheafSectionsNatIsoEvaluation, sheafToPresheaf, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf	32
Theorems amalgamateOfArrows_map, amalgamateOfArrows_map_assoc, amalgamate_map, amalgamate_map_assoc, existsUnique_amalgamation_ofArrows, hom_ext, hom_ext_ofArrows, isSheafFor, of_le, isLimit_iff_isSheafFor, isLimit_iff_isSheafFor_presieve, isSeparated_iff_subsingleton, isSheaf_bot, isSheaf_comp_of_isSheaf, isSheaf_iff_isLimit, isSheaf_iff_isLimit_pretopology, isSheaf_iff_isSheaf', isSheaf_iff_isSheaf_comp, isSheaf_iff_isSheaf_forget, isSheaf_iff_multiequalizer, isSheaf_iff_multifork, isSheaf_of_isSheaf_comp, isSheaf_of_isTerminal, isSheaf_of_iso_iff, subsingleton_iff_isSeparatedFor, w, add_app, epi_of_presheaf_epi, mono_of_presheaf_mono, cond, hom_ext, hom_ext_iff, isTerminalTerminal_from_hom, terminal_obj, isSheaf_iff_isSheaf_of_type, sheafBotEquivalence_counitIso, sheafBotEquivalence_functor, sheafBotEquivalence_inverse_map_hom, sheafBotEquivalence_inverse_obj_obj, sheafBotEquivalence_unitIso, sheafOver_obj, sheafSectionsNatIsoEvaluation_hom_app, sheafSectionsNatIsoEvaluation_inv_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app	49
Total	81

CategoryTheory

Definitions

Name	Category	Theorems
Sheaf 📖	CompOp	503 math math: Sheaf.cartesianMonoidalCategoryLift_val, GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso, sheafBotEquivalence_functor, SheafOfModules.pushforward_assoc, Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, Sheaf.ΓHomEquiv_naturality_left_symm, isIso_sheafificationAdjunction_counit, Sheaf.isLocallySurjective_sheafToPresheaf_map_iff, Functor.sheafPushforwardContinuousIso_inv, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem, GrothendieckTopology.Point.skyscraperSheafFunctor_obj_obj, GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, LightCondensed.ihomPoints_apply, Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom, Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous, Equivalence.sheafCongr_functor, GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_down, CompHausLike.LocallyConstant.functor_obj_obj, Presheaf.coherentExtensiveEquivalence_inverse_map_hom, Equivalence.sheafCongr.inverse_obj_obj_map, Equivalence.sheafCongrPrecoherent_unitIso_inv_app_hom_app, Equivalence.sheafCongr.unitIso_inv_app_hom_app, Sheaf.instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, GrothendieckTopology.yonedaULiftEquiv_apply, GrothendieckTopology.yonedaEquiv_symm_app_apply, SheafOfModules.pushforwardNatIso_inv, Functor.IsCoverDense.Types.sheafIso_inv_hom, GrothendieckTopology.W_eq_inverseImage_isomorphisms, Sheaf.toImage_ι_assoc, GrothendieckTopology.overMapPullback_comp_id, Functor.sheafPullbackConstruction.instPreservesFiniteLimitsSheafSheafPullback, Sheaf.isPullback_χ_truth, Functor.sheafPushforwardContinuous_map_hom_app, Sheaf.classifier_χ, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, Equivalence.sheafCongr.functor_obj_obj_map, CondensedMod.isDiscrete_tfae, instFullSheafSheafComposeOfFaithful, SheafOfModules.forgetToSheafModuleCat_map_hom, CompHausLike.LocallyConstant.adjunction_counit, typeEquiv_functor_map_hom_app, sheafificationNatIso_hom_app_hom, CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_carrier, GrothendieckTopology.instFaithfulSheafTypeUliftYoneda, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_sub_apply, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.discrete_map, Functor.IsCoverDense.Types.sheafIso_hom_hom, GrothendieckTopology.overMapPullbackId_inv_app_hom_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, constantCommuteCompose_hom_app_val, GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, Sheaf.isLocallySurjective_comp, Sheaf.adjunction_unit_app_hom, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, Equivalence.sheafCongrPrecoherent_functor_obj_obj_obj, Equivalence.instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify, Equivalence.sheafCongrPreregular_functor_obj_obj_obj, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, Sheaf.isLocallySurjective_iff_epi, Functor.sheafPushforwardContinuousNatTrans_app_hom, LightCondensed.discrete_map, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, Sheaf.cartesianMonoidalCategoryLift_hom, Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, sheafToPresheaf_μ, Presheaf.isLocallyInjective_presheafToSheaf_map_iff, Functor.sheafPushforwardContinuousId'_hom_app_hom_app, GrothendieckTopology.uliftYonedaEquiv_naturality, instEpiSheafTypeToImage, Functor.sheafAdjunctionCocontinuous_counit_app_val, GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, GrothendieckTopology.instFullSheafTypeYoneda, Sheaf.mem_essImage_of_isConstant, GrothendieckTopology.overMapPullbackComp_hom_app_hom_app, hasLimitsEssentiallySmallSite, GrothendieckTopology.overMapPullbackId_hom_app_hom_app, Equivalence.sheafCongr.functor_obj_obj_obj, Adjunction.sheafPushforwardContinuous_unit_app_hom_app, Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app, GrothendieckTopology.MayerVietorisSquare.isPushout, GrothendieckTopology.uliftYonedaEquiv_naturality', Sheaf.instHasColimitsOfShape, Functor.sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify, Functor.OneHypercoverDenseData.essSurj, GrothendieckTopology.uliftYonedaEquiv_symm_map, Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant, Functor.sheafAdjunctionCocontinuous_unit_app_hom, Functor.IsCoverDense.sheafIso_hom_hom, HasSheafify.isLeftExact, GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj, GrothendieckTopology.Point.Hom.sheafFiber_comp_assoc, GrothendieckTopology.yonedaULiftEquiv_naturality', GrothendieckTopology.preservesSheafification_iff_of_adjunctions, Functor.IsCoverDense.faithful_sheafPushforwardContinuous, instIsIsoFunctorOppositeSheafSheafComposeNatTrans, Sheaf.toImage_ι, sheafBotEquivalence_inverse_map_hom, instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms, typeEquiv_inverse_obj, Presheaf.coherentExtensiveEquivalence_unitIso_hom_app_hom_app, Sheaf.epi_of_isLocallySurjective', GrothendieckTopology.W_iff_isIso_map_of_adjunction, GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf, Sheaf.ΓHomEquiv_naturality_left, Sheaf.classifier_truth, Sheaf.classifier_Ω₀, SheafOfModules.pushforwardComp_inv_app_val_app, Sheaf.instHasSubobjectClassifierTypeOfEssentiallySmall, Functor.IsCoverDense.sheafIso_inv_hom, Sheaf.isConstant_iff_forget, Functor.OneHypercoverDenseData.isEquivalence, instHasImagesSheafType, Sheaf.hasFilteredColimitsOfSize, plusPlusSheaf_map_hom, instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, GrothendieckTopology.instFullSheafTypeUliftYoneda, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, SheafOfModules.pushforwardNatTrans_id, topCatToSheafCompHausLike_map_hom_app, Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_app, instPreservesFiniteCoproductsSheafTypeUliftYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf, Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left, Presheaf.coherentExtensiveEquivalence_functor_obj_obj, GrothendieckTopology.W_adj_unit_app, Sheaf.cartesianMonoidalCategorySnd_hom, Sheaf.instHasFunctorialFactorizationLocallySurjectiveLocallyInjective, Sheaf.isLocallySurjective_iff_epi', SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, typeEquiv_unitIso_hom_app, Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, Sheaf.cartesianMonoidalCategorySnd_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, Sheaf.classifier_Ω, GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, Sheaf.instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CompHausLike.LocallyConstant.counit_app_hom_app, Functor.sheafAdjunctionCocontinuous_counit_app_hom, Presheaf.coherentExtensiveEquivalence_inverse_obj_obj, Equivalence.sheafCongrPrecoherent_counitIso_hom_app_hom_app, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf_1, SheafOfTypes.finitary_extensive, Sheaf.instIsGrothendieckAbelian, GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_symm_apply, Sheaf.natTransΓRes_app, GrothendieckTopology.yonedaEquiv_naturality', equivYoneda'_hom_hom, GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, SheafOfModules.Presentation.quasicoherentData_presentation, Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left, typeEquiv_counitIso_hom_app_hom_app, GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, GrothendieckTopology.overMapPullback_assoc_assoc, Sheaf.isSheaf_of_isLimit, Equivalence.sheafCongr.unitIso_hom_app_hom_app, Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom, Functor.sheafPushforwardContinuousId_hom_app_hom_app, Sheaf.instHasFiniteColimits, sheafToPresheaf_δ, Sheaf.Hom.mono_iff_presheaf_mono, typeEquiv_unitIso_inv_app, GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, isRegularEpiCategory_sheaf, GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app, GrothendieckTopology.Point.Hom.sheafFiber_comp, PresheafOfModules.sheafification_map, toPresheafToSheafCompComposeAndSheafify_app, GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app, CompHausLike.LocallyConstant.functor_map_hom, instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf, SheafOfModules.pullback_comp_id, GrothendieckTopology.map_yonedaEquiv', sheafBotEquivalence_unitIso, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zero_apply, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_add_apply, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, GrothendieckTopology.Point.skyscraperSheafFunctor_map_hom, isSheaf_pointwiseColimit, topCatToSheafCompHausLike_obj, Sheaf.adjunction_counit_app_val, GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, SheafOfTypes.adhesive, GrothendieckTopology.yonedaEquiv_comp, GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, Equivalence.sheafCongr.inverse_obj_obj_obj, Equivalence.sheafCongrPreregular_inverse_obj_obj_obj, LightCondensed.forget_map_hom_app, Sheaf.isSeparating, Sheaf.isGrothendieckAbelian_of_essentiallySmall, ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type, GrothendieckTopology.yonedaEquiv_symm_map, Functor.IsDenseSubsite.sheafEquiv_inverse, Sheaf.ΓObjEquivSections_naturality_symm, Sheaf.mono_of_isLocallyInjective, Sheaf.classifier_χ₀, Functor.sheafPushforwardContinuous_obj_obj_obj, Sheaf.ΓRes_map_assoc, Sheaf.ab5ofSize, GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, Sheaf.ΓObjEquivHom_naturality_symm, SheafOfModules.toSheaf_obj_obj, instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf, Sheaf.hasSeparator, instFaithfulSheafSheafCompose, GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso, SheafOfModules.conjugateEquiv_pullbackComp_inv, Equivalence.sheafCongrPreregular_inverse_map_hom_app, Sheaf.Hom.mono_of_presheaf_mono, Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, plusPlusSheaf_obj_obj, sheafComposeNatTrans_app_uniq, Presheaf.coherentExtensiveEquivalence_functor_map_hom, Sheaf.instHasFiniteLimits, Equivalence.sheafCongrPreregular_inverse_obj_obj_map, instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify, CompHausLike.LocallyConstant.adjunction_left_triangle, Sheaf.isLocallyInjective_forget, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, SheafOfModules.pullback_id_comp, instReflectsIsomorphismsSheafSheafCompose, sheafificationNatIso_inv_app_hom, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc, Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, Sheaf.coneΓ_pt, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_nsmul_apply, instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, GrothendieckTopology.uliftYoneda_obj_obj_map_down, Sheaf.isConstant_iff_isIso_counit_app', SheafOfTypes.balanced, preservesFiniteLimits_presheafToSheaf, typeEquiv_counitIso_inv_app_hom_app, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_neg_apply, typeEquiv_inverse_map, SheafOfModules.pushforward_map_val, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, GrothendieckTopology.Point.instIsLeftAdjointSheafSheafFiber, GrothendieckTopology.overMapPullbackCongr_eq_eqToIso, Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, Sheaf.cartesianMonoidalCategoryFst_hom, SheafOfModules.pushforwardComp_hom_app_val_app, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, Equivalence.sheafCongrPreregular_functor_map_hom_app, Sheaf.adjunction_unit_app_val, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, GrothendieckTopology.uliftYoneda_obj_obj_obj, instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf, instPreservesColimitsOfShapeSheafTypeYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf, Equivalence.sheafCongrPreregular_counitIso_inv_app_hom_app, sheafificationIso_inv_hom, Equivalence.sheafCongr_counitIso, GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app, AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf, Functor.sheafPushforwardContinuous_obj_obj_map, Functor.toSheafify_pullbackSheafificationCompatibility, Sheaf.ΓHomEquiv_naturality_right_symm, GrothendieckTopology.preservesLimitsOfSize_yoneda, Sheaf.ΓObjEquivHom_naturality, Sheaf.ΓRes_map, SheafOfModules.pushforwardCongr_symm, GrothendieckTopology.Point.sheafFiberComapIso_hom_app, GrothendieckTopology.map_uliftYonedaEquiv', AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, Sheaf.cartesianMonoidalCategoryWhiskerRight_val, SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf, ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful, CondensedSet.isDiscrete_tfae, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isModule_smul_apply, Equivalence.sheafCongr.counitIso_inv_app_hom_app, sheafBotEquivalence_inverse_obj_obj, Sheaf.instHasLimitsOfShape, Functor.IsCoverDense.iso_of_restrict_iso, GrothendieckTopology.overMapPullback_comp_id_assoc, GrothendieckTopology.MayerVietorisSquare.shortComplex_g, plusPlusSheaf_preservesZeroMorphisms, GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, coherentTopology.epi_π_app_zero_of_epi, Sheaf.instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, Sheaf.isConstant_iff_mem_essImage, Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits, sheafCompose_map_hom, GrothendieckTopology.yonedaEquiv_naturality, sheafificationAdjunction_unit_app, sheafificationIso_hom_hom, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf, CompHausLike.LocallyConstantModule.functor_obj_obj_obj_isAddCommGroup_zsmul_apply, GrothendieckTopology.Point.Hom.sheafFiber_id, instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction, Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf, GrothendieckTopology.map_yonedaULiftEquiv', SheafOfModules.unitToPushforwardObjUnit_val_app_apply, SheafOfModules.pullback_assoc, GrothendieckTopology.uliftYonedaEquiv_apply, instPreservesColimitSheafTypeYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf_1, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, presheafToSheaf_additive, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, Sheaf.Hom.epi_of_presheaf_epi, Sheaf.isLocallyInjective_sheafToPresheaf_map_iff, Functor.sheafPullbackConstruction.preservesFiniteLimits, GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left, instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf, Sheaf.isConstant_iff_of_equivalence, Sheaf.hasExactColimitsOfShape, instPreservesLimitsOfShapeSheafTypeUliftYoneda, presheafToSheafCompComposeAndSheafifyIso_inv_app, Sheaf.instHasFiniteCoproducts, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, GrothendieckTopology.instFaithfulSheafTypeYoneda, Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget, Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right_assoc, Sheaf.cohomologyFunctor_obj, Sheaf.mono_of_injective, GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW, GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, Equivalence.sheafCongrPrecoherent_functor_obj_obj_map, Equivalence.sheafCongrPrecoherent_inverse_obj_obj_obj, Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, Equivalence.sheafCongrPrecoherent_inverse_obj_obj_map, Sheaf.epi_of_isLocallySurjective, sheafToPresheaf_η, GrothendieckTopology.overMapPullbackCongr_inv_app_hom_app, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, SheafOfModules.toSheaf_map_hom, ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, Sheaf.instHasColimitsOfSize, SheafOfModules.pushforwardNatTrans_app_val_app, GrothendieckTopology.W_iff, GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction, Equivalence.sheafCongrPreregular_unitIso_inv_app_hom_app, GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, Functor.sheafPushforwardContinuousIso_hom, GrothendieckTopology.yonedaULiftEquiv_naturality, Functor.sheafPushforwardContinuousComp_inv_app_hom_app, Sheaf.cartesianMonoidalCategoryFst_val, Sheaf.ΓHomEquiv_naturality_right, Sheaf.instIsLeftAdjointComposeAndSheafify, Equivalence.sheafCongr.functor_map_hom_app, GrothendieckTopology.Point.instIsRightAdjointSheafSkyscraperSheafFunctor, Sheaf.isSeparator, GrothendieckTopology.map_uliftYonedaEquiv, Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app, Equivalence.sheafCongrPrecoherent_functor_map_hom_app, Equivalence.sheafCongrPrecoherent_inverse_map_hom_app, GrothendieckTopology.MayerVietorisSquare.shortComplex_f, Sheaf.isLocallyBijective_iff_isIso, instIsConstantObjSheafSheafCompose, instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify, sheafToPresheaf_ε, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, sheafificationAdjunction_counit_app_val, preservesLimitsOfShape_presheafToSheaf, GrothendieckTopology.yonedaULiftEquiv_comp, GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp, GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, hasColimitsEssentiallySmallSite, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, SheafOfModules.pushforward_comp_id, Equivalence.sheafCongr_inverse, GrothendieckTopology.overMapPullback_id_comp_assoc, SheafOfModules.forgetToSheafModuleCat_obj_obj, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, constantSheafAdj_counit_w, sheafCompose_id, instPreservesFiniteCoproductsSheafTypeYonedaOfPreservesFiniteProductsOppositeObjFunctorIsSheaf, CompHausLike.LocallyConstant.unit_app, typeEquiv_functor_obj_obj_map, AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty, yoneda'_comp, GrothendieckTopology.overMapPullbackCongr_hom_app_hom_app, coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map, GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, typeEquiv_functor_obj_obj_obj, GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, Sheaf.sheafifyCocone_ι_app_val_assoc, SheafOfModules.conjugateEquiv_pullbackId_hom, Sheaf.Hom.add_app, Sheaf.hasLimitsOfSize, constantCommuteCompose_hom_app_hom, GrothendieckTopology.yonedaULiftEquiv_symm_map, Sheaf.adjunction_counit_app_hom, sheafToPresheaf_isRightAdjoint, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, GrothendieckTopology.Point.sheafFiberComapIso_inv_app, GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, Functor.sheafPushforwardContinuousComp'_inv_app_hom_app, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj, GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, GrothendieckTopology.yonedaEquiv_symm_naturality_left, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left_assoc, Functor.sheafPushforwardContinuousId'_inv_app_hom_app, GrothendieckTopology.yoneda_map_hom, Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify, SheafOfModules.pushforwardNatTrans_app_val_app_apply, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, Equivalence.sheafCongrPreregular_functor_obj_obj_map, instIsRegularEpiCategorySheafTypeOfHasSheafify, sheafCompose_obj_obj, SheafOfModules.pushforward_id_comp, sheafBotEquivalence_counitIso, Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb, GrothendieckTopology.W_eq_W_range_sheafToPresheaf_obj, sheafification_reflective, Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, sheafHomSectionsEquiv_symm_apply_coe_apply, Functor.isEquivalence_of_isOneHypercoverDense, GrothendieckTopology.Point.sheafFiberCompIso_hom_app, Adjunction.sheafPushforwardContinuous_counit_app_hom_app, GrothendieckTopology.yoneda_obj_obj, GrothendieckTopology.map_yonedaEquiv, Sheaf.isLocallySurjective_iff_isIso, GrothendieckTopology.overMapPullback_assoc, Sheaf.ΓObjEquivSections_naturality, Functor.sheafPushforwardContinuousComp'_hom_app_hom_app, constantSheafAdj_counit_app, GrothendieckTopology.uliftYoneda_map_hom_app_down, sheafSectionsNatIsoEvaluation_hom_app, SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat, GrothendieckTopology.overMapPullback_id_comp, Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map, Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify, Sheaf.isConstant_iff_isIso_counit_app, GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map, instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf, Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, Sheaf.ΓRes_naturality, Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app, SheafOfModules.pushforwardNatIso_hom, Functor.sheafPushforwardContinuousComp_hom_app_hom_app, Equivalence.sheafCongr_unitIso, GrothendieckTopology.Point.instPreservesFiniteColimitsSheafSheafFiber, Sheaf.sheafifyCocone_ι_app_val, Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, equivYoneda'_inv_hom, Functor.IsDenseSubsite.full_sheafPushforwardContinuous, GrothendieckTopology.map_yonedaULiftEquiv, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_app, sheafSectionsNatIsoEvaluation_inv_app, Sheaf.IsConstant.mem_essImage, Functor.sheafPushforwardContinuousId_inv_app_hom_app, Functor.sheafAdjunctionCocontinuous_unit_app_val, yoneda'_obj_obj, CompHausLike.LocallyConstantModule.functor_map_hom_app_hom_apply_apply, SheafOfModules.pushforward_obj_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom, GrothendieckTopology.Point.sheafFiberCompIso_inv_app, instPreservesColimitsOfShapeSheafTypeUliftYonedaOfPreservesLimitsOfShapeOppositeObjFunctorIsSheaf, instPreservesLimitsOfShapeSheafTypeYoneda, Sheaf.instHasFiniteProducts, GrothendieckTopology.yonedaEquiv_yoneda_map, GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, Condensed.discrete_obj, GrothendieckTopology.uliftYonedaEquiv_comp, Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom, sheafComposeNatTrans_fac, ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms, GrothendieckTopology.yonedaEquiv_apply, yoneda'_map_hom, Equivalence.sheafCongr.inverse_map_hom_app, GrothendieckTopology.yonedaEquiv_symm_naturality_right, CompHausLike.LocallyConstant.adjunction_unit, Functor.IsDenseSubsite.faithful_sheafPushforwardContinuous, Presheaf.isLocallySurjective_presheafToSheaf_map_iff, SheafOfModules.pushforwardNatTrans_comp, Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app, Sheaf.cartesianMonoidalCategoryWhiskerRight_hom, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, instMonoSheafTypeImageι, Sheaf.isTerminalTerminal_from_hom, Functor.IsCoverDense.full_sheafPushforwardContinuous, GrothendieckTopology.MayerVietorisSquare.shortComplex_exact, Equivalence.sheafCongr.counitIso_hom_app_hom_app, sheafCompose_comp
fullyFaithfulSheafToPresheaf 📖	CompOp	—
instInhabitedSheafBotGrothendieckTopologyType 📖	CompOp	—
sheafBotEquivalence 📖	CompOp	5 math math: sheafBotEquivalence_functor, sheafBotEquivalence_inverse_map_hom, sheafBotEquivalence_unitIso, sheafBotEquivalence_inverse_obj_obj, sheafBotEquivalence_counitIso
sheafOver 📖	CompOp	5 math math: Functor.IsCoverDense.isoOver_hom_app, Functor.IsCoverDense.sheafCoyonedaHom_app, Functor.IsCoverDense.homOver_app, sheafOver_obj, Functor.IsCoverDense.isoOver_inv_app
sheafSections 📖	CompOp	14 math math: CompHausLike.LocallyConstant.adjunction_counit, Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant, CompHausLike.LocallyConstant.counit_app_hom_app, Sheaf.natTransΓRes_app, CompHausLike.LocallyConstant.adjunction_left_triangle, Sheaf.isConstant_iff_isIso_counit_app', CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, constantSheafAdj_counit_w, CompHausLike.LocallyConstant.unit_app, constantSheafAdj_counit_app, sheafSectionsNatIsoEvaluation_hom_app, Sheaf.isConstant_iff_isIso_counit_app, sheafSectionsNatIsoEvaluation_inv_app, CompHausLike.LocallyConstant.adjunction_unit
sheafSectionsNatIsoEvaluation 📖	CompOp	2 math math: sheafSectionsNatIsoEvaluation_hom_app, sheafSectionsNatIsoEvaluation_inv_app
sheafToPresheaf 📖	CompOp	100 math math: GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso, sheafBotEquivalence_functor, isIso_sheafificationAdjunction_counit, Sheaf.isLocallySurjective_sheafToPresheaf_map_iff, GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_hom_app_down, Presheaf.coherentExtensiveEquivalence_inverse_map_hom, GrothendieckTopology.yonedaULiftEquiv_apply, Functor.sheafPushforwardContinuous_map_hom_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafificationNatIso_hom_app_hom, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, Functor.sheafPushforwardContinuousNatTrans_app_hom, sheafToPresheaf_μ, HasSheafify.isLeftExact, GrothendieckTopology.preservesSheafification_iff_of_adjunctions, instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app, Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, GrothendieckTopology.W_adj_unit_app, typeEquiv_unitIso_hom_app, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_hom, GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, typeEquiv_counitIso_hom_app_hom_app, Sheaf.isSheaf_of_isLimit, sheafToPresheaf_δ, typeEquiv_unitIso_inv_app, GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app, GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app, instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, isSheaf_pointwiseColimit, LightCondensed.forget_map_hom_app, GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, Equivalence.sheafCongrPreregular_inverse_map_hom_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, Presheaf.coherentExtensiveEquivalence_functor_map_hom, sheafificationNatIso_inv_app_hom, Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, GrothendieckTopology.uliftYoneda_obj_obj_map_down, typeEquiv_counitIso_inv_app_hom_app, SheafOfModules.pushforward_map_val, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, Equivalence.sheafCongrPreregular_functor_map_hom_app, GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app, GrothendieckTopology.map_uliftYonedaEquiv', Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits, sheafCompose_map_hom, sheafificationAdjunction_unit_app, instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf, instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction, GrothendieckTopology.map_yonedaULiftEquiv', GrothendieckTopology.uliftYonedaEquiv_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_apply, GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, Sheaf.isLocallyInjective_sheafToPresheaf_map_iff, GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, sheafToPresheaf_η, GrothendieckTopology.overMapPullbackCongr_inv_app_hom_app, Equivalence.sheafCongr.functor_map_hom_app, GrothendieckTopology.map_uliftYonedaEquiv, Equivalence.sheafCongrPrecoherent_functor_map_hom_app, Equivalence.sheafCongrPrecoherent_inverse_map_hom_app, sheafToPresheaf_ε, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, sheafificationAdjunction_counit_app_val, yoneda'_comp, GrothendieckTopology.overMapPullbackCongr_hom_app_hom_app, GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, Sheaf.sheafifyCocone_ι_app_val_assoc, sheafToPresheaf_isRightAdjoint, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom, instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj, sheafBotEquivalence_counitIso, GrothendieckTopology.W_eq_W_range_sheafToPresheaf_obj, sheafification_reflective, constantSheafAdj_counit_app, GrothendieckTopology.uliftYoneda_map_hom_app_down, sheafSectionsNatIsoEvaluation_hom_app, GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map, Presheaf.coherentExtensiveEquivalence_counitIso_inv_app_hom_app, Presheaf.coherentExtensiveEquivalence_counitIso_hom_app_hom_app, Sheaf.sheafifyCocone_ι_app_val, GrothendieckTopology.map_yonedaULiftEquiv, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_hom_app, sheafSectionsNatIsoEvaluation_inv_app, SheafOfModules.pushforward_obj_val, GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, sheafComposeNatTrans_fac, Equivalence.sheafCongr.inverse_map_hom_app
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf 📖	CompOp	4 math math: sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf 📖	CompOp	3 math math: sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_iff_isSheaf_of_type 📖	mathematical	—	Presheaf.IsSheaf types Presieve.IsSheaf	—	Presieve.isSheaf_iso Presieve.IsSheafFor.valid_glue Presieve.IsSeparatedFor.ext Presieve.IsSheafFor.isSeparatedFor
sheafBotEquivalence_counitIso 📖	mathematical	—	Equivalence.counitIso Sheaf Bot.bot GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Functor Opposite Category.opposite ObjectProperty.FullSubcategory.category Functor.category Presheaf.IsSheaf sheafBotEquivalence Iso.refl Functor.comp Presheaf.isSheaf_bot ObjectProperty.FullSubcategory ObjectProperty.FullSubcategory.obj sheafToPresheaf	—	Presheaf.isSheaf_bot
sheafBotEquivalence_functor 📖	mathematical	—	Equivalence.functor Sheaf Bot.bot GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Functor Opposite Category.opposite ObjectProperty.FullSubcategory.category Functor.category Presheaf.IsSheaf sheafBotEquivalence sheafToPresheaf	—	—
sheafBotEquivalence_inverse_map_hom 📖	mathematical	—	InducedCategory.Hom.hom ObjectProperty.FullSubcategory Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf Bot.bot GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder ObjectProperty.FullSubcategory.obj Presheaf.isSheaf_bot Functor.map Sheaf ObjectProperty.FullSubcategory.category Equivalence.inverse sheafBotEquivalence	—	Presheaf.isSheaf_bot
sheafBotEquivalence_inverse_obj_obj 📖	mathematical	—	ObjectProperty.FullSubcategory.obj Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf Bot.bot GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Functor.obj Sheaf ObjectProperty.FullSubcategory.category Equivalence.inverse sheafBotEquivalence	—	—
sheafBotEquivalence_unitIso 📖	mathematical	—	Equivalence.unitIso Sheaf Bot.bot GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Functor Opposite Category.opposite ObjectProperty.FullSubcategory.category Functor.category Presheaf.IsSheaf sheafBotEquivalence Iso.refl Functor.id	—	—
sheafOver_obj 📖	mathematical	—	ObjectProperty.FullSubcategory.obj Functor Opposite Category.opposite types Functor.category Presheaf.IsSheaf sheafOver Functor.comp Functor.obj coyoneda Opposite.op	—	—
sheafSectionsNatIsoEvaluation_hom_app 📖	mathematical	—	NatTrans.app Sheaf ObjectProperty.FullSubcategory.category Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf Functor.obj sheafSections Opposite.op Iso.hom Functor.comp sheafToPresheaf evaluation sheafSectionsNatIsoEvaluation CategoryStruct.id Category.toCategoryStruct ObjectProperty.FullSubcategory.obj	—	—
sheafSectionsNatIsoEvaluation_inv_app 📖	mathematical	—	NatTrans.app Sheaf ObjectProperty.FullSubcategory.category Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf Functor.obj sheafSections Opposite.op Iso.inv Functor.comp sheafToPresheaf evaluation sheafSectionsNatIsoEvaluation CategoryStruct.id Category.toCategoryStruct ObjectProperty.FullSubcategory.obj	—	—
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app 📖	mathematical	—	Iso.app Sheaf ObjectProperty.FullSubcategory.category Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf types Functor.obj Functor.comp Functor.op sheafToPresheaf coyoneda Functor.whiskeringLeft Opposite.op sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf Equiv.toIso Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct ObjectProperty.FullSubcategory.obj Opposite.unop Equiv.symm Sheaf.homEquiv	—	—
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom 📖	mathematical	—	InducedCategory.Hom.hom ObjectProperty.FullSubcategory Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf ObjectProperty.FullSubcategory.obj Opposite.unop Sheaf NatTrans.app ObjectProperty.FullSubcategory.category types Functor.obj Functor.comp Functor.op sheafToPresheaf coyoneda Functor.whiskeringLeft Iso.hom sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct EquivLike.toFunLike yoneda Opposite.op Equiv.instEquivLike Equiv.ulift uliftCoyoneda Iso.inv uliftCoyonedaIsoCoyoneda	—	—
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app 📖	mathematical	—	NatTrans.app Sheaf ObjectProperty.FullSubcategory.category Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf types Functor.obj coyoneda Functor.comp Functor.op sheafToPresheaf Functor.whiskeringLeft Iso.inv sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf InducedCategory.Hom.hom ObjectProperty.FullSubcategory ObjectProperty.FullSubcategory.obj Opposite.unop	—	—
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app 📖	mathematical	—	Iso.app Opposite Sheaf Category.opposite ObjectProperty.FullSubcategory.category Functor Functor.category Presheaf.IsSheaf types Functor.obj Functor.comp sheafToPresheaf yoneda Functor.whiskeringLeft Functor.op sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf Opposite.op Equiv.toIso Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct ObjectProperty.FullSubcategory.obj Opposite.unop Equiv.symm Sheaf.homEquiv	—	—
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom 📖	mathematical	—	InducedCategory.Hom.hom ObjectProperty.FullSubcategory Functor Opposite Category.opposite Functor.category Presheaf.IsSheaf ObjectProperty.FullSubcategory.obj Opposite.unop Sheaf NatTrans.app ObjectProperty.FullSubcategory.category types Functor.obj Functor.comp sheafToPresheaf yoneda Functor.whiskeringLeft Functor.op Iso.hom sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.ulift uliftYoneda Iso.inv uliftYonedaIsoYoneda Opposite.op	—	—
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app 📖	mathematical	—	NatTrans.app Opposite Sheaf Category.opposite ObjectProperty.FullSubcategory.category Functor Functor.category Presheaf.IsSheaf types Functor.obj yoneda Functor.comp sheafToPresheaf Functor.whiskeringLeft Functor.op Iso.inv sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf InducedCategory.Hom.hom ObjectProperty.FullSubcategory ObjectProperty.FullSubcategory.obj Opposite.unop	—	—

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
IsSeparated 📖	MathDef	2 math math: IsSheaf.isSeparated, CategoryTheory.Sheaf.isSeparated
IsSheaf' 📖	MathDef	1 math math: isSheaf_iff_isSheaf'
conesEquivSieveCompatibleFamily 📖	CompOp	—
firstMap 📖	CompOp	1 math math: w
firstObj 📖	CompOp	1 math math: w
forkMap 📖	CompOp	1 math math: w
homEquivAmalgamation 📖	CompOp	—
isLimitOfIsSheaf 📖	CompOp	—
isSheafForIsSheafFor' 📖	CompOp	—
secondMap 📖	CompOp	1 math math: w
secondObj 📖	CompOp	1 math math: w

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLimit_iff_isSheafFor 📖	mathematical	—	CategoryTheory.Limits.IsLimit Opposite CategoryTheory.Presieve.category CategoryTheory.Sieve.arrows CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Presieve.diagram CategoryTheory.Functor.mapCone CategoryTheory.Limits.Cocone.op CategoryTheory.Presieve.cocone CategoryTheory.Presieve.IsSheafFor CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda	—	Equiv.nonempty_congr Classical.nonempty_pi unique_subtype_iff_existsUnique Equiv.left_inv
isLimit_iff_isSheafFor_presieve 📖	mathematical	—	CategoryTheory.Limits.IsLimit Opposite CategoryTheory.Presieve.category CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Presieve.diagram CategoryTheory.Functor.mapCone CategoryTheory.Limits.Cocone.op CategoryTheory.Presieve.cocone CategoryTheory.Presieve.IsSheafFor CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda	—	isLimit_iff_isSheafFor CategoryTheory.Presieve.isSheafFor_iff_generate
isSeparated_iff_subsingleton 📖	mathematical	—	CategoryTheory.Presieve.IsSeparated CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op Quiver.Hom CategoryTheory.Limits.Cone CategoryTheory.Presieve.category CategoryTheory.Sieve.arrows CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.op CategoryTheory.Presieve.diagram CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.category CategoryTheory.Functor.mapCone CategoryTheory.Limits.Cocone.op CategoryTheory.Presieve.cocone	—	subsingleton_iff_isSeparatedFor
isSheaf_bot 📖	mathematical	—	IsSheaf Bot.bot CategoryTheory.GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	CategoryTheory.Presieve.isSheaf_bot
isSheaf_comp_of_isSheaf 📖	mathematical	IsSheaf	IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	isSheaf_iff_isLimit Nonempty.map CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
isSheaf_iff_isLimit 📖	mathematical	—	IsSheaf CategoryTheory.Limits.IsLimit Opposite CategoryTheory.Presieve.category CategoryTheory.Sieve.arrows CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Presieve.diagram CategoryTheory.Functor.mapCone CategoryTheory.Limits.Cocone.op CategoryTheory.Presieve.cocone	—	isLimit_iff_isSheafFor
isSheaf_iff_isLimit_pretopology 📖	mathematical	—	IsSheaf CategoryTheory.Pretopology.toGrothendieck CategoryTheory.Limits.IsLimit Opposite CategoryTheory.Presieve.category CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Presieve.diagram CategoryTheory.Functor.mapCone CategoryTheory.Limits.Cocone.op CategoryTheory.Presieve.cocone	—	isLimit_iff_isSheafFor_presieve
isSheaf_iff_isSheaf' 📖	mathematical	CategoryTheory.Limits.HasProducts	IsSheaf IsSheaf'	—	w CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.Equalizer.Presieve.w CategoryTheory.Equalizer.Presieve.sheaf_condition CategoryTheory.Presieve.isSheafFor_iff_generate CategoryTheory.coyonedaPreservesLimitsOfShape CategoryTheory.Sieve.generate_sieve CategoryTheory.coyoneda_preservesLimit
isSheaf_iff_isSheaf_comp 📖	mathematical	—	IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	isSheaf_comp_of_isSheaf isSheaf_of_isSheaf_comp CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms
isSheaf_iff_isSheaf_forget 📖	mathematical	—	IsSheaf CategoryTheory.types CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	CategoryTheory.Limits.hasLimitsOfSizeShrink CategoryTheory.Limits.preservesLimitsOfSize_shrink isSheaf_iff_isSheaf_comp
isSheaf_iff_multiequalizer 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.GrothendieckTopology.Cover.index	IsSheaf CategoryTheory.IsIso CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Limits.multiequalizer CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.GrothendieckTopology.Cover.toMultiequalizer	—	isSheaf_iff_multifork CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.limit.lift_π
isSheaf_iff_multifork 📖	mathematical	—	IsSheaf CategoryTheory.Limits.IsLimit CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.GrothendieckTopology.Cover.multifork	—	CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w CategoryTheory.Limits.IsLimit.fac CategoryTheory.Limits.IsLimit.uniq CategoryTheory.Limits.Cone.w CategoryTheory.Category.assoc
isSheaf_of_isSheaf_comp 📖	mathematical	IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	IsSheaf	—	isSheaf_iff_isLimit Nonempty.map CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits
isSheaf_of_isTerminal 📖	mathematical	—	IsSheaf CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.const	—	CategoryTheory.Limits.IsTerminal.hom_ext
isSheaf_of_iso_iff 📖	mathematical	—	IsSheaf	—	CategoryTheory.Presieve.isSheaf_iso
subsingleton_iff_isSeparatedFor 📖	mathematical	—	Quiver.Hom CategoryTheory.Limits.Cone Opposite CategoryTheory.Presieve.category CategoryTheory.Sieve.arrows CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Presieve.diagram CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.category CategoryTheory.Functor.mapCone CategoryTheory.Limits.Cocone.op CategoryTheory.Presieve.cocone CategoryTheory.Presieve.IsSeparatedFor CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda	—	CategoryTheory.Presieve.is_compatible_of_exists_amalgamation CategoryTheory.Presieve.compatible_iff_sieveCompatible Equiv.injective Equiv.left_inv
w 📖	mathematical	CategoryTheory.Limits.HasProducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op firstObj secondObj forkMap firstMap secondMap	—	CategoryTheory.Limits.limit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Functor.map_comp CategoryTheory.op_comp CategoryTheory.Limits.pullback.condition

CategoryTheory.Presheaf.IsSheaf

Definitions

Name	Category	Theorems
amalgamate 📖	CompOp	2 math math: amalgamate_map, amalgamate_map_assoc
amalgamateOfArrows 📖	CompOp	2 math math: amalgamateOfArrows_map, amalgamateOfArrows_map_assoc
isLimitMultifork 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
amalgamateOfArrows_map 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op amalgamateOfArrows CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	existsUnique_amalgamation_ofArrows
amalgamateOfArrows_map_assoc 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op amalgamateOfArrows CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' amalgamateOfArrows_map
amalgamate_map 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.Z CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁ CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y amalgamate CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f	—	CategoryTheory.Presieve.IsSheafFor.valid_glue CategoryTheory.GrothendieckTopology.Cover.condition CategoryTheory.GrothendieckTopology.Cover.Arrow.hf
amalgamate_map_assoc 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.Z CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁ CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op amalgamate CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' amalgamate_map
existsUnique_amalgamation_ofArrows 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	ExistsUnique Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op	—	CategoryTheory.Presieve.isSheafFor_arrows_iff CategoryTheory.Presieve.isSheafFor_iff_generate
hom_ext 📖	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f	—	—	CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheafFor.isSeparatedFor CategoryTheory.GrothendieckTopology.Cover.condition
hom_ext_ofArrows 📖	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	—	hom_ext CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
isSheafFor 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.types CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Sieve.arrows	—	CategoryTheory.isSheaf_iff_isSheaf_of_type
of_le 📖	mathematical	CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Presheaf.IsSheaf	—	—

CategoryTheory.Presieve.FamilyOfElements.SieveCompatible

Definitions

Name	Category	Theorems
cone 📖	CompOp	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
homEquiv 📖	CompOp	2 math math: CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app
isTerminalOfBotCover 📖	CompOp	—
isTerminalOfEqTop 📖	CompOp	—
isTerminalTerminal 📖	CompOp	3 math math: isPullback_χ_truth, classifier_χ₀, isTerminalTerminal_from_hom
terminal 📖	CompOp	6 math math: isPullback_χ_truth, terminal_obj, classifier_Ω₀, classifier_χ₀, truth_hom, isTerminalTerminal_from_hom
val 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cond 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	CategoryTheory.ObjectProperty.FullSubcategory.property
hom_ext 📖	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj	—	—	CategoryTheory.ObjectProperty.hom_ext CategoryTheory.NatTrans.ext'
hom_ext_iff 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj	—	CategoryTheory.ObjectProperty.hom_ext CategoryTheory.NatTrans.ext'
isTerminalTerminal_from_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.ObjectProperty.FullSubcategory.obj terminal CategoryTheory.Limits.IsTerminal.from CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category isTerminalTerminal CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Functor.isTerminalConst	—	—
terminal_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf terminal CategoryTheory.Functor.obj CategoryTheory.Functor.const	—	—

CategoryTheory.Sheaf.Hom

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Preadditive.fullSubcategory CategoryTheory.functorCategoryPreadditive CategoryTheory.Functor.obj	—	—
epi_of_presheaf_epi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits CategoryTheory.Limits.fullyFaithful_reflectsColimits CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
mono_of_presheaf_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι

---

← Back to Index