Over

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

Statistics

Metric	Count
Definitions over, overMapPullback, overMapPullbackComp, overMapPullbackCongr, overMapPullbackId, overPullback, over, overEquiv	8
Theorems coverPreserving_over_star, instIsCocontinuousOverForgetOver, instIsContinuousOverForgetOver, instIsContinuousOverMapOver, instIsContinuousOverStarOver, mem_over_iff, overEquiv_symm_mem_over, overMapPullbackComp_hom_app_val_app, overMapPullbackComp_inv_app_val_app, overMapPullbackCongr_eq_eqToIso, overMapPullbackCongr_hom_app_val_app, overMapPullbackCongr_inv_app_val_app, overMapPullbackId_hom_app_val_app, overMapPullbackId_inv_app_val_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_generate, overEquiv_iff, overEquiv_le_overEquiv_iff, overEquiv_pullback, 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	41
Total	49

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	—	Functor.IsDenseSubsite.instIsCocontinuous instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv
instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver 📖	mathematical	—	Functor.IsCocontinuous Over instCategoryOver Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit Over.iteratedSliceForward GrothendieckTopology.over	—	Functor.IsDenseSubsite.instIsCocontinuous Equivalence.instIsDenseSubsiteFunctor instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv
instIsContinuousOverLeftDiscretePUnitIteratedSliceBackwardOver 📖	mathematical	—	Functor.IsContinuous Over Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit instCategoryOver Over.iteratedSliceBackward GrothendieckTopology.over	—	Functor.IsDenseSubsite.instIsContinuous instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv
instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver 📖	mathematical	—	Functor.IsContinuous Over instCategoryOver Comma.left Discrete discreteCategory Functor.id Functor.fromPUnit Over.iteratedSliceForward GrothendieckTopology.over	—	Functor.IsDenseSubsite.instIsContinuous Equivalence.instIsDenseSubsiteFunctor instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv
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 Precoverage.instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan instIsConnectedWidePullbackShape Precoverage.instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan Over.preservesLimitsOfShape_forget_of_isConnected 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	45 math math: overMapPullbackId_hom_app_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, overMapPullback_comp_id, overMapPullbackId_inv_app_val_app, instIsContinuousOverStarOver, over_map_coverPreserving, CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app, pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, instIsCocontinuousOverForgetOver, coverPreserving_over_star, overEquiv_symm_mem_over, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj, mem_over_iff, overMapPullback_assoc_assoc, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app, CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, overMapPullbackCongr_eq_eqToIso, SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver, CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app, CategoryTheory.Pseudofunctor.IsPrestack.isSheaf, overMapPullback_comp_id_assoc, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map, overMapPullbackComp_inv_app_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α, overMapPullbackComp_hom_app_val_app, instIsContinuousOverForgetOver, overMapPullback_id_comp_assoc, pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, overMapPullbackCongr_hom_app_val_app, instIsContinuousOverMapOver, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, over_map_compatiblePreserving, CategoryTheory.sheafHomSectionsEquiv_symm_apply_coe_apply, overMapPullback_assoc, CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget, overMapPullback_id_comp, CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver, pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, CategoryTheory.instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv, pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, overMapPullbackCongr_inv_app_val_app, over_forget_coverPreserving, CategoryTheory.Pseudofunctor.sheafHom_val
overMapPullback 📖	CompOp	18 math math: overMapPullbackId_hom_app_val_app, pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, overMapPullback_comp_id, overMapPullbackId_inv_app_val_app, pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, overMapPullback_assoc_assoc, overMapPullbackCongr_eq_eqToIso, overMapPullback_comp_id_assoc, overMapPullbackComp_inv_app_val_app, overMapPullbackComp_hom_app_val_app, overMapPullback_id_comp_assoc, pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, overMapPullbackCongr_hom_app_val_app, overMapPullback_assoc, overMapPullback_id_comp, pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, overMapPullbackCongr_inv_app_val_app
overMapPullbackComp 📖	CompOp	8 math math: overMapPullback_comp_id, overMapPullback_assoc_assoc, overMapPullback_comp_id_assoc, overMapPullbackComp_inv_app_val_app, overMapPullbackComp_hom_app_val_app, 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, overMapPullback_id_comp_assoc, overMapPullbackCongr_hom_app_val_app, overMapPullback_assoc, overMapPullback_id_comp, overMapPullbackCongr_inv_app_val_app
overMapPullbackId 📖	CompOp	6 math math: overMapPullbackId_hom_app_val_app, overMapPullback_comp_id, overMapPullbackId_inv_app_val_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_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
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
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.Over CategoryTheory.instCategoryOver over Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Sieve.overEquiv	—	Equiv.apply_symm_apply
overMapPullbackComp_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.comp CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map instIsContinuousOverMapOver CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp instIsContinuousOverMapOver CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category 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.Sheaf.instCategorySheaf CategoryTheory.Functor.category overMapPullback	—	CategoryTheory.Iso.ext CategoryTheory.NatTrans.ext' CategoryTheory.Sheaf.hom_ext CategoryTheory.Functor.map_id
overMapPullbackCongr_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Over.map CategoryTheory.Sheaf.val over CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuousOverMapOver CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Over.map CategoryTheory.Sheaf.val over CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuousOverMapOver CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Sheaf.val over CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.id CategoryTheory.Functor.sheafPushforwardContinuous CategoryTheory.Over.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category 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.Sheaf.instCategorySheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category 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.Sheaf.hom_ext overMapPullbackComp_inv_app_val_app overMapPullbackComp_hom_app_val_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.Sheaf.instCategorySheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category 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.Sheaf.instCategorySheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category 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.Sheaf.hom_ext overMapPullbackComp_inv_app_val_app overMapPullbackId_hom_app_val_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.Sheaf.instCategorySheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category 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.Sheaf.instCategorySheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category 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.Sheaf.hom_ext overMapPullbackComp_inv_app_val_app overMapPullbackId_hom_app_val_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.Sheaf.instCategorySheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category 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	16 math math: overEquiv_pullback, 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_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_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_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_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