Over

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

Statistics

Metric	Count
Definitions over, overMapPullback, overMapPullbackComp, overMapPullbackCongr, overMapPullbackId, overPullback, over, overEquiv	8
Theorems coverPreserving_overPullback, coverPreserving_over_star, instIsCocontinuousOverForgetOver, instIsCocontinuousOverMapOver, instIsContinuousOverForgetOver, instIsContinuousOverMapOver, instIsContinuousOverPullbackOver, instIsContinuousOverStarOver, mem_over_iff, overEquiv_symm_mem_over, overMapPullbackComp_hom_app_hom_app, overMapPullbackComp_inv_app_hom_app, overMapPullbackCongr_eq_eqToIso, overMapPullbackCongr_hom_app_hom_app, overMapPullbackCongr_inv_app_hom_app, overMapPullbackId_hom_app_hom_app, overMapPullbackId_inv_app_hom_app, overMapPullback_assoc, overMapPullback_assoc_assoc, overMapPullback_comp_id, overMapPullback_comp_id_assoc, overMapPullback_id_comp, overMapPullback_id_comp_assoc, over_forget_compatiblePreserving, over_forget_coverPreserving, over_map_compatiblePreserving, over_map_coverPreserving, map_functorPullback_overForget, functorPushforward_over_map, overEquiv_bot, overEquiv_functorPullback_map, overEquiv_generate, overEquiv_iff, overEquiv_le_overEquiv_iff, overEquiv_pullback, overEquiv_symm_bot, overEquiv_symm_generate, overEquiv_symm_iff, overEquiv_symm_pullback, overEquiv_symm_top, overEquiv_top, instIsCocontinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver, instIsContinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver, instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv, over_toGrothendieck_eq_toGrothendieck_comap_forget	47
Total	55

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCocontinuousOverLeftDiscretePUnitIteratedSliceBackwardOver 📖	mathematical	—	Functor.IsCocontinuous Over Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit instCategoryOver Over.iteratedSliceBackward GrothendieckTopology.over	—	—
instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver 📖	mathematical	—	Functor.IsCocontinuous Over instCategoryOver Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit Over.iteratedSliceForward GrothendieckTopology.over	—	—
instIsContinuousOverLeftDiscretePUnitIteratedSliceBackwardOver 📖	mathematical	—	Functor.IsContinuous Over Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit instCategoryOver Over.iteratedSliceBackward GrothendieckTopology.over	—	—
instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver 📖	mathematical	—	Functor.IsContinuous Over instCategoryOver Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit Over.iteratedSliceForward GrothendieckTopology.over	—	—
instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv 📖	mathematical	—	Functor.IsDenseSubsite Over Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit instCategoryOver GrothendieckTopology.over Equivalence.inverse Over.iteratedSliceEquiv	—	Equivalence.instIsCoverDenseOfIsEquivalence Equivalence.isEquivalence_inverse Functor.IsLocallyFull.of_full Equivalence.full_inverse Functor.IsLocallyFaithful.of_faithful Equivalence.faithful_inverse Sieve.functorPushforward_comp
over_toGrothendieck_eq_toGrothendieck_comap_forget 📖	mathematical	—	GrothendieckTopology.over Precoverage.toGrothendieck Over instCategoryOver Precoverage.comap Over.forget	—	le_antisymm Equiv.surjective Sieve.overEquiv_symm_generate Presieve.map_functorPullback_overForget Sieve.overEquiv_symm_top GrothendieckTopology.transitive Sieve.overEquiv_symm_pullback Discrete.instSubsingleton Equiv.apply_symm_apply Precoverage.toGrothendieck_le_iff_le_toPrecoverage GrothendieckTopology.mem_toPrecoverage_iff GrothendieckTopology.mem_over_iff Sieve.overEquiv.eq_1 Sieve.generate_map_eq_functorPushforward Precoverage.mem_comap_iff

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
over 📖	CompOp	65 math math: CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, SheafOfModules.QuasicoherentData.localGeneratorsData_generators, overMapPullback_comp_id, instIsContinuousOverStarOver, instHasEnoughPointsOverOverOfWEqualsLocallyBijectiveHomOfHasSheafifyType, SheafOfModules.Presentation.isQuasicoherent, overMapPullbackId_inv_app_hom_app, pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, over_map_coverPreserving, CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver, subcanonical_over, overMapPullbackComp_hom_app_hom_app, overMapPullbackId_hom_app_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_obj, instIsCocontinuousOverForgetOver, SheafOfModules.QuasicoherentData.IsFinitePresentation.isFinite_presentation, coverPreserving_over_star, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_hom_app, overEquiv_symm_mem_over, instIsContinuousOverPullbackOver, mem_over_iff, SheafOfModules.IsQuasicoherent.of_coversTop, SheafOfModules.Presentation.quasicoherentData_presentation, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over, overMapPullback_assoc_assoc, AlgebraicGeometry.Scheme.ProEt.instLocallyCoverDenseOverForgetOverProetaleTopology, pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, AlgebraicGeometry.Scheme.ProEt.topology_eq_inducedTopology, CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, overMapPullbackComp_inv_app_hom_app, overMapPullbackCongr_eq_eqToIso, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, CategoryTheory.Pseudofunctor.IsPrestack.isSheaf, overMapPullback_comp_id_assoc, CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le, overMapPullbackCongr_inv_app_hom_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, instIsContinuousOverForgetOver, CategoryTheory.Pseudofunctor.sheafHom_obj, overMapPullback_id_comp_assoc, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_hom_app, SheafOfModules.LocalGeneratorsData.IsFiniteType.isFiniteType, overMapPullbackCongr_hom_app_hom_app, pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, instIsContinuousOverMapOver, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, coverPreserving_overPullback, over_map_compatiblePreserving, CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply, SheafOfModules.Presentation.quasicoherentData_I, overMapPullback_assoc, instIsCocontinuousOverMapOver, CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget, overMapPullback_id_comp, CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver, AlgebraicGeometry.Scheme.ProEt.instIsContinuousOverForgetTopologyOverProetaleTopology, CategoryTheory.instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_obj_map, Point.over_fiber, over_forget_coverPreserving, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_hom_app, pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app, SheafOfModules.Presentation.quasicoherentData_X
overMapPullback 📖	CompOp	18 math math: pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, overMapPullback_comp_id, overMapPullbackId_inv_app_hom_app, pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, overMapPullbackComp_hom_app_hom_app, overMapPullbackId_hom_app_hom_app, overMapPullback_assoc_assoc, pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, overMapPullbackComp_inv_app_hom_app, overMapPullbackCongr_eq_eqToIso, overMapPullback_comp_id_assoc, overMapPullbackCongr_inv_app_hom_app, overMapPullback_id_comp_assoc, overMapPullbackCongr_hom_app_hom_app, pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, overMapPullback_assoc, overMapPullback_id_comp, pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app
overMapPullbackComp 📖	CompOp	8 math math: overMapPullback_comp_id, overMapPullbackComp_hom_app_hom_app, overMapPullback_assoc_assoc, overMapPullbackComp_inv_app_hom_app, overMapPullback_comp_id_assoc, overMapPullback_id_comp_assoc, overMapPullback_assoc, overMapPullback_id_comp
overMapPullbackCongr 📖	CompOp	9 math math: overMapPullback_comp_id, overMapPullback_assoc_assoc, overMapPullbackCongr_eq_eqToIso, overMapPullback_comp_id_assoc, overMapPullbackCongr_inv_app_hom_app, overMapPullback_id_comp_assoc, overMapPullbackCongr_hom_app_hom_app, overMapPullback_assoc, overMapPullback_id_comp
overMapPullbackId 📖	CompOp	6 math math: overMapPullback_comp_id, overMapPullbackId_inv_app_hom_app, overMapPullbackId_hom_app_hom_app, overMapPullback_comp_id_assoc, overMapPullback_id_comp_assoc, overMapPullback_id_comp
overPullback 📖	CompOp	1 math math: CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverPreserving_overPullback 📖	mathematical	—	CategoryTheory.CoverPreserving CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.Over.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Adjunction.isCocontinuous_iff_coverPreserving instIsCocontinuousOverMapOver
coverPreserving_over_star 📖	mathematical	—	CategoryTheory.CoverPreserving CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.Over.star	—	superset_covering CategoryTheory.Presieve.functorPushforward_comp CategoryTheory.Limits.prod.hom_ext CategoryTheory.Functor.map_comp CategoryTheory.Limits.prod.map_map CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.id_comp CategoryTheory.Limits.limit.lift_π pullback_stable
instIsCocontinuousOverForgetOver 📖	mathematical	—	CategoryTheory.Functor.IsCocontinuous CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget over	—	overEquiv_symm_mem_over
instIsCocontinuousOverMapOver 📖	mathematical	—	CategoryTheory.Functor.IsCocontinuous CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.map over	—	mem_over_iff CategoryTheory.Sieve.overEquiv_functorPullback_map
instIsContinuousOverForgetOver 📖	mathematical	—	CategoryTheory.Functor.IsContinuous CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget over	—	CategoryTheory.Functor.isContinuous_of_coverPreserving over_forget_compatiblePreserving over_forget_coverPreserving
instIsContinuousOverMapOver 📖	mathematical	—	CategoryTheory.Functor.IsContinuous CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.map over	—	CategoryTheory.Functor.isContinuous_of_coverPreserving over_map_compatiblePreserving over_map_coverPreserving
instIsContinuousOverPullbackOver 📖	mathematical	—	CategoryTheory.Functor.IsContinuous CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan over	—	CategoryTheory.Adjunction.isContinuous_of_isCocontinuous CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instIsCocontinuousOverMapOver
instIsContinuousOverStarOver 📖	mathematical	—	CategoryTheory.Functor.IsContinuous CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.star over	—	CategoryTheory.Functor.isContinuous_of_coverPreserving CategoryTheory.compatiblePreservingOfFlat CategoryTheory.RepresentablyFlat.of_isRightAdjoint CategoryTheory.Over.instIsRightAdjointStar coverPreserving_over_star
mem_over_iff 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve over CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Sieve.overEquiv	—	—
overEquiv_symm_mem_over 📖	mathematical	CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve over Equiv CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Sieve.overEquiv	—	Equiv.apply_symm_apply
overMapPullbackComp_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.comp CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map instIsContinuousOverMapOver CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom overMapPullback overMapPullbackComp CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Over.mapComp	—	CategoryTheory.Category.id_comp
overMapPullbackComp_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp instIsContinuousOverMapOver CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv overMapPullback overMapPullbackComp CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Over.mapComp	—	CategoryTheory.Category.comp_id
overMapPullbackCongr_eq_eqToIso 📖	mathematical	—	overMapPullbackCongr CategoryTheory.eqToIso CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf overMapPullback	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.ObjectProperty.hom_ext CategoryTheory.Functor.map_id
overMapPullbackCongr_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Over.map CategoryTheory.Functor.obj CategoryTheory.Sheaf over CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuousOverMapOver CategoryTheory.Iso.hom overMapPullback overMapPullbackCongr CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Over.mapCongr	—	instIsContinuousOverMapOver
overMapPullbackCongr_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Over.map CategoryTheory.Functor.obj CategoryTheory.Sheaf over CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.sheafToPresheaf CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuousOverMapOver CategoryTheory.Iso.inv overMapPullback overMapPullbackCongr CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Over.mapCongr	—	instIsContinuousOverMapOver
overMapPullbackId_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom overMapPullback overMapPullbackId CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv CategoryTheory.Over.mapId	—	CategoryTheory.Category.comp_id
overMapPullbackId_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.id CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv overMapPullback overMapPullbackId CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom CategoryTheory.Over.mapId	—	CategoryTheory.Category.id_comp
overMapPullback_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct overMapPullback CategoryTheory.Functor.comp CategoryTheory.Iso.inv overMapPullbackComp CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft overMapPullbackCongr	—	CategoryTheory.NatTrans.ext' CategoryTheory.ObjectProperty.hom_ext overMapPullbackComp_inv_app_hom_app overMapPullbackComp_hom_app_hom_app CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Over.OverMorphism.ext CategoryTheory.Category.comp_id
overMapPullback_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct overMapPullback CategoryTheory.Functor.comp CategoryTheory.Iso.inv overMapPullbackComp CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft overMapPullbackCongr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' overMapPullback_assoc
overMapPullback_comp_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct overMapPullback CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv overMapPullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom overMapPullbackId CategoryTheory.Functor.leftUnitor overMapPullbackCongr	—	CategoryTheory.NatTrans.ext' CategoryTheory.ObjectProperty.hom_ext overMapPullbackComp_inv_app_hom_app overMapPullbackId_hom_app_hom_app CategoryTheory.Category.comp_id CategoryTheory.Over.OverMorphism.ext
overMapPullback_comp_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct overMapPullback CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv overMapPullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight CategoryTheory.Iso.hom overMapPullbackId CategoryTheory.Functor.leftUnitor overMapPullbackCongr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' overMapPullback_comp_id
overMapPullback_id_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct overMapPullback CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv overMapPullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom overMapPullbackId CategoryTheory.Functor.rightUnitor overMapPullbackCongr	—	CategoryTheory.NatTrans.ext' CategoryTheory.ObjectProperty.hom_ext overMapPullbackComp_inv_app_hom_app overMapPullbackId_hom_app_hom_app CategoryTheory.Category.comp_id CategoryTheory.Over.OverMorphism.ext
overMapPullback_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct overMapPullback CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv overMapPullbackComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom overMapPullbackId CategoryTheory.Functor.rightUnitor overMapPullbackCongr	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' overMapPullback_id_comp
over_forget_compatiblePreserving 📖	mathematical	—	CategoryTheory.CompatiblePreserving CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget	—	CategoryTheory.Category.assoc CategoryTheory.Over.w CategoryTheory.eq_whisker CategoryTheory.Over.OverMorphism.ext
over_forget_coverPreserving 📖	mathematical	—	CategoryTheory.CoverPreserving CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.Over.forget	—	—
over_map_compatiblePreserving 📖	mathematical	—	CategoryTheory.CompatiblePreserving CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.Over.map	—	CategoryTheory.Category.assoc CategoryTheory.Over.w CategoryTheory.eq_whisker CategoryTheory.Functor.congr_map CategoryTheory.Category.id_comp CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp CategoryTheory.Over.OverMorphism.ext
over_map_coverPreserving 📖	mathematical	—	CategoryTheory.CoverPreserving CategoryTheory.Over CategoryTheory.instCategoryOver over CategoryTheory.Over.map	—	Equiv.surjective CategoryTheory.Sieve.functorPushforward_over_map overEquiv_symm_mem_over Equiv.apply_symm_apply

