Continuous

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

Statistics

Metric	Count
Definitions sheafPushforwardContinuous, IsContinuous, PreservesOneHypercovers, sheafPushforwardContinuous, sheafPushforwardContinuousComp, sheafPushforwardContinuousComp', sheafPushforwardContinuousCompSheafToPresheafIso, sheafPushforwardContinuousId, sheafPushforwardContinuousId', sheafPushforwardContinuousIso, sheafPushforwardContinuousNatTrans, IsPreservedBy, map, isLimitMapMultiforkEquiv, map	15
Theorems sheafPushforwardContinuous_counit_app_hom_app, sheafPushforwardContinuous_unit_app_hom_app, op_comp_isSheaf_of_types, W_map_of_adjunction_of_isContinuous, instIsContinuousCompId, instIsContinuousCompId_1, instIsContinuousOfPreservesOneHypercovers, isContinuous_comp, isContinuous_comp', isContinuous_id, isContinuous_of_iso, isContinuous_of_preservesOneHypercovers, isContinuous_toGrothendieck_of_pullbacksPreservedBy, op_comp_isSheaf, op_comp_isSheaf_of_isSheaf, op_comp_isSheaf_of_preservesOneHypercovers, op_comp_isSheaf_of_types, sheafPushforwardContinuousComp'_hom_app_hom_app, sheafPushforwardContinuousComp'_inv_app_hom_app, sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, sheafPushforwardContinuousComp_hom_app_hom_app, sheafPushforwardContinuousComp_inv_app_hom_app, sheafPushforwardContinuousId'_hom_app_hom_app, sheafPushforwardContinuousId'_inv_app_hom_app, sheafPushforwardContinuousId_hom_app_hom_app, sheafPushforwardContinuousId_inv_app_hom_app, sheafPushforwardContinuousIso_hom, sheafPushforwardContinuousIso_inv, sheafPushforwardContinuousNatTrans_app_hom, sheafPushforwardContinuous_map_hom_app, sheafPushforwardContinuous_obj_obj_map, sheafPushforwardContinuous_obj_obj_obj, mem₀, mem₁, instIsPreservedById, map_toPreOneHypercover, map_I₀, map_I₁, map_X, map_Y, map_f, map_p₁, map_p₂	44
Total	59

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
sheafPushforwardContinuous 📖	CompOp	2 math math: sheafPushforwardContinuous_unit_app_hom_app, sheafPushforwardContinuous_counit_app_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sheafPushforwardContinuous_counit_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.sheafPushforwardContinuous counit sheafPushforwardContinuous CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct unit	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
sheafPushforwardContinuous_unit_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.op CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor.sheafPushforwardContinuous unit sheafPushforwardContinuous CategoryTheory.Functor.map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct counit	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsContinuous 📖	CompData	28 math math: AlgebraicGeometry.Scheme.ProEt.instIsContinuousCompOverForgetForgetTopologyProetaleTopology, Topology.IsOpenEmbedding.functor_isContinuous, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, CategoryTheory.instIsContinuousRightAdjointOfIsCocontinuous, CategoryTheory.GrothendieckTopology.instIsContinuousOverStarOver, instIsContinuousCompId_1, TopologicalSpace.Opens.instIsContinuousCompGrothendieckTopology, instIsContinuousOfPreservesOneHypercovers, CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver, isContinuous_of_coverPreserving, isContinuous_id, AlgebraicGeometry.Scheme.instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology, IsCoverDense.isContinuous, CategoryTheory.GrothendieckTopology.instIsContinuousOverPullbackOver, CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceBackwardOver, isContinuous_toGrothendieck_of_pullbacksPreservedBy, isContinuous_comp, isContinuous_of_preservesOneHypercovers, instIsContinuousCompId, isContinuous_comp', isContinuous_of_iso, IsDenseSubsite.instIsContinuous, CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver, instIsContinuousOpensCarrierMapGrothendieckTopology, CategoryTheory.GrothendieckTopology.instIsContinuousOverMapOver, TopCat.instIsContinuousUliftFunctorGrothendieckTopology, CategoryTheory.Adjunction.isContinuous_of_isCocontinuous, AlgebraicGeometry.Scheme.ProEt.instIsContinuousOverForgetTopologyOverProetaleTopology
PreservesOneHypercovers 📖	MathDef	—
sheafPushforwardContinuous 📖	CompOp	66 math math: SheafOfModules.pushforward_assoc, IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, sheafPushforwardContinuousIso_inv, sheafAdjunctionCocontinuous_homEquiv_apply_hom, IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous, SheafOfModules.pushforwardNatIso_inv, sheafPushforwardContinuous_map_hom_app, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_hom_app, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, sheafPushforwardContinuousNatTrans_app_hom, sheafPushforwardContinuousId'_hom_app_hom_app, sheafAdjunctionCocontinuous_counit_app_val, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_hom_app, CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_app, CategoryTheory.Adjunction.sheafPushforwardContinuous_unit_app_hom_app, sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify, OneHypercoverDenseData.essSurj, sheafAdjunctionCocontinuous_unit_app_hom, IsCoverDense.faithful_sheafPushforwardContinuous, SheafOfModules.pushforwardComp_inv_app_val_app, OneHypercoverDenseData.isEquivalence, SheafOfModules.pushforwardNatTrans_id, sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, sheafAdjunctionCocontinuous_counit_app_hom, sheafPushforwardContinuousId_hom_app_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_hom_app, IsDenseSubsite.sheafEquiv_inverse, sheafPushforwardContinuous_obj_obj_obj, SheafOfModules.conjugateEquiv_pullbackComp_inv, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_app, SheafOfModules.pushforward_map_val, SheafOfModules.pushforwardComp_hom_app_val_app, sheafPushforwardContinuous_obj_obj_map, toSheafify_pullbackSheafificationCompatibility, SheafOfModules.pushforwardCongr_symm, CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_hom_app, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, SheafOfModules.pullback_assoc, sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_hom_app, SheafOfModules.pushforwardNatTrans_app_val_app, sheafPushforwardContinuousIso_hom, sheafPushforwardContinuousComp_inv_app_hom_app, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_hom_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app, CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso_inv_app, sheafPushforwardContinuousComp'_inv_app_hom_app, sheafPushforwardContinuousId'_inv_app_hom_app, SheafOfModules.pushforwardNatTrans_app_val_app_apply, isEquivalence_of_isOneHypercoverDense, CategoryTheory.Adjunction.sheafPushforwardContinuous_counit_app_hom_app, sheafPushforwardContinuousComp'_hom_app_hom_app, sheafAdjunctionCocontinuous_homEquiv_apply_val, SheafOfModules.pushforwardNatIso_hom, sheafPushforwardContinuousComp_hom_app_hom_app, pushforwardContinuousSheafificationCompatibility_hom_app_val, IsDenseSubsite.full_sheafPushforwardContinuous, sheafPushforwardContinuousId_inv_app_hom_app, sheafAdjunctionCocontinuous_unit_app_val, SheafOfModules.pushforward_obj_val, pushforwardContinuousSheafificationCompatibility_hom_app_hom, IsDenseSubsite.faithful_sheafPushforwardContinuous, SheafOfModules.pushforwardNatTrans_comp, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_hom_app, IsCoverDense.full_sheafPushforwardContinuous
sheafPushforwardContinuousComp 📖	CompOp	2 math math: sheafPushforwardContinuousComp_inv_app_hom_app, sheafPushforwardContinuousComp_hom_app_hom_app
sheafPushforwardContinuousComp' 📖	CompOp	2 math math: sheafPushforwardContinuousComp'_inv_app_hom_app, sheafPushforwardContinuousComp'_hom_app_hom_app
sheafPushforwardContinuousCompSheafToPresheafIso 📖	CompOp	2 math math: sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app
sheafPushforwardContinuousId 📖	CompOp	2 math math: sheafPushforwardContinuousId_hom_app_hom_app, sheafPushforwardContinuousId_inv_app_hom_app
sheafPushforwardContinuousId' 📖	CompOp	2 math math: sheafPushforwardContinuousId'_hom_app_hom_app, sheafPushforwardContinuousId'_inv_app_hom_app
sheafPushforwardContinuousIso 📖	CompOp	2 math math: sheafPushforwardContinuousIso_inv, sheafPushforwardContinuousIso_hom
sheafPushforwardContinuousNatTrans 📖	CompOp	9 math math: sheafPushforwardContinuousIso_inv, SheafOfModules.pushforwardNatIso_inv, sheafPushforwardContinuousNatTrans_app_hom, SheafOfModules.pushforwardNatTrans_id, SheafOfModules.pushforwardNatTrans_app_val_app, sheafPushforwardContinuousIso_hom, SheafOfModules.pushforwardNatTrans_app_val_app_apply, SheafOfModules.pushforwardNatIso_hom, SheafOfModules.pushforwardNatTrans_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_map_of_adjunction_of_isContinuous 📖	mathematical	CategoryTheory.GrothendieckTopology.W	CategoryTheory.GrothendieckTopology.W obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite category map	—	CategoryTheory.Adjunction.map_comp_bijective_iff op_comp_isSheaf_of_isSheaf
instIsContinuousCompId 📖	mathematical	—	IsContinuous comp id	—	—
instIsContinuousCompId_1 📖	mathematical	—	IsContinuous comp id	—	—
instIsContinuousOfPreservesOneHypercovers 📖	mathematical	PreservesOneHypercovers	IsContinuous	—	isContinuous_of_preservesOneHypercovers CategoryTheory.GrothendieckTopology.instIsGeneratedByOneHypercovers
isContinuous_comp 📖	mathematical	—	IsContinuous comp	—	op_comp_isSheaf_of_types CategoryTheory.isSheaf_iff_isSheaf_of_type
isContinuous_comp' 📖	mathematical	—	IsContinuous	—	isContinuous_comp isContinuous_of_iso
isContinuous_id 📖	mathematical	—	IsContinuous id	—	CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.ObjectProperty.FullSubcategory.property
isContinuous_of_iso 📖	mathematical	—	IsContinuous	—	CategoryTheory.Presieve.isSheaf_iso op_comp_isSheaf_of_types
isContinuous_of_preservesOneHypercovers 📖	mathematical	PreservesOneHypercovers	IsContinuous	—	CategoryTheory.isSheaf_iff_isSheaf_of_type op_comp_isSheaf_of_preservesOneHypercovers
isContinuous_toGrothendieck_of_pullbacksPreservedBy 📖	mathematical	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder CategoryTheory.Precoverage.comap	IsContinuous CategoryTheory.Precoverage.toGrothendieck	—	CategoryTheory.Precoverage.toGrothendieck_toCoverage CategoryTheory.Presieve.isSheaf_coverage CategoryTheory.Precoverage.preservesPairwisePullbacks_of_mem CategoryTheory.Precoverage.hasPairwisePullbacks_of_mem CategoryTheory.Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks CategoryTheory.isSheaf_iff_isSheaf_of_type
op_comp_isSheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf comp Opposite CategoryTheory.Category.opposite op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category	—	op_comp_isSheaf_of_types CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.ObjectProperty.FullSubcategory.property
op_comp_isSheaf_of_isSheaf 📖	mathematical	CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Presheaf.IsSheaf comp Opposite CategoryTheory.Category.opposite op	—	op_comp_isSheaf
op_comp_isSheaf_of_preservesOneHypercovers 📖	mathematical	PreservesOneHypercovers CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Presheaf.IsSheaf comp Opposite CategoryTheory.Category.opposite op	—	CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers
op_comp_isSheaf_of_types 📖	mathematical	—	CategoryTheory.Presieve.IsSheaf comp Opposite CategoryTheory.Category.opposite CategoryTheory.types op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf	—	CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.Presheaf.isSheaf_of_iso_iff CategoryTheory.ObjectProperty.FullSubcategory.property
sheafPushforwardContinuousComp'_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category comp sheafPushforwardContinuous CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom sheafPushforwardContinuousComp' map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	CategoryTheory.Category.id_comp
sheafPushforwardContinuousComp'_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category sheafPushforwardContinuous comp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv sheafPushforwardContinuousComp' map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	CategoryTheory.Category.comp_id
sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf comp sheafPushforwardContinuous CategoryTheory.sheafToPresheaf CategoryTheory.Iso.hom whiskeringLeft op sheafPushforwardContinuousCompSheafToPresheafIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Opposite.unop	—	—
sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf comp sheafPushforwardContinuous CategoryTheory.sheafToPresheaf CategoryTheory.Iso.inv whiskeringLeft op sheafPushforwardContinuousCompSheafToPresheafIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj Opposite.op Opposite.unop	—	—
sheafPushforwardContinuousComp_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category comp sheafPushforwardContinuous CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom isContinuous_comp sheafPushforwardContinuousComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op Opposite.unop	—	isContinuous_comp
sheafPushforwardContinuousComp_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category comp sheafPushforwardContinuous CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv isContinuous_comp sheafPushforwardContinuousComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op Opposite.unop	—	isContinuous_comp
sheafPushforwardContinuousId'_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category sheafPushforwardContinuous id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom sheafPushforwardContinuousId' map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id
sheafPushforwardContinuousId'_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category id sheafPushforwardContinuous CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv sheafPushforwardContinuousId' map Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	CategoryTheory.Category.id_comp
sheafPushforwardContinuousId_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category sheafPushforwardContinuous id isContinuous_id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.hom sheafPushforwardContinuousId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isContinuous_id
sheafPushforwardContinuousId_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category sheafPushforwardContinuous id isContinuous_id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Iso.inv sheafPushforwardContinuousId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isContinuous_id
sheafPushforwardContinuousIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite category CategoryTheory.Presheaf.IsSheaf sheafPushforwardContinuous sheafPushforwardContinuousIso sheafPushforwardContinuousNatTrans CategoryTheory.Iso.inv	—	—
sheafPushforwardContinuousIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite category CategoryTheory.Presheaf.IsSheaf sheafPushforwardContinuous sheafPushforwardContinuousIso sheafPushforwardContinuousNatTrans CategoryTheory.Iso.hom	—	—
sheafPushforwardContinuousNatTrans_app_hom 📖	mathematical	—	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 sheafPushforwardContinuous CategoryTheory.NatTrans.app sheafPushforwardContinuousNatTrans whiskerRight op CategoryTheory.NatTrans.op CategoryTheory.sheafToPresheaf	—	—
sheafPushforwardContinuous_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf comp CategoryTheory.sheafToPresheaf whiskeringLeft op CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj op_comp_isSheaf map sheafPushforwardContinuous Opposite.op Opposite.unop	—	op_comp_isSheaf
sheafPushforwardContinuous_obj_obj_map 📖	mathematical	—	map Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf obj CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category sheafPushforwardContinuous Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
sheafPushforwardContinuous_obj_obj_obj 📖	mathematical	—	obj Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category sheafPushforwardContinuous Opposite.op Opposite.unop	—	—

