Whiskering

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

Statistics

Metric	Count
Definitions mapMultifork, multicospanComp, HasSheafCompose, fullyFaithfulSheafCompose, fullyFaithfulSheafComposeCompSheafToPresheaf, sheafCompose, sheafCompose_map	7
Theorems multicospanComp_hom_app, multicospanComp_inv_app, isSheaf, isSeparated, isSeparated, hasSheafCompose_of_preservesLimitsOfSize, hasSheafCompose_of_preservesMulticospan, instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf, instFaithfulSheafSheafCompose, instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, instFullSheafSheafComposeOfFaithful, instReflectsIsomorphismsSheafSheafCompose, sheafCompose_comp, sheafCompose_id, sheafCompose_map_val, sheafCompose_obj_val	16
Total	23

CategoryTheory

Definitions

Name	Category	Theorems
fullyFaithfulSheafCompose 📖	CompOp	—
fullyFaithfulSheafComposeCompSheafToPresheaf 📖	CompOp	—
sheafCompose 📖	CompOp	29 math math: instFullSheafSheafComposeOfFaithful, constantCommuteCompose_hom_app_val, sheafCompose_map_val, instIsIsoFunctorOppositeSheafSheafComposeNatTrans, Sheaf.isConstant_iff_forget, GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, Sheaf.adjunction_counit_app_val, instFaithfulSheafSheafCompose, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, Sheaf.isLocallyInjective_forget, instReflectsIsomorphismsSheafSheafCompose, GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, Sheaf.adjunction_unit_app_val, instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf, GrothendieckTopology.uliftYonedaOpCompCoyoneda_hom_app_app_down, Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget, instIsConstantObjSheafSheafCompose, constantSheafAdj_counit_w, sheafCompose_id, instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful, GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify, GrothendieckTopology.Point.sheafFiberCompIso_hom_app, GrothendieckTopology.Point.sheafFiberCompIso_inv_app, GrothendieckTopology.uliftYoneda_map_val_app_down, sheafCompose_obj_val, sheafComposeNatTrans_fac, GrothendieckTopology.uliftYonedaOpCompCoyoneda_inv_app_app_val_app, sheafCompose_comp
sheafCompose_map 📖	CompOp	2 math math: sheafCompose_id, sheafCompose_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSheafCompose_of_preservesLimitsOfSize 📖	mathematical	—	GrothendieckTopology.HasSheafCompose	—	Presheaf.isSheaf_comp_of_isSheaf
hasSheafCompose_of_preservesMulticospan 📖	mathematical	Limits.PreservesLimit Limits.WalkingMulticospan GrothendieckTopology.Cover.shape Limits.WalkingMulticospan.instSmallCategory Limits.MulticospanIndex.multicospan GrothendieckTopology.Cover.index	GrothendieckTopology.HasSheafCompose	—	Presheaf.isSheaf_iff_multifork
instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf 📖	mathematical	—	Functor.Faithful Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category Functor.comp sheafCompose sheafToPresheaf	—	Functor.Faithful.comp instFaithfulSheafFunctorOppositeSheafToPresheaf Functor.faithful_whiskeringRight_obj
instFaithfulSheafSheafCompose 📖	mathematical	—	Functor.Faithful Sheaf Sheaf.instCategorySheaf sheafCompose	—	Functor.Faithful.of_comp instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf
instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful 📖	mathematical	—	Functor.Full Sheaf Sheaf.instCategorySheaf Functor Opposite Category.opposite Functor.category Functor.comp sheafCompose sheafToPresheaf	—	Functor.Full.comp instFullSheafFunctorOppositeSheafToPresheaf Functor.full_whiskeringRight_obj
instFullSheafSheafComposeOfFaithful 📖	mathematical	—	Functor.Full Sheaf Sheaf.instCategorySheaf sheafCompose	—	Functor.Full.of_comp_faithful instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful instFaithfulSheafFunctorOppositeSheafToPresheaf
instReflectsIsomorphismsSheafSheafCompose 📖	mathematical	—	Functor.ReflectsIsomorphisms Sheaf Sheaf.instCategorySheaf sheafCompose	—	isIso_iff_of_reflects_iso instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf instReflectsIsomorphismsFunctorObjWhiskeringRight Functor.map_isIso
sheafCompose_comp 📖	mathematical	—	sheafCompose_map CategoryStruct.comp Functor Category.toCategoryStruct Functor.category Sheaf Sheaf.instCategorySheaf sheafCompose	—	—
sheafCompose_id 📖	mathematical	—	sheafCompose_map CategoryStruct.id Functor Category.toCategoryStruct Functor.category Sheaf Sheaf.instCategorySheaf sheafCompose	—	—
sheafCompose_map_val 📖	mathematical	—	Sheaf.Hom.val Functor.comp Opposite Category.opposite Sheaf.val Functor.map Sheaf Sheaf.instCategorySheaf sheafCompose Functor.whiskerRight	—	—
sheafCompose_obj_val 📖	mathematical	—	Sheaf.val Functor.obj Sheaf Sheaf.instCategorySheaf sheafCompose Functor.comp Opposite Category.opposite	—	—

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
HasSheafCompose 📖	CompData	6 math math: CategoryTheory.hasSheafComposeEssentiallySmallSite, CategoryTheory.hasSheafCompose_of_preservesMulticospan, CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfProjectiveOfPreservesFiniteProducts, CategoryTheory.Presheaf.instHasSheafComposeCoherentTopologyOfForallEffectiveEpiHasPullbackOfPreservesFiniteLimits, CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize, CategoryTheory.Equivalence.hasSheafCompose

CategoryTheory.GrothendieckTopology.Cover

Definitions

Name	Category	Theorems
mapMultifork 📖	CompOp	—
multicospanComp 📖	CompOp	2 math math: multicospanComp_inv_app, multicospanComp_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multicospanComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMulticospan shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan index CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category multicospanComp CategoryTheory.Functor.obj Opposite.op Arrow.Y Arrow.Relation.Z Relation.fst Relation.snd Relation.r CategoryTheory.Iso CategoryTheory.Iso.refl	—	—
multicospanComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingMulticospan shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Functor.comp CategoryTheory.Limits.MulticospanIndex.multicospan index Opposite CategoryTheory.Category.opposite CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category multicospanComp CategoryTheory.Functor.obj Opposite.op Arrow.Y Arrow.Relation.Z Relation.fst Relation.snd Relation.r CategoryTheory.Iso CategoryTheory.Iso.refl	—	—

CategoryTheory.GrothendieckTopology.HasSheafCompose

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf 📖	mathematical	CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite	—	—

CategoryTheory.Presheaf.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparated 📖	mathematical	CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Presheaf.IsSeparated	—	CategoryTheory.Sheaf.isSeparated

CategoryTheory.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparated 📖	mathematical	—	CategoryTheory.Presheaf.IsSeparated val	—	CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheaf.isSeparated CategoryTheory.isSheaf_iff_isSheaf_of_type cond

---

← Back to Index