Documentation Verification Report

CoverLifting

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

Statistics

Metric	Count
Definitions `IsCocontinuous`, `pushforwardContinuousSheafificationCompatibility`, `sheafAdjunctionCocontinuous`, `sheafPushforwardCocontinuous`, `sheafPushforwardCocontinuousCompSheafToPresheafIso`, `isLimitMultifork`, `liftAux`	7
Theorems `isCocontinuous_iff_coverPreserving`, `isContinuous_of_isCocontinuous`, `cover_lift`, `cover_lift`, `pushforwardContinuousSheafificationCompatibility_hom_app_hom`, `pushforwardContinuousSheafificationCompatibility_hom_app_val`, `sheafAdjunctionCocontinuous_counit_app_hom`, `sheafAdjunctionCocontinuous_counit_app_val`, `sheafAdjunctionCocontinuous_homEquiv_apply_hom`, `sheafAdjunctionCocontinuous_homEquiv_apply_val`, `sheafAdjunctionCocontinuous_unit_app_hom`, `sheafAdjunctionCocontinuous_unit_app_val`, `sheafPushforwardCocontinuousCompSheafToPresheafIso_hom`, `sheafPushforwardCocontinuousCompSheafToPresheafIso_inv`, `toSheafify_pullbackSheafificationCompatibility`, `fac`, `fac'`, `fac_assoc`, `hom_ext`, `liftAux_map`, `liftAux_map'`, `instIsContinuousRightAdjointOfIsCocontinuous`, `isCocontinuous_comp`, `isCocontinuous_id`, `ran_isSheaf_of_isCocontinuous`	25
Total	32

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsContinuousRightAdjointOfIsCocontinuous` 📖	mathematical	—	`Functor.IsContinuous` `Functor.rightAdjoint`	—	`Adjunction.isContinuous_of_isCocontinuous`
`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` `Opposite` `Category.opposite` `Functor.category` `Functor.ran` `Functor.op` `Functor.instHasRightKanExtension` `ObjectProperty.FullSubcategory.obj`	—	`Functor.instHasRightKanExtension` `Presheaf.isSheaf_iff_multifork` `ObjectProperty.FullSubcategory.property`

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCocontinuous_iff_coverPreserving` 📖	mathematical	—	`CategoryTheory.Functor.IsCocontinuous` `CategoryTheory.CoverPreserving`	—	`CategoryTheory.GrothendieckTopology.superset_covering` `CategoryTheory.Functor.map_comp` `unit_naturality_assoc` `right_triangle_components` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.IsCocontinuous.cover_lift` `CategoryTheory.GrothendieckTopology.pullback_stable` `homEquiv_naturality_left_symm` `homEquiv_symm_unit` `CategoryTheory.Sieve.downward_closed` `CategoryTheory.CoverPreserving.cover_preserve`
`isContinuous_of_isCocontinuous` 📖	mathematical	—	`CategoryTheory.Functor.IsContinuous`	—	`isRightAdjoint` `CategoryTheory.Functor.isContinuous_of_coverPreserving` `CategoryTheory.compatiblePreservingOfFlat` `CategoryTheory.RepresentablyFlat.of_isRightAdjoint` `isCocontinuous_iff_coverPreserving`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`IsCocontinuous` 📖	CompData	9 math math: `inducedTopology_isCocontinuous`, `CategoryTheory.isCocontinuous_comp`, `CategoryTheory.GrothendieckTopology.instIsCocontinuousOverForgetOver`, `IsDenseSubsite.instIsCocontinuous`, `CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceBackwardOver`, `CategoryTheory.Adjunction.isCocontinuous_iff_coverPreserving`, `CategoryTheory.isCocontinuous_id`, `CategoryTheory.GrothendieckTopology.instIsCocontinuousOverMapOver`, `CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver`
`pushforwardContinuousSheafificationCompatibility` 📖	CompOp	3 math math: `toSheafify_pullbackSheafificationCompatibility`, `pushforwardContinuousSheafificationCompatibility_hom_app_val`, `pushforwardContinuousSheafificationCompatibility_hom_app_hom`
`sheafAdjunctionCocontinuous` 📖	CompOp	7 math math: `IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous`, `sheafAdjunctionCocontinuous_homEquiv_apply_hom`, `sheafAdjunctionCocontinuous_counit_app_val`, `sheafAdjunctionCocontinuous_unit_app_hom`, `sheafAdjunctionCocontinuous_counit_app_hom`, `sheafAdjunctionCocontinuous_homEquiv_apply_val`, `sheafAdjunctionCocontinuous_unit_app_val`
`sheafPushforwardCocontinuous` 📖	CompOp	9 math math: `IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous`, `sheafAdjunctionCocontinuous_homEquiv_apply_hom`, `sheafAdjunctionCocontinuous_counit_app_val`, `sheafAdjunctionCocontinuous_unit_app_hom`, `sheafAdjunctionCocontinuous_counit_app_hom`, `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` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `CategoryTheory.Sieve.functorPullback`	—	`IsCocontinuous.cover_lift`
`pushforwardContinuousSheafificationCompatibility_hom_app_hom` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `comp` `whiskeringLeft` `op` `CategoryTheory.presheafToSheaf` `sheafPushforwardContinuous` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `pushforwardContinuousSheafificationCompatibility` `CategoryTheory.sheafifyLift` `CategoryTheory.sheafify` `whiskerLeft` `CategoryTheory.toSheafify` `CategoryTheory.ObjectProperty.FullSubcategory.property`	—	`CategoryTheory.sheafifyLift_unique` `CategoryTheory.ObjectProperty.FullSubcategory.property` `toSheafify_pullbackSheafificationCompatibility`
`pushforwardContinuousSheafificationCompatibility_hom_app_val` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `comp` `whiskeringLeft` `op` `CategoryTheory.presheafToSheaf` `sheafPushforwardContinuous` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `pushforwardContinuousSheafificationCompatibility` `CategoryTheory.sheafifyLift` `CategoryTheory.sheafify` `whiskerLeft` `CategoryTheory.toSheafify` `CategoryTheory.ObjectProperty.FullSubcategory.property`	—	`pushforwardContinuousSheafificationCompatibility_hom_app_hom`
`sheafAdjunctionCocontinuous_counit_app_hom` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `comp` `sheafPushforwardCocontinuous` `sheafPushforwardContinuous` `id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `sheafAdjunctionCocontinuous` `ran` `op` `instHasRightKanExtension` `whiskeringLeft` `ranAdjunction`	—	`instHasRightKanExtension` `CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app` `ranAdjunction_counit` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.ext'`
`sheafAdjunctionCocontinuous_counit_app_val` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `comp` `sheafPushforwardCocontinuous` `sheafPushforwardContinuous` `id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `sheafAdjunctionCocontinuous` `ran` `op` `instHasRightKanExtension` `whiskeringLeft` `ranAdjunction`	—	`sheafAdjunctionCocontinuous_counit_app_hom`
`sheafAdjunctionCocontinuous_homEquiv_apply_hom` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `sheafPushforwardCocontinuous` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `sheafPushforwardContinuous` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `sheafAdjunctionCocontinuous` `whiskeringLeft` `op` `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_homEquiv_apply_val` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `sheafPushforwardCocontinuous` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `sheafPushforwardContinuous` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `sheafAdjunctionCocontinuous` `whiskeringLeft` `op` `ran` `instHasRightKanExtension` `ranAdjunction`	—	`sheafAdjunctionCocontinuous_homEquiv_apply_hom`
`sheafAdjunctionCocontinuous_unit_app_hom` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `id` `comp` `sheafPushforwardContinuous` `sheafPushforwardCocontinuous` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `sheafAdjunctionCocontinuous` `whiskeringLeft` `op` `ran` `instHasRightKanExtension` `ranAdjunction`	—	`instHasRightKanExtension` `CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app` `map_id` `CategoryTheory.Category.comp_id`
`sheafAdjunctionCocontinuous_unit_app_val` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `id` `comp` `sheafPushforwardContinuous` `sheafPushforwardCocontinuous` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `sheafAdjunctionCocontinuous` `whiskeringLeft` `op` `ran` `instHasRightKanExtension` `ranAdjunction`	—	`sheafAdjunctionCocontinuous_unit_app_hom`
`sheafPushforwardCocontinuousCompSheafToPresheafIso_hom` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `comp` `sheafPushforwardCocontinuous` `CategoryTheory.sheafToPresheaf` `ran` `op` `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.ObjectProperty.FullSubcategory.category` `Opposite` `CategoryTheory.Category.opposite` `category` `CategoryTheory.Presheaf.IsSheaf` `comp` `sheafPushforwardCocontinuous` `CategoryTheory.sheafToPresheaf` `ran` `op` `instHasRightKanExtension` `sheafPushforwardCocontinuousCompSheafToPresheafIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`instHasRightKanExtension`
`toSheafify_pullbackSheafificationCompatibility` 📖	mathematical	`HasPointwiseRightKanExtension` `Opposite` `CategoryTheory.Category.opposite` `op`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Category.toCategoryStruct` `category` `comp` `op` `CategoryTheory.sheafify` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Presheaf.IsSheaf` `obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.presheafToSheaf` `sheafPushforwardContinuous` `CategoryTheory.toSheafify` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `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_hom`

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` `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.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` `liftAux` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.MulticospanIndex.left` `CategoryTheory.Limits.Multifork.ι` `CategoryTheory.GrothendieckTopology.Cover.Arrow.Y` `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.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` `liftAux` `CategoryTheory.Functor.map` `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