CategoryTheory.Functor.IsContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_comp_isSheaf_of_types 📖	mathematical	—	CategoryTheory.Presieve.IsSheaf CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf	—	—

CategoryTheory.GrothendieckTopology.OneHypercover

Definitions

Name	Category	Theorems
IsPreservedBy 📖	CompData	1 math math: instIsPreservedById
map 📖	CompOp	1 math math: map_toPreOneHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsPreservedById 📖	mathematical	—	IsPreservedBy CategoryTheory.Functor.id	—	mem₀ mem₁
map_toPreOneHypercover 📖	mathematical	—	toPreOneHypercover CategoryTheory.Functor.obj map CategoryTheory.PreOneHypercover.map	—	—

CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem₀ 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Functor.obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreZeroHypercover.sieve₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.map CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover	—	—
mem₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover CategoryTheory.Functor.map CategoryTheory.PreZeroHypercover.f	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreOneHypercover.sieve₁ CategoryTheory.Functor.obj CategoryTheory.PreOneHypercover.map CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover	—	—

CategoryTheory.PreOneHypercover

Definitions

Name	Category	Theorems
isLimitMapMultiforkEquiv 📖	CompOp	—
map 📖	CompOp	10 math math: map_I₀, map_X, map_p₁, CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁, CategoryTheory.GrothendieckTopology.OneHypercover.map_toPreOneHypercover, CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₀, map_Y, map_f, map_p₂, map_I₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Functor.obj toPreZeroHypercover map	—	—
map_I₁ 📖	mathematical	—	I₁ CategoryTheory.Functor.obj map	—	—
map_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X CategoryTheory.Functor.obj toPreZeroHypercover map	—	—
map_Y 📖	mathematical	—	Y CategoryTheory.Functor.obj map	—	—
map_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f CategoryTheory.Functor.obj toPreZeroHypercover map CategoryTheory.Functor.map CategoryTheory.PreZeroHypercover.X	—	—
map_p₁ 📖	mathematical	—	p₁ CategoryTheory.Functor.obj map CategoryTheory.Functor.map Y CategoryTheory.PreZeroHypercover.X toPreZeroHypercover	—	—
map_p₂ 📖	mathematical	—	p₂ CategoryTheory.Functor.obj map CategoryTheory.Functor.map Y CategoryTheory.PreZeroHypercover.X toPreZeroHypercover	—	—

---

← Back to Index