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, addCommGroup, val, homEquiv, instCategorySheaf, instInhabitedHom, isTerminalOfBotCover, val, fullyFaithfulSheafToPresheaf, instAddHomSheaf, instInhabitedSheafBotGrothendieckTopologyType, instNegHomSheaf, instPreadditiveSheaf, instSubHomSheaf, instZeroHomSheaf, sheafBotEquivalence, sheafHomHasNSMul, sheafHomHasZSMul, sheafOver, sheafSections, sheafSectionsNatIsoEvaluation, sheafToPresheaf, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf	38
Theorems amalgamateOfArrows_map, amalgamateOfArrows_map_assoc, amalgamate_map, amalgamate_map_assoc, existsUnique_amalgamation_ofArrows, hom_ext, hom_ext_ofArrows, isSheafFor, 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, ext, ext_iff, mono_of_presheaf_mono, comp_val, comp_val_assoc, cond, hom_ext, hom_ext_iff, id_val, fullyFaithfulSheafToPresheaf_preimage_val, instFaithfulSheafFunctorOppositeSheafToPresheaf, instFullSheafFunctorOppositeSheafToPresheaf, instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf, isSheaf_iff_isSheaf_of_type, sheafBotEquivalence_counitIso, sheafBotEquivalence_functor, sheafBotEquivalence_inverse_map_val, sheafBotEquivalence_inverse_obj_val, sheafBotEquivalence_unitIso, sheafOver_val, sheafSectionsNatIsoEvaluation_hom_app, sheafSectionsNatIsoEvaluation_inv_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafToPresheaf_map, sheafToPresheaf_obj	57
Total	95

CategoryTheory

Definitions