CategoryTheory.Presieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_functorPullback_overForget 📖	mathematical	—	map CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget functorPullback	—	le_antisymm map_functorPullback

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
over 📖	CompOp	5 math math: SheafOfModules.QuasicoherentData.localGeneratorsData_generators, SheafOfModules.QuasicoherentData.IsFinitePresentation.isFinite_presentation, SheafOfModules.Presentation.quasicoherentData_presentation, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, SheafOfModules.LocalGeneratorsData.IsFiniteType.isFiniteType

CategoryTheory.Sieve

Definitions

Name	Category	Theorems
overEquiv 📖	CompOp	19 math math: overEquiv_pullback, overEquiv_bot, overEquiv_le_overEquiv_iff, overEquiv_symm_iff, CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over, functorPushforward_over_map, CategoryTheory.GrothendieckTopology.mem_over_iff, overEquiv_top, overEquiv_symm_pullback, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor, overEquiv_functorPullback_map, overEquiv_symm_generate, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, overEquiv_symm_top, overEquiv_generate, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor', overEquiv_symm_bot, overEquiv_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorPushforward_over_map 📖	mathematical	—	functorPushforward CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.map DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm overEquiv CategoryTheory.Functor.obj	—	ext downward_closed CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Over.w CategoryTheory.Over.OverMorphism.ext
overEquiv_bot 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike overEquiv Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	functorPushforward_bot
overEquiv_functorPullback_map 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike overEquiv functorPullback CategoryTheory.Over.map CategoryTheory.Functor.obj	—	ext CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Over.OverMorphism.ext CategoryTheory.Category.comp_id overEquiv_iff
overEquiv_generate 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike overEquiv generate CategoryTheory.Presieve.functorPushforward CategoryTheory.Over.forget	—	le_antisymm overEquiv_iff CategoryTheory.Category.id_comp generate_le_iff CategoryTheory.Category.assoc CategoryTheory.Over.w
overEquiv_iff 📖	mathematical	—	arrows CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver EquivLike.toFunLike Equiv.instEquivLike overEquiv CategoryTheory.Functor.obj CategoryTheory.Comma.right CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom CategoryTheory.Over.homMk	—	Equiv.surjective Equiv.apply_symm_apply
overEquiv_le_overEquiv_iff 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice DFunLike.coe Equiv CategoryTheory.Over CategoryTheory.instCategoryOver EquivLike.toFunLike Equiv.instEquivLike overEquiv	—	functorPullback_monotone Equiv.symm_apply_apply functorPushforward_monotone
overEquiv_pullback 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike overEquiv pullback CategoryTheory.CommaMorphism.left	—	ext CategoryTheory.Category.assoc CategoryTheory.Over.w Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Over.OverMorphism.ext downward_closed CategoryTheory.Category.id_comp
overEquiv_symm_bot 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm overEquiv Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	overEquiv.eq_1 functorPullback_bot
overEquiv_symm_generate 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm overEquiv generate CategoryTheory.Presieve.functorPullback CategoryTheory.Over.forget	—	le_antisymm overEquiv_symm_iff CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Over.w CategoryTheory.Over.OverMorphism.ext generate_le_iff le_generate
overEquiv_symm_iff 📖	mathematical	—	arrows CategoryTheory.Over CategoryTheory.instCategoryOver DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm overEquiv CategoryTheory.CommaMorphism.left	—	—
overEquiv_symm_pullback 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm overEquiv pullback CategoryTheory.CommaMorphism.left	—	functorPullback_pullback
overEquiv_symm_top 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Over CategoryTheory.instCategoryOver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm overEquiv Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Equiv.injective Equiv.apply_symm_apply overEquiv_top
overEquiv_top 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike overEquiv Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext CategoryTheory.Category.comp_id

---

← Back to Index