CoverLifting

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

Statistics

Metric	Count
Definitions IsCocontinuous, pushforwardContinuousSheafificationCompatibility, sheafAdjunctionCocontinuous, sheafPushforwardCocontinuous, sheafPushforwardCocontinuousCompSheafToPresheafIso, isLimitMultifork, liftAux	7
Theorems cover_lift, cover_lift, pushforwardContinuousSheafificationCompatibility_hom_app_val, sheafAdjunctionCocontinuous_counit_app_val, sheafAdjunctionCocontinuous_homEquiv_apply_val, sheafAdjunctionCocontinuous_unit_app_val, sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, toSheafify_pullbackSheafificationCompatibility, fac, fac', fac_assoc, hom_ext, liftAux_map, liftAux_map', isCocontinuous_comp, isCocontinuous_id, ran_isSheaf_of_isCocontinuous	18
Total	25

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCocontinuous_comp 📖	mathematical	—	Functor.IsCocontinuous Functor.comp	—	Functor.cover_lift
isCocontinuous_id 📖	mathematical	—	Functor.IsCocontinuous Functor.id	—	Sieve.functorPullback_id
ran_isSheaf_of_isCocontinuous 📖	mathematical	Functor.HasPointwiseRightKanExtension Opposite Category.opposite Functor.op	Presheaf.IsSheaf Functor.obj Functor Functor.category Functor.ran Functor.instHasRightKanExtension Sheaf.val	—	Functor.instHasRightKanExtension Presheaf.isSheaf_iff_multifork Sheaf.cond

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsCocontinuous 📖	CompData	7 math math: inducedTopology_isCocontinuous, CategoryTheory.isCocontinuous_comp, CategoryTheory.GrothendieckTopology.instIsCocontinuousOverForgetOver, IsDenseSubsite.instIsCocontinuous, CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, CategoryTheory.isCocontinuous_id, CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver
pushforwardContinuousSheafificationCompatibility 📖	CompOp	2 math math: toSheafify_pullbackSheafificationCompatibility, pushforwardContinuousSheafificationCompatibility_hom_app_val
sheafAdjunctionCocontinuous 📖	CompOp	4 math math: IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, sheafAdjunctionCocontinuous_counit_app_val, sheafAdjunctionCocontinuous_homEquiv_apply_val, sheafAdjunctionCocontinuous_unit_app_val
sheafPushforwardCocontinuous 📖	CompOp	7 math math: IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, IsDenseSubsite.sheafEquiv_functor, sheafAdjunctionCocontinuous_counit_app_val, sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, sheafPushforwardCocontinuousCompSheafToPresheafIso_hom, sheafAdjunctionCocontinuous_homEquiv_apply_val, sheafAdjunctionCocontinuous_unit_app_val
sheafPushforwardCocontinuousCompSheafToPresheafIso 📖	CompOp	2 math math: sheafPushforwardCocontinuousCompSheafToPresheafIso_inv, sheafPushforwardCocontinuousCompSheafToPresheafIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cover_lift 📖	mathematical	CategoryTheory.Sieve obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.Sieve.functorPullback	—	IsCocontinuous.cover_lift
pushforwardContinuousSheafificationCompatibility_hom_app_val 📖	mathematical	HasPointwiseRightKanExtension Opposite CategoryTheory.Category.opposite op	CategoryTheory.Sheaf.Hom.val obj CategoryTheory.Functor category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf comp whiskeringLeft CategoryTheory.presheafToSheaf sheafPushforwardContinuous CategoryTheory.NatTrans.app CategoryTheory.Iso.hom pushforwardContinuousSheafificationCompatibility CategoryTheory.sheafifyLift CategoryTheory.sheafify whiskerLeft CategoryTheory.toSheafify CategoryTheory.Sheaf.cond	—	CategoryTheory.sheafifyLift_unique CategoryTheory.Sheaf.cond toSheafify_pullbackSheafificationCompatibility
sheafAdjunctionCocontinuous_counit_app_val 📖	mathematical	HasPointwiseRightKanExtension Opposite CategoryTheory.Category.opposite op	CategoryTheory.Sheaf.Hom.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf comp sheafPushforwardCocontinuous sheafPushforwardContinuous id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit sheafAdjunctionCocontinuous CategoryTheory.Functor category ran instHasRightKanExtension whiskeringLeft ranAdjunction CategoryTheory.Sheaf.val	—	instHasRightKanExtension CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app ranAdjunction_counit CategoryTheory.Category.id_comp CategoryTheory.NatTrans.ext'
sheafAdjunctionCocontinuous_homEquiv_apply_val 📖	mathematical	HasPointwiseRightKanExtension Opposite CategoryTheory.Category.opposite op	CategoryTheory.Sheaf.Hom.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardCocontinuous DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct sheafPushforwardContinuous EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv sheafAdjunctionCocontinuous CategoryTheory.Functor category whiskeringLeft CategoryTheory.Sheaf.val ran instHasRightKanExtension ranAdjunction	—	instHasRightKanExtension congr_map CategoryTheory.Adjunction.restrictFullyFaithful_homEquiv_apply map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Adjunction.homEquiv_unit
sheafAdjunctionCocontinuous_unit_app_val 📖	mathematical	HasPointwiseRightKanExtension Opposite CategoryTheory.Category.opposite op	CategoryTheory.Sheaf.Hom.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf id comp sheafPushforwardContinuous sheafPushforwardCocontinuous CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit sheafAdjunctionCocontinuous CategoryTheory.Functor category whiskeringLeft ran instHasRightKanExtension ranAdjunction CategoryTheory.Sheaf.val	—	instHasRightKanExtension CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app map_id CategoryTheory.Category.comp_id
sheafPushforwardCocontinuousCompSheafToPresheafIso_hom 📖	mathematical	HasPointwiseRightKanExtension Opposite CategoryTheory.Category.opposite op	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf category comp sheafPushforwardCocontinuous CategoryTheory.sheafToPresheaf ran instHasRightKanExtension sheafPushforwardCocontinuousCompSheafToPresheafIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	instHasRightKanExtension
sheafPushforwardCocontinuousCompSheafToPresheafIso_inv 📖	mathematical	HasPointwiseRightKanExtension Opposite CategoryTheory.Category.opposite op	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf category comp sheafPushforwardCocontinuous CategoryTheory.sheafToPresheaf ran instHasRightKanExtension sheafPushforwardCocontinuousCompSheafToPresheafIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	instHasRightKanExtension
toSheafify_pullbackSheafificationCompatibility 📖	mathematical	HasPointwiseRightKanExtension Opposite CategoryTheory.Category.opposite op	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct category comp CategoryTheory.sheafify CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.presheafToSheaf sheafPushforwardContinuous CategoryTheory.toSheafify CategoryTheory.Sheaf.Hom.val whiskeringLeft CategoryTheory.NatTrans.app CategoryTheory.Iso.hom pushforwardContinuousSheafificationCompatibility whiskerLeft	—	instHasRightKanExtension Equiv.injective CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app CategoryTheory.Adjunction.homEquiv_unit map_comp CategoryTheory.Category.assoc comp_map CategoryTheory.Adjunction.comp_unit_app CategoryTheory.Adjunction.homEquiv_counit CategoryTheory.Adjunction.unit_naturality sheafAdjunctionCocontinuous_unit_app_val

CategoryTheory.Functor.IsCocontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cover_lift 📖	mathematical	CategoryTheory.Sieve CategoryTheory.Functor.obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.Sieve.functorPullback	—	—

CategoryTheory.RanIsSheafOfIsCocontinuous

Definitions

Name	Category	Theorems
isLimitMultifork 📖	CompOp	—
liftAux 📖	CompOp	3 math math: liftAux_map', fac', liftAux_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.GrothendieckTopology.Cover.Arrow.Y lift CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Limits.IsLimit.hom_ext fac' CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id liftAux_map CategoryTheory.Category.id_comp
fac' 📖	mathematical	CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.op lift CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.comp liftAux Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.left	—	CategoryTheory.Limits.IsLimit.fac
fac_assoc 📖	mathematical	CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op lift CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.GrothendieckTopology.Cover.Arrow.f CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
hom_ext 📖	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.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.Limits.IsLimit.hom_ext CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Functor.cover_lift CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
liftAux_map 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GrothendieckTopology.Cover.Arrow.Y CategoryTheory.GrothendieckTopology.Cover.Arrow.f CategoryTheory.Functor.map	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index Opposite CategoryTheory.Category.opposite Opposite.op liftAux Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Limits.Multifork.ι CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.op	—	CategoryTheory.Functor.cover_lift CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Sieve.downward_closed CategoryTheory.GrothendieckTopology.Cover.Arrow.hf CategoryTheory.Limits.Multifork.IsLimit.fac CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Limits.Multifork.condition
liftAux_map' 📖	mathematical	CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index Opposite CategoryTheory.Category.opposite Opposite.op liftAux Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Functor.cover_lift CategoryTheory.GrothendieckTopology.pullback_stable liftAux_map CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Functor.map_id

---

← Back to Index