Name	Category	Theorems
fullyFaithfulSheafToPresheaf 📖	CompOp	1 math math: fullyFaithfulSheafToPresheaf_preimage_val
instAddHomSheaf 📖	CompOp	1 math math: Sheaf.Hom.add_app
instInhabitedSheafBotGrothendieckTopologyType 📖	CompOp	—
instNegHomSheaf 📖	CompOp	—
instPreadditiveSheaf 📖	CompOp	14 math math: GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, GrothendieckTopology.MayerVietorisSquare.shortComplex_g, plusPlusSheaf_preservesZeroMorphisms, presheafToSheaf_additive, GrothendieckTopology.MayerVietorisSquare.shortComplex_f, GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, GrothendieckTopology.MayerVietorisSquare.shortComplex_exact
instSubHomSheaf 📖	CompOp	—
instZeroHomSheaf 📖	CompOp	—
sheafBotEquivalence 📖	CompOp	5 math math: sheafBotEquivalence_functor, sheafBotEquivalence_inverse_map_val, sheafBotEquivalence_unitIso, sheafBotEquivalence_inverse_obj_val, sheafBotEquivalence_counitIso
sheafHomHasNSMul 📖	CompOp	—
sheafHomHasZSMul 📖	CompOp	—
sheafOver 📖	CompOp	5 math math: sheafOver_val, Functor.IsCoverDense.isoOver_hom_app, Functor.IsCoverDense.sheafCoyonedaHom_app, Functor.IsCoverDense.homOver_app, Functor.IsCoverDense.isoOver_inv_app
sheafSections 📖	CompOp	14 math math: CompHausLike.LocallyConstant.adjunction_counit, Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant, Sheaf.natTransΓRes_app, CompHausLike.LocallyConstant.adjunction_left_triangle, Sheaf.isConstant_iff_isIso_counit_app', CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, CompHausLike.LocallyConstant.counit_app_val, 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	77 math math: GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso, sheafBotEquivalence_functor, isIso_sheafificationAdjunction_counit, Sheaf.isLocallySurjective_sheafToPresheaf_map_iff, GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafificationNatIso_inv_app_val, instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafificationNatIso_hom_app_val, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheaf_μ, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, HasSheafify.isLeftExact, GrothendieckTopology.preservesSheafification_iff_of_adjunctions, instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, GrothendieckTopology.W_adj_unit_app, sheafToPresheaf_obj, sheafToPresheaf_map, typeEquiv_unitIso_hom_app, fullyFaithfulSheafToPresheaf_preimage_val, 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, typeEquiv_counitIso_inv_app_val_app, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, isSheaf_pointwiseColimit, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_val_app, Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf, instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, plusPlusAdjunction_counit_app_val, Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits, sheafificationAdjunction_unit_app, typeEquiv_counitIso_hom_app_val_app, instFaithfulSheafFunctorOppositeSheafToPresheaf, instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf, GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, Sheaf.isLocallyInjective_sheafToPresheaf_map_iff, plusPlusAdjunction_unit_app, GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, sheafToPresheaf_η, GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_val_app_down, sheafToPresheaf_ε, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, sheafificationAdjunction_counit_app_val, yoneda'_comp, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, Sheaf.sheafifyCocone_ι_app_val_assoc, sheafToPresheaf_isRightAdjoint, instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, sheafBotEquivalence_counitIso, GrothendieckTopology.W_eq_W_range_sheafToPresheaf_obj, sheafification_reflective, constantSheafAdj_counit_app, sheafSectionsNatIsoEvaluation_hom_app, instFullSheafFunctorOppositeSheafToPresheaf, Sheaf.sheafifyCocone_ι_app_val, sheafSectionsNatIsoEvaluation_inv_app, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, sheafComposeNatTrans_fac, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf 📖	CompOp	4 math math: sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf 📖	CompOp	3 math math: sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fullyFaithfulSheafToPresheaf_preimage_val 📖	mathematical	—	Sheaf.Hom.val Functor.FullyFaithful.preimage Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf fullyFaithfulSheafToPresheaf	—	—
instFaithfulSheafFunctorOppositeSheafToPresheaf 📖	mathematical	—	Functor.Faithful Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf	—	Functor.FullyFaithful.faithful
instFullSheafFunctorOppositeSheafToPresheaf 📖	mathematical	—	Functor.Full Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf	—	Functor.FullyFaithful.full
instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf 📖	mathematical	—	Functor.ReflectsIsomorphisms Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf	—	Functor.FullyFaithful.reflectsIsomorphisms
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 Sheaf.instCategorySheaf Functor.category sheafBotEquivalence Iso.refl Functor.comp Presheaf.isSheaf_bot 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 Sheaf.instCategorySheaf Functor.category sheafBotEquivalence sheafToPresheaf	—	—
sheafBotEquivalence_inverse_map_val 📖	mathematical	—	Sheaf.Hom.val Bot.bot GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Presheaf.isSheaf_bot Functor.map Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf Equivalence.inverse sheafBotEquivalence	—	Presheaf.isSheaf_bot
sheafBotEquivalence_inverse_obj_val 📖	mathematical	—	Sheaf.val Bot.bot GrothendieckTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Functor.obj Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf 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 Sheaf.instCategorySheaf Functor.category sheafBotEquivalence Iso.refl Functor.id	—	—
sheafOver_val 📖	mathematical	—	Sheaf.val types sheafOver Functor.comp Opposite Category.opposite Functor.obj Functor Functor.category coyoneda Opposite.op	—	—
sheafSectionsNatIsoEvaluation_hom_app 📖	mathematical	—	NatTrans.app Sheaf Sheaf.instCategorySheaf Functor.obj Opposite Category.opposite Functor Functor.category sheafSections Opposite.op Functor.comp sheafToPresheaf evaluation Iso.hom sheafSectionsNatIsoEvaluation CategoryStruct.id Category.toCategoryStruct Sheaf.val	—	—
sheafSectionsNatIsoEvaluation_inv_app 📖	mathematical	—	NatTrans.app Sheaf Sheaf.instCategorySheaf Functor.comp Functor Opposite Category.opposite Functor.category sheafToPresheaf Functor.obj evaluation Opposite.op sheafSections Iso.inv sheafSectionsNatIsoEvaluation CategoryStruct.id Category.toCategoryStruct Sheaf.val	—	—
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app 📖	mathematical	—	Iso.app Sheaf Sheaf.instCategorySheaf types Functor.obj Opposite Category.opposite Functor Functor.category Functor.comp Functor.op sheafToPresheaf coyoneda Functor.whiskeringLeft Opposite.op sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf Equiv.toIso Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Sheaf.val Opposite.unop Equiv.symm Sheaf.homEquiv	—	—
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val 📖	mathematical	—	Sheaf.Hom.val Opposite.unop Sheaf NatTrans.app Sheaf.instCategorySheaf types Functor.obj Opposite Category.opposite Functor Functor.category Functor.comp Functor.op sheafToPresheaf coyoneda Functor.whiskeringLeft Iso.hom sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf	—	—
sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app 📖	mathematical	—	NatTrans.app Sheaf Sheaf.instCategorySheaf types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Functor.comp Functor.op sheafToPresheaf Functor.whiskeringLeft Iso.inv sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf Sheaf.Hom.val Opposite.unop	—	—
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app 📖	mathematical	—	Iso.app Opposite Sheaf Category.opposite Sheaf.instCategorySheaf types Functor.obj Functor Functor.category Functor.comp sheafToPresheaf yoneda Functor.whiskeringLeft Functor.op sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf Opposite.op Equiv.toIso Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Sheaf.val Opposite.unop Equiv.symm Sheaf.homEquiv	—	—
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val 📖	mathematical	—	Sheaf.Hom.val Opposite.unop Sheaf NatTrans.app Opposite Category.opposite Sheaf.instCategorySheaf types Functor.obj Functor Functor.category Functor.comp sheafToPresheaf yoneda Functor.whiskeringLeft Functor.op Iso.hom sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf	—	—
sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app 📖	mathematical	—	NatTrans.app Opposite Sheaf Category.opposite Sheaf.instCategorySheaf types Functor.obj Functor Functor.category yoneda Functor.comp sheafToPresheaf Functor.whiskeringLeft Functor.op Iso.inv sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf Sheaf.Hom.val Opposite.unop	—	—
sheafToPresheaf_map 📖	mathematical	—	Functor.map Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf Sheaf.Hom.val	—	—
sheafToPresheaf_obj 📖	mathematical	—	Functor.obj Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category sheafToPresheaf Sheaf.val	—	—

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	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.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 📖	—	IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	—	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	amalgamateOfArrows	—	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	amalgamateOfArrows	—	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₂	amalgamate 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₂	amalgamate 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.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

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
instCategorySheaf 📖	CompOp	442 math math: cartesianMonoidalCategoryLift_val, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_val_app, CategoryTheory.GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso, CategoryTheory.sheafBotEquivalence_functor, SheafOfModules.pushforward_assoc, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_val_app, CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, ΓHomEquiv_naturality_left_symm, CategoryTheory.isIso_sheafificationAdjunction_counit, isLocallySurjective_sheafToPresheaf_map_iff, CategoryTheory.Functor.sheafPushforwardContinuousIso_inv, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_val_app, CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_val_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_val, LightCondensed.ihomPoints_apply, CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous, CategoryTheory.Equivalence.sheafCongr_functor, CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_val_app, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply, SheafOfModules.pushforwardNatIso_inv, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms, toImage_ι_assoc, CategoryTheory.GrothendieckTopology.overMapPullback_comp_id, CategoryTheory.Functor.sheafPullbackConstruction.instPreservesFiniteLimitsSheafSheafPullback, CategoryTheory.typeEquiv_functor_obj_val_obj, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_val_app, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CondensedMod.isDiscrete_tfae, CategoryTheory.instFullSheafSheafComposeOfFaithful, CategoryTheory.GrothendieckTopology.yoneda_map_val, CompHausLike.LocallyConstant.adjunction_counit, CategoryTheory.sheafificationNatIso_inv_app_val, CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeUliftYoneda, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.discrete_map, CategoryTheory.instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, CategoryTheory.sheafificationNatIso_hom_app_val, CategoryTheory.constantCommuteCompose_hom_app_val, isLocallySurjective_comp, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, CategoryTheory.Equivalence.instPreservesFiniteLimitsFunctorOppositeSheafTransportAndSheafify, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_val_app, isLocallySurjective_iff_epi, CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_functor, CategoryTheory.sheafCompose_map_val, comp_val, LightCondensed.discrete_map, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallySurjectiveHomYonedaGluedToSheafOfIsLocallySurjectiveZariskiTopologyDescFunctorOppositeType, isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, SheafOfModules.toSheaf_obj_val, CategoryTheory.sheafToPresheaf_μ, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, CategoryTheory.Presheaf.isLocallyInjective_presheafToSheaf_map_iff, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality, CategoryTheory.instEpiSheafTypeToImage, CategoryTheory.plusPlusSheaf_obj_val, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val, CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_val_map, mem_essImage_of_isConstant, CategoryTheory.hasLimitsEssentiallySmallSite, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout, CategoryTheory.sheafificationIso_inv_val, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality', instHasColimitsOfShape, CategoryTheory.Functor.sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_val_obj, CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_val, CompHausLike.LocallyConstantModule.functor_map_val, CompHausLike.LocallyConstant.functor_map_val, instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso, CategoryTheory.Functor.sheafPushforwardContinuous_map_val_app, CategoryTheory.HasSheafify.isLeftExact, CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp_assoc, topCatToSheafCompHausLike_map_val_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality', CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions, CategoryTheory.Functor.IsCoverDense.faithful_sheafPushforwardContinuous, CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans, toImage_ι, CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits, CategoryTheory.typeEquiv_inverse_obj, epi_of_isLocallySurjective', CategoryTheory.GrothendieckTopology.W_iff_isIso_map_of_adjunction, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_obj, CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf, ΓHomEquiv_naturality_left, SheafOfModules.pushforwardComp_inv_app_val_app, isConstant_iff_forget, CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_val_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_val, CategoryTheory.instHasImagesSheafType, hasFilteredColimitsOfSize, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, CategoryTheory.GrothendieckTopology.instFullSheafTypeUliftYoneda, SheafOfModules.pushforwardNatTrans_id, CategoryTheory.plusPlusSheaf_map_val, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left, CategoryTheory.equivYoneda'_inv_val, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_val_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_val_map, CategoryTheory.GrothendieckTopology.W_adj_unit_app, instHasFunctorialFactorizationLocallySurjectiveLocallyInjective, CategoryTheory.sheafToPresheaf_obj, CategoryTheory.sheafToPresheaf_map, isLocallySurjective_iff_epi', SheafOfModules.instAdditiveSheafAddCommGrpCatToSheaf, CategoryTheory.typeEquiv_unitIso_hom_app, CompHausLike.LocallyConstant.functor_obj_val, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_map, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, cartesianMonoidalCategorySnd_val, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_val_app, CategoryTheory.fullyFaithfulSheafToPresheaf_preimage_val, CategoryTheory.SheafOfTypes.finitary_extensive, instIsGrothendieckAbelian, natTransΓRes_app, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality', CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, SheafOfModules.Presentation.quasicoherentData_presentation, CompHausLike.LocallyConstantModule.functor_obj_val, SheafOfModules.toSheaf_map_val, CategoryTheory.instIsRightAdjointSheafΓ, CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, CategoryTheory.GrothendieckTopology.overMapPullback_assoc_assoc, isSheaf_of_isLimit, instHasFiniteColimits, CategoryTheory.sheafToPresheaf_δ, Hom.mono_iff_presheaf_mono, CategoryTheory.sheafBotEquivalence_inverse_map_val, CategoryTheory.typeEquiv_unitIso_inv_app, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, CategoryTheory.isRegularEpiCategory_sheaf, CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app, CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp, PresheafOfModules.sheafification_map, CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app, CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_hom_app_app, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf, SheafOfModules.pullback_comp_id, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_val_obj, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', CategoryTheory.sheafBotEquivalence_unitIso, SheafOfModules.instPreservesFiniteLimitsFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, CategoryTheory.typeEquiv_counitIso_inv_app_val_app, CategoryTheory.sheafBotEquivalence_inverse_obj_val, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, CategoryTheory.isSheaf_pointwiseColimit, topCatToSheafCompHausLike_obj, CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_obj, adjunction_counit_app_val, CategoryTheory.SheafOfTypes.adhesive, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, isSeparating, isGrothendieckAbelian_of_essentiallySmall, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map, CategoryTheory.Functor.IsDenseSubsite.sheafEquiv_inverse, ΓObjEquivSections_naturality_symm, mono_of_isLocallyInjective, ΓRes_map_assoc, CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_map, ab5ofSize, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, ΓObjEquivHom_naturality_symm, CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf, CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_val_app, hasSeparator, CategoryTheory.instFaithfulSheafSheafCompose, SheafOfModules.conjugateEquiv_pullbackComp_inv, CategoryTheory.typeEquiv_functor_obj_val_map, Hom.mono_of_presheaf_mono, instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_val, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, instHasFiniteLimits, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_val_app, CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_val_app, CategoryTheory.instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify, CompHausLike.LocallyConstant.adjunction_left_triangle, isLocallyInjective_forget, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf, SheafOfModules.pullback_id_comp, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_val_app, CategoryTheory.instReflectsIsomorphismsSheafSheafCompose, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc, CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfSizeSheafSheafFiberOfHasSheafifyOfWEqualsLocallyBijectiveOfReflectsIsomorphismsOfPreservesFilteredColimitsOfSizeForgetOfLocallySmall, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_val_app, CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, coneΓ_pt, CategoryTheory.Equivalence.sheafCongr.functor_map_val_app, CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_val_app, CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf, CategoryTheory.instPreservesColimitsOfShapeSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreservesFiniteProductsColim, CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_obj, isConstant_iff_isIso_counit_app', CategoryTheory.SheafOfTypes.balanced, CategoryTheory.preservesFiniteLimits_presheafToSheaf, CategoryTheory.typeEquiv_inverse_map, SheafOfModules.pushforward_map_val, CategoryTheory.plusPlusAdjunction_counit_app_val, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_eq_eqToIso, CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, SheafOfModules.pushforwardComp_hom_app_val_app, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, adjunction_unit_app_val, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_val_app, CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_val_app, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, CategoryTheory.Equivalence.sheafCongr_counitIso, AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf, CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility, ΓHomEquiv_naturality_right_symm, CategoryTheory.Equivalence.sheafCongr.functor_obj_val_map, CategoryTheory.GrothendieckTopology.preservesLimitsOfSize_yoneda, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_val_app, ΓObjEquivHom_naturality, ΓRes_map, SheafOfModules.pushforwardCongr_symm, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv', AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, cartesianMonoidalCategoryWhiskerRight_val, SheafOfModules.instFaithfulSheafAddCommGrpCatToSheaf, CondensedSet.isDiscrete_tfae, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, instHasLimitsOfShape, CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso, CategoryTheory.GrothendieckTopology.overMapPullback_comp_id_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, CategoryTheory.plusPlusSheaf_preservesZeroMorphisms, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.GrothendieckTopology.yoneda_obj_val, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_val, isConstant_iff_mem_essImage, instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality, CategoryTheory.sheafificationAdjunction_unit_app, CategoryTheory.typeEquiv_counitIso_hom_app_val_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso, CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf, AlgebraicGeometry.Scheme.LocalRepresentability.instIsLocallyInjectiveHomYonedaGluedToSheaf, CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf, CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_id, instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv', SheafOfModules.unitToPushforwardObjUnit_val_app_apply, SheafOfModules.pullback_assoc, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply, CategoryTheory.Functor.IsCoverDense.sheafIso_inv_val, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.presheafToSheaf_additive, LightCondensed.ihomPoints_symm_apply, CategoryTheory.sheafificationIso_hom_val, LightCondensed.discrete_obj, Hom.epi_of_presheaf_epi, isLocallyInjective_sheafToPresheaf_map_iff, id_val, CategoryTheory.Functor.sheafPullbackConstruction.preservesFiniteLimits, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_val_app, isConstant_iff_of_equivalence, hasExactColimitsOfShape, CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app, instHasFiniteCoproducts, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_val, CategoryTheory.yoneda'_obj_val, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda, instIsLocallySurjectiveHomMapTypeSheafComposeForget, CategoryTheory.plusPlusAdjunction_unit_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_val_map, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_val_app, mono_of_injective, CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, epi_of_isLocallySurjective, CategoryTheory.sheafToPresheaf_η, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_val_obj, CompHausLike.LocallyConstant.counit_app_val, instHasColimitsOfSize, SheafOfModules.pushforwardNatTrans_app_val_app, CategoryTheory.GrothendieckTopology.W_iff, CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction, CategoryTheory.typeEquiv_functor_map_val_app, CategoryTheory.Functor.sheafPushforwardContinuousIso_hom, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality, CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_map, cartesianMonoidalCategoryFst_val, ΓHomEquiv_naturality_right, instIsLeftAdjointComposeAndSheafify, isSeparator, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_val_app_down, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, isLocallyBijective_iff_isIso, CategoryTheory.instIsConstantObjSheafSheafCompose, CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify, CategoryTheory.sheafToPresheaf_ε, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, CategoryTheory.sheafificationAdjunction_counit_app_val, CategoryTheory.preservesLimitsOfShape_presheafToSheaf, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_val_app, CategoryTheory.hasColimitsEssentiallySmallSite, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, SheafOfModules.pushforward_comp_id, CategoryTheory.Equivalence.sheafCongr_inverse, CategoryTheory.GrothendieckTopology.overMapPullback_id_comp_assoc, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, CategoryTheory.constantSheafAdj_counit_w, CategoryTheory.sheafCompose_id, CompHausLike.LocallyConstant.unit_app, comp_val_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, CategoryTheory.yoneda'_comp, SheafOfModules.forgetToSheafModuleCat_map_val, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, PresheafOfModules.instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf, sheafifyCocone_ι_app_val_assoc, SheafOfModules.conjugateEquiv_pullbackId_hom, Hom.add_app, hasLimitsOfSize, CategoryTheory.Equivalence.sheafCongr.inverse_map_val_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_map, CategoryTheory.equivYoneda'_hom_val, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_val_app, CategoryTheory.sheafToPresheaf_isRightAdjoint, CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_val_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, SheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf, CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj, CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, instIsRightAdjointSheafComposeOfHasWeakSheafify, SheafOfModules.pushforwardNatTrans_app_val_app_apply, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf, CategoryTheory.instIsRegularEpiCategorySheafTypeOfHasSheafify, SheafOfModules.pushforward_id_comp, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, CategoryTheory.sheafBotEquivalence_counitIso, CategoryTheory.GrothendieckTopology.W_eq_W_range_sheafToPresheaf_obj, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_val_app, CategoryTheory.sheafification_reflective, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app, CategoryTheory.Equivalence.sheafCongr.functor_obj_val_obj, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_val_app, CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_val_app, CategoryTheory.GrothendieckTopology.map_yonedaEquiv, isLocallySurjective_iff_isIso, CategoryTheory.GrothendieckTopology.overMapPullback_assoc, ΓObjEquivSections_naturality, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_val, CategoryTheory.constantSheafAdj_counit_app, CategoryTheory.sheafSectionsNatIsoEvaluation_hom_app, SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat, CategoryTheory.GrothendieckTopology.overMapPullback_id_comp, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_val_obj, CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_val_app, CategoryTheory.Functor.IsCoverDense.sheafIso_hom_val, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, CategoryTheory.instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf, isConstant_iff_isIso_counit_app, SheafOfModules.forgetToSheafModuleCat_obj_val, CategoryTheory.yoneda'_map_val, CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_val_map_down, cartesianMonoidalCategoryWhiskerLeft_val, ΓRes_naturality, SheafOfModules.pushforwardNatIso_hom, CategoryTheory.Equivalence.sheafCongr_unitIso, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, sheafifyCocone_ι_app_val, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, CategoryTheory.Functor.IsDenseSubsite.full_sheafPushforwardContinuous, CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_val_app, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_val_app, CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_val_app, CategoryTheory.sheafSectionsNatIsoEvaluation_inv_app, IsConstant.mem_essImage, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val, SheafOfModules.pushforward_obj_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app, CategoryTheory.GrothendieckTopology.uliftYoneda_map_val_app_down, CategoryTheory.sheafCompose_obj_val, instHasFiniteProducts, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, Condensed.discrete_obj, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp, CategoryTheory.sheafComposeNatTrans_fac, CategoryTheory.GrothendieckTopology.yonedaEquiv_apply, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right, CompHausLike.LocallyConstant.adjunction_unit, CategoryTheory.Functor.IsDenseSubsite.faithful_sheafPushforwardContinuous, CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff, SheafOfModules.pushforwardNatTrans_comp, instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf, CategoryTheory.instMonoSheafTypeImageι, CategoryTheory.Functor.IsCoverDense.full_sheafPushforwardContinuous, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact, CategoryTheory.sheafCompose_comp
instInhabitedHom 📖	CompOp	—
isTerminalOfBotCover 📖	CompOp	—
val 📖	CompOp	477 math math: CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac, cartesianMonoidalCategoryLift_val, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_val_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_val_app, ΓHomEquiv_naturality_left_symm, CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_val_app, TopCat.Sheaf.interUnionPullbackCone_snd, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafOfModulesToPresheafOfModules, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_val_app, CategoryTheory.sheafOver_val, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_id, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_val, LightCondensed.ihomPoints_apply, CategoryTheory.eval_app, AlgebraicGeometry.StructureSheaf.comap_id, PresheafOfModules.instIsLocallySurjectiveToSheafify, CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_val_app, condensedSetToTopCat_obj_carrier, AlgebraicGeometry.StructureSheaf.const_mul_rev, Condensed.hom_ext_iff, CategoryTheory.ran_isSheaf_of_isCocontinuous, LightCondensed.forget_obj_val_map, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply, AlgebraicGeometry.StructureSheaf.comap_comp, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply, PresheafOfModules.Sheafify.add_smul, SheafOfModules.instFullPresheafOfModulesValRingCatForget, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map, AlgebraicGeometry.StructureSheaf.const_self, LightCondensed.ihomPoints_symm_comp, CategoryTheory.typeEquiv_functor_obj_val_obj, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_val_app, AlgebraicGeometry.Proj.pow_apply, CategoryTheory.instPreservesFiniteProductsOppositeVal, AlgebraicGeometry.Spec_presheaf, LightCondSet.continuous_coinducingCoprod, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, AlgebraicGeometry.Proj.mul_apply, AlgebraicGeometry.StructureSheaf.comap_id', CondensedSet.hom_naturality_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm_assoc, CategoryTheory.sheafificationNatIso_inv_app_val, AlgebraicGeometry.StructureSheaf.const_add, PresheafOfModules.toSheafify_app_apply', CategoryTheory.instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, CategoryTheory.sheafificationNatIso_hom_app_val, AlgebraicGeometry.structureSheafInType.mul_apply, AlgebraicGeometry.StructureSheaf.exists_const, TopCat.Sheaf.pushforward_map, CategoryTheory.Functor.IsCoverDense.isoOver_hom_app, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.structurePresheafInCommRing_obj_carrier, smoothSheaf.ι_evalHom_apply, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_app_app, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_val_app, TopCat.toSheafCompHausLike_val_obj, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf', TopCat.Sheaf.interUnionPullbackCone_fst, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, CategoryTheory.sheafCompose_map_val, comp_val, SheafOfModules.evaluationPreservesLimitsOfShape, isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, SheafOfModules.toSheaf_obj_val, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc, AlgebraicGeometry.Proj.one_apply, Condensed.epi_iff_surjective_on_stonean, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, CategoryTheory.plusPlusSheaf_obj_val, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_val_map, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map, CategoryTheory.Functor.IsCoverDense.Types.appHom_valid_glue, PresheafOfModules.toPresheaf_map_toSheafify, LightCondSet.topCatAdjunctionUnit_val_app_apply, TopCat.Sheaf.id_app, AlgebraicGeometry.StructureSheaf.comap_const, CategoryTheory.sheafificationIso_inv_val, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality', CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_of_sheaf, AlgebraicGeometry.Proj.sub_apply, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_assoc, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def, AlgebraicGeometry.instIsScalarTowerObjOppositeOpensCarrierTopValStructureSheafInType, Condensed.isSheafStonean, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_map, smoothSheaf.ι_evalHom_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, CategoryTheory.Functor.IsCoverDense.sheafHom_eq, AlgebraicGeometry.StructureSheaf.comap_apply, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_val_obj, CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_val, SheafOfModules.evaluationPreservesLimitsOfSize, Condensed.instPreservesFiniteProductsOppositeCompHausVal, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm, CategoryTheory.Functor.sheafPushforwardContinuous_map_val_app, topCatToSheafCompHausLike_map_val_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality', AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom_apply, AlgebraicGeometry.Scheme.ΓSpecIso_inv, tensorProd_isSheaf, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction_assoc, SheafOfModules.isSheaf, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left, AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app', imageι_val, CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq, CategoryTheory.typeEquiv_inverse_obj, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_obj, ΓHomEquiv_naturality_left, SheafOfModules.pushforwardComp_inv_app_val_app, CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_val_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_val, TopCat.Sheaf.extend_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, CategoryTheory.presheaf_mono_of_mono, SheafOfModules.restrictScalars_obj_val, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_left, CategoryTheory.equivYoneda'_inv_val, SheafOfModules.instReflectsIsomorphismsPresheafOfModulesValRingCatForget, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_val_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_obj_val_map, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc, AlgebraicGeometry.StructureSheaf.algebraMap_self_map, CategoryTheory.sheafToPresheaf_obj, CondensedMod.epi_iff_surjective_on_stonean, CompHausLike.LocallyConstant.functor_obj_val, CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_val_map, AlgebraicGeometry.Spec.map_appLE, cartesianMonoidalCategorySnd_val, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, CondensedSet.epi_iff_surjective_on_stonean, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_val_app, toImage_val, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_assoc, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, SheafOfModules.instFaithfulPresheafOfModulesValRingCatForget, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality', CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, CategoryTheory.Functor.IsCoverDense.presheafIso_hom_app, Condensed.instPreservesFiniteProductsOppositeProfiniteVal, AlgebraicGeometry.StructureSheaf.const_mul_cancel, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map, CompHausLike.LocallyConstantModule.functor_obj_val, SheafOfModules.pushforwardCongr_hom_app_val_app, SheafOfModules.toSheaf_map_val, AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, Hom.mono_iff_presheaf_mono, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_inv_app_app, CondensedSet.topCatAdjunctionUnit_val_app_apply, CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app, TopCat.Presheaf.stalk_mono_of_mono, TopCat.Sheaf.interUnionPullbackConeLift_right, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_val_obj, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', AlgebraicGeometry.StructureSheaf.const_one, AlgebraicGeometry.StructureSheaf.globalSectionsIso_hom, CategoryTheory.typeEquiv_counitIso_inv_app_val_app, LightCondensed.forget_map_val_app, Condensed.comp_val, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, CategoryTheory.sheafBotEquivalence_inverse_obj_val, CondensedMod.hom_naturality_apply, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, AlgebraicGeometry.StructureSheaf.smul_const, AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app', Condensed.epi_iff_locallySurjective_on_compHaus, CategoryTheory.Functor.op_comp_isSheaf_of_types, CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_obj, adjunction_counit_app_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, SheafOfModules.id_val, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict, cond, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map, ΓObjEquivSections_naturality_symm, isLocallyInjective_iff_injective, AlgebraicGeometry.StructureSheaf.const_zero, ΓRes_map_assoc, CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_map, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_compatible, TopCat.Sheaf.comp_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, SheafOfModules.pushforwardCongr_inv_app_val_app, CategoryTheory.Functor.IsCoverDense.Types.appIso_inv, PresheafOfModules.Sheafify.smul_add, CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_val_app, AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app, CategoryTheory.typeEquiv_functor_obj_val_map, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_val, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_app_app, TopCat.subsheafToTypes_val, CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_val_app, LightCondensed.ofSheafForgetLightProfinite_val, CompHausLike.LocallyConstant.adjunction_left_triangle, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, CategoryTheory.extensiveTopology.isLocallySurjective_iff, TopCat.Sheaf.pushforward_obj_val, SheafOfModules.fullyFaithfulForget_preimage_val, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_val_app, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_assoc, SheafOfModules.restrictScalars_map_val, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_val_app, coneΓ_pt, CategoryTheory.Equivalence.sheafCongr.functor_map_val_app, CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_val_app, CondensedSet.continuous_coinducingCoprod, AlgebraicGeometry.Proj.zero_apply, CategoryTheory.Functor.sheafPushforwardContinuous_obj_val_obj, CategoryTheory.Functor.IsCoverDense.Types.presheafIso_inv_app, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, AlgebraicGeometry.StructureSheaf.const_algebraMap, CategoryTheory.typeEquiv_inverse_map, SheafOfModules.pushforward_map_val, CategoryTheory.plusPlusAdjunction_counit_app_val, SheafOfModules.pushforwardComp_hom_app_val_app, SheafOfModules.unit_val, SheafOfModules.Presentation.map_relations_I, adjunction_unit_app_val, TopCat.Sheaf.interUnionPullbackConeLift_left, CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_val_app, SheafOfModules.Presentation.mapRelations_mapGenerators, CondensedSet.topCatAdjunctionUnit_val_app, CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_val_app, LightCondensed.hom_ext_iff, SheafOfModules.relationsOfIsCokernelFree_I, AlgebraicGeometry.structureSheafInType.add_apply, LightCondensed.underlying_obj, CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility, ΓHomEquiv_naturality_right_symm, CategoryTheory.Functor.IsCoverDense.Types.naturality_apply, CategoryTheory.Equivalence.sheafCongr.functor_obj_val_map, coneΓ_π_app, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_val_app, ΓRes_map, LightCondSet.hom_naturality_apply, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv', SheafOfModules.add_val, cartesianMonoidalCategoryWhiskerRight_val, AlgebraicGeometry.Proj.add_apply, AlgebraicGeometry.stalkMap_toStalk_apply, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, CategoryTheory.Functor.IsCoverDense.presheafIso_inv, CategoryTheory.GrothendieckTopology.yoneda_obj_val, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_val, AlgebraicGeometry.StructureSheaf.comapₗ_const, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality, CategoryTheory.typeEquiv_counitIso_hom_app_val_app, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map_assoc, AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc, AlgebraicGeometry.StructureSheaf.res_apply, LightCondensed.equalizerCondition, CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal, LightCondMod.hom_naturality_apply, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv', SheafOfModules.unitToPushforwardObjUnit_val_app_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply, CategoryTheory.Functor.IsCoverDense.sheafIso_inv_val, SheafOfModules.forget_map, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, LightCondensed.ihomPoints_symm_apply, CategoryTheory.sheafificationIso_hom_val, SheafOfModules.forgetPreservesLimitsOfSize, id_val, CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_left, AlgebraicGeometry.StructureSheaf.algebraMap_germ, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_val_app, CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_val, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction, CategoryTheory.yoneda'_obj_val, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, AlgebraicGeometry.StructureSheaf.const_mul_cancel', CategoryTheory.Functor.IsCoverDense.homOver_app, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_obj_val_map, lightCondSetToTopCat_obj_carrier, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_val_app, SheafOfModules.Finite.forgetPreservesFiniteLimits, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app, SheafOfModules.forget_obj, CategoryTheory.Functor.IsCoverDense.Types.presheafIso_hom_app, CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, SheafOfModules.comp_val_assoc, LightCondensed.ihom_map_val_app, CategoryTheory.Functor.IsDenseSubsite.mapPreimage_of_eq, AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective, AlgebraicGeometry.StructureSheaf.comap_id_eq_map, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_obj_val_obj, CompHausLike.LocallyConstant.counit_app_val, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext_iff, Condensed.instPreservesFiniteProductsOppositeStoneanVal, SheafOfModules.pushforwardNatTrans_app_val_app, PresheafOfModules.Sheafify.one_smul, CondensedMod.epi_iff_locallySurjective_on_compHaus, AlgebraicGeometry.ΓSpec.toSpecΓ_of, TopCat.toSheafCompHausLike_val_map, CategoryTheory.Functor.IsCoverDense.Types.presheafHom_app, AlgebraicGeometry.StructureSheaf.toOpen_germ, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_naturality, CategoryTheory.Equivalence.sheafCongr.inverse_obj_val_map, cartesianMonoidalCategoryFst_val, ΓHomEquiv_naturality_right, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf_map', CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_val_app_down, AlgebraicGeometry.Scheme.Modules.instFullPresheafOfModulesToPresheafOfModules, CategoryTheory.Functor.IsCoverDense.isoOver_inv_app, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, smoothSheaf.ι_evalHom, AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc, AlgebraicGeometry.StructureSheaf.toOpenₗ_eq_const, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app, CategoryTheory.sheafificationAdjunction_counit_app_val, AlgebraicGeometry.StructureSheaf.res_const, CategoryTheory.Functor.op_comp_isSheaf, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_val_app, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, SheafOfModules.relationsOfIsCokernelFree_s, CategoryTheory.constantSheafAdj_counit_w, comp_val_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, SheafOfModules.forgetToSheafModuleCat_map_val, LightCondSet.topCatAdjunctionUnit_val_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, Condensed.underlying_obj, sheafifyCocone_ι_app_val_assoc, Hom.add_app, AlgebraicGeometry.tilde.toOpen_map_app_assoc, CategoryTheory.Equivalence.sheafCongr.inverse_map_val_app, CategoryTheory.Functor.IsDenseSubsite.map_eq_of_eq, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_map, CategoryTheory.equivYoneda'_hom_val, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_val_app, LightCondensed.id_val, PresheafOfModules.Sheafify.zero_smul, CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_val_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, PresheafOfModules.sheafificationAdjunction_homEquiv_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left, AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app, SheafOfModules.forgetPreservesLimitsOfShape, SheafOfModules.Presentation.IsFinite.finite_relations, SheafOfModules.pushforwardNatTrans_app_val_app_apply, SheafOfModules.comp_val, AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf, CategoryTheory.Functor.IsContinuous.op_comp_isSheaf_of_types, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, CondensedSet.toTopCatMap_hom_apply, AlgebraicGeometry.structurePresheafInCommRingCat_obj_carrier, CategoryTheory.Functor.IsCoverDense.Types.appIso_hom, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc, LightCondensed.comp_val, PresheafOfModules.instIsLocallyInjectiveToSheafify, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_val_app, AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules, CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply, TopCat.Sheaf.eq_of_locally_eq_iff, LightCondensed.underlying_map, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app, Condensed.underlying_map, CategoryTheory.Equivalence.sheafCongr.functor_obj_val_obj, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_val_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite, AlgebraicGeometry.Proj.res_apply, TopCat.Presheaf.app_injective_iff_stalkFunctor_map_injective, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_val_app, SheafOfModules.pushforwardSections_coe, CategoryTheory.GrothendieckTopology.map_yonedaEquiv, PresheafOfModules.Sheafify.smul_zero, PresheafOfModules.Sheafify.map_smul, AlgebraicGeometry.StructureSheaf.toOpen_res, CategoryTheory.coherentTopology.isLocallySurjective_iff, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, ΓObjEquivSections_naturality, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, LightCondSet.toTopCatMap_hom_apply, CondensedSet.epi_iff_locallySurjective_on_compHaus, AlgebraicGeometry.StructureSheaf.const_mul, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_val, CategoryTheory.constantSheafAdj_counit_app, PresheafOfModules.toSheafify_app_apply, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, TopCat.Sheaf.interUnionPullbackCone_pt, CategoryTheory.sheafSectionsNatIsoEvaluation_hom_app, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_yonedaULift_map, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_val_obj, CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_val_app, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map, CategoryTheory.Functor.IsCoverDense.sheafIso_hom_val, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, SheafOfModules.forgetToSheafModuleCat_obj_val, CategoryTheory.GrothendieckTopology.uliftYoneda_obj_val_map_down, cartesianMonoidalCategoryWhiskerLeft_val, ΓRes_naturality, AlgebraicGeometry.structureSheafInType.smul_apply, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, Condensed.isSheafProfinite, CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac, isSeparated, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right, Condensed.id_val, TopCat.Presheaf.mono_iff_stalk_mono, CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_val_app, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_val_app, CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_val_app, CategoryTheory.sheafSectionsNatIsoEvaluation_inv_app, AlgebraicGeometry.StructureSheaf.algebraMap_germ_apply, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val, SheafOfModules.pushforward_obj_val, Condensed.equalizerCondition_profinite, PresheafOfModules.Sheafify.mul_smul, CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app, CategoryTheory.GrothendieckTopology.uliftYoneda_map_val_app_down, Condensed.equalizerCondition, CategoryTheory.sheafCompose_obj_val, LightCondensed.ofSheafLightProfinite_val, CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp, CategoryTheory.GrothendieckTopology.yonedaEquiv_apply, SheafOfModules.Finite.evaluationPreservesFiniteLimits, SheafOfModules.instAdditivePresheafOfModulesValRingCatForget, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, AlgebraicGeometry.ΓSpec.toSpecΓ_unop, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm, CategoryTheory.Pseudofunctor.sheafHom_val, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, CategoryTheory.Functor.IsCoverDense.Types.naturality_assoc, AlgebraicGeometry.Spec.sheafedSpaceObj_presheaf, AlgebraicGeometry.Spec.map_app, SheafOfModules.unitHomEquiv_apply_coe, image_val, AlgebraicGeometry.tilde.toOpen_map_app, CategoryTheory.Functor.IsCoverDense.Types.naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_val 📖	mathematical	—	Hom.val CategoryTheory.CategoryStruct.comp CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct instCategorySheaf CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category val	—	—
comp_val_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category val Hom.val CategoryTheory.Sheaf instCategorySheaf	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_val
cond 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf val	—	—
hom_ext 📖	—	Hom.val	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.val	—	hom_ext
id_val 📖	mathematical	—	Hom.val CategoryTheory.CategoryStruct.id CategoryTheory.Sheaf CategoryTheory.Category.toCategoryStruct instCategorySheaf CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category val	—	—

CategoryTheory.Sheaf.Hom

Definitions

Name	Category	Theorems
addCommGroup 📖	CompOp	—
val 📖	CompOp	192 math math: CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_val_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_hom_app_val_app, CategoryTheory.Equivalence.sheafCongr.counitIso_hom_app_val_app, CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_inv_app_val_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_map_val, CategoryTheory.eval_app, CategoryTheory.Functor.sheafPushforwardContinuousComp'_inv_app_val_app, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, Condensed.hom_ext_iff, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_val_app, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CategoryTheory.GrothendieckTopology.yoneda_map_val, CondensedSet.hom_naturality_apply, CategoryTheory.sheafificationNatIso_inv_app_val, CategoryTheory.instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf_inv_app_app, CategoryTheory.sheafificationNatIso_hom_app_val, CategoryTheory.constantCommuteCompose_hom_app_val, TopCat.Sheaf.pushforward_map, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_val_app, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, CategoryTheory.sheafCompose_map_val, CategoryTheory.Sheaf.comp_val, Condensed.epi_iff_surjective_on_stonean, CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_val, CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val, LightCondSet.topCatAdjunctionUnit_val_app_apply, TopCat.Sheaf.id_app, CategoryTheory.sheafificationIso_inv_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, CategoryTheory.Functor.sheafPushforwardContinuousNatTrans_app_val, CompHausLike.LocallyConstantModule.functor_map_val, CompHausLike.LocallyConstant.functor_map_val, CategoryTheory.Presheaf.coherentExtensiveEquivalence_counitIso, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm, CategoryTheory.Functor.sheafPushforwardContinuous_map_val_app, topCatToSheafCompHausLike_map_val_app, CategoryTheory.Sheaf.imageι_val, CategoryTheory.Equivalence.sheafCongrPreregular_functor_map_val_app, CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_map_val, CategoryTheory.presheaf_mono_of_mono, CategoryTheory.plusPlusSheaf_map_val, SheafOfModules.restrictScalars_obj_val, CategoryTheory.equivYoneda'_inv_val, CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_val_app, CategoryTheory.sheafToPresheaf_map, CondensedMod.epi_iff_surjective_on_stonean, CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_naturality_right, CondensedSet.epi_iff_surjective_on_stonean, CategoryTheory.Equivalence.sheafCongrPrecoherent_inverse_map_val_app, CategoryTheory.Sheaf.toImage_val, CategoryTheory.fullyFaithfulSheafToPresheaf_preimage_val, SheafOfModules.toSheaf_map_val, mono_iff_presheaf_mono, CategoryTheory.sheafBotEquivalence_inverse_map_val, CondensedSet.topCatAdjunctionUnit_val_app_apply, TopCat.Presheaf.stalk_mono_of_mono, CategoryTheory.GrothendieckTopology.map_yonedaEquiv', CategoryTheory.typeEquiv_counitIso_inv_app_val_app, LightCondensed.forget_map_val_app, Condensed.comp_val, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, CondensedMod.hom_naturality_apply, Condensed.epi_iff_locallySurjective_on_compHaus, CategoryTheory.Sheaf.adjunction_counit_app_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, CategoryTheory.Sheaf.ΓObjEquivSections_naturality_symm, CategoryTheory.Sheaf.isLocallyInjective_iff_injective, TopCat.Sheaf.comp_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply, CategoryTheory.Equivalence.sheafCongr.unitIso_hom_app_val_app, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_hom_val, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_val_app, CategoryTheory.Functor.sheafPushforwardContinuousComp_inv_app_val_app, CompHausLike.LocallyConstant.adjunction_left_triangle, CategoryTheory.extensiveTopology.isLocallySurjective_iff, CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_val_app, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_assoc, SheafOfModules.restrictScalars_map_val, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf_assoc, CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_val_app, CategoryTheory.Equivalence.sheafCongr.functor_map_val_app, CategoryTheory.Functor.sheafPushforwardContinuousComp_hom_app_val_app, CategoryTheory.typeEquiv_inverse_map, SheafOfModules.pushforward_map_val, CategoryTheory.plusPlusAdjunction_counit_app_val, CategoryTheory.Sheaf.adjunction_unit_app_val, CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_val_app, CondensedSet.topCatAdjunctionUnit_val_app, CategoryTheory.Functor.sheafPushforwardContinuousId'_inv_app_val_app, LightCondensed.hom_ext_iff, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right_symm, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_inv_app_val_app, LightCondSet.hom_naturality_apply, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv', AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_val, CategoryTheory.typeEquiv_counitIso_hom_app_val_app, LightCondMod.hom_naturality_apply, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv', SheafOfModules.unitToPushforwardObjUnit_val_app_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply, CategoryTheory.Functor.IsCoverDense.sheafIso_inv_val, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, CategoryTheory.sheafificationIso_hom_val, CategoryTheory.Sheaf.id_val, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_val_app, CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_val_app, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, CompHausLike.LocallyConstant.counit_app_val, CondensedMod.epi_iff_locallySurjective_on_compHaus, CategoryTheory.typeEquiv_functor_map_val_app, CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val, CategoryTheory.Sheaf.ΓHomEquiv_naturality_right, CategoryTheory.GrothendieckTopology.map_uliftYonedaEquiv, CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_inv_app_val_app_down, CategoryTheory.sheafificationAdjunction_counit_app_val, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_comp, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_comp, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_val_app, CategoryTheory.Sheaf.comp_val_assoc, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, SheafOfModules.forgetToSheafModuleCat_map_val, LightCondSet.topCatAdjunctionUnit_val_app, CategoryTheory.GrothendieckTopology.yonedaULiftEquiv_symm_app_apply, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val_assoc, add_app, AlgebraicGeometry.tilde.toOpen_map_app_assoc, CategoryTheory.Equivalence.sheafCongr.inverse_map_val_app, CategoryTheory.equivYoneda'_hom_val, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_val_app, LightCondensed.id_val, CategoryTheory.Sheaf.hom_ext_iff, CategoryTheory.Functor.sheafPushforwardContinuousId_inv_app_val_app, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_naturality_right, CondensedSet.toTopCatMap_hom_apply, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right_symm_assoc, LightCondensed.comp_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, CategoryTheory.Equivalence.sheafCongrPrecoherent_functor_map_val_app, LightCondensed.underlying_map, Condensed.underlying_map, CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_inv_app_val_app, CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_val_app, CategoryTheory.GrothendieckTopology.map_yonedaEquiv, CategoryTheory.coherentTopology.isLocallySurjective_iff, CategoryTheory.Sheaf.ΓObjEquivSections_naturality, LightCondSet.toTopCatMap_hom_apply, CondensedSet.epi_iff_locallySurjective_on_compHaus, TopCat.Presheaf.isIso_iff_stalkFunctor_map_iso, CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val, CategoryTheory.Functor.sheafPushforwardContinuousId'_hom_app_val_app, CategoryTheory.Functor.IsCoverDense.sheafIso_hom_val, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, CategoryTheory.yoneda'_map_val, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, CategoryTheory.Sheaf.ΓRes_naturality, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, CategoryTheory.Sheaf.sheafifyCocone_ι_app_val, CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right, Condensed.id_val, TopCat.Presheaf.mono_iff_stalk_mono, CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_val_app, CategoryTheory.GrothendieckTopology.map_yonedaULiftEquiv, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_val_app, CategoryTheory.Equivalence.sheafCongr.counitIso_inv_app_val_app, CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val, SheafOfModules.pushforward_obj_val, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf_app_toGlued, CategoryTheory.GrothendieckTopology.uliftYoneda_map_val_app_down, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp, CategoryTheory.GrothendieckTopology.yonedaEquiv_apply, CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_right, ext_iff, CategoryTheory.Sheaf.image_val, AlgebraicGeometry.tilde.toOpen_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val val Quiver.Hom CategoryTheory.Sheaf CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.instAddHomSheaf CategoryTheory.Functor.obj AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	—
epi_of_presheaf_epi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits CategoryTheory.Limits.fullyFaithful_reflectsColimits CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf
ext 📖	—	val	—	—	—
ext_iff 📖	mathematical	—	val	—	ext
mono_of_presheaf_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf	—	CategoryTheory.Functor.mono_of_mono_map CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf

---

← Back to Index