Continuous

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

Statistics

Metric	Count
Definitions IsContinuous, PreservesOneHypercovers, sheafPushforwardContinuous, sheafPushforwardContinuousComp, sheafPushforwardContinuousComp', sheafPushforwardContinuousCompSheafToPresheafIso, sheafPushforwardContinuousId, sheafPushforwardContinuousId', sheafPushforwardContinuousIso, sheafPushforwardContinuousNatTrans, IsPreservedBy, map, isLimitMapMultiforkEquiv, map	14
Theorems op_comp_isSheaf_of_types, 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_preservesOneHypercovers, op_comp_isSheaf_of_types, sheafPushforwardContinuousComp'_hom_app_val_app, sheafPushforwardContinuousComp'_inv_app_val_app, sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, sheafPushforwardContinuousComp_hom_app_val_app, sheafPushforwardContinuousComp_inv_app_val_app, sheafPushforwardContinuousId'_hom_app_val_app, sheafPushforwardContinuousId'_inv_app_val_app, sheafPushforwardContinuousId_hom_app_val_app, sheafPushforwardContinuousId_inv_app_val_app, sheafPushforwardContinuousIso_hom, sheafPushforwardContinuousIso_inv, sheafPushforwardContinuousNatTrans_app_val, sheafPushforwardContinuous_map_val_app, sheafPushforwardContinuous_obj_val_map, sheafPushforwardContinuous_obj_val_obj, mem₀, mem₁, instIsPreservedById, map_toPreOneHypercover, map_I₀, map_I₁, map_X, map_Y, map_f, map_p₁, map_p₂	40
Total	54

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsContinuous 📖	CompData	21 math math: Topology.IsOpenEmbedding.functor_isContinuous, AlgebraicGeometry.Scheme.Hom.instIsContinuousOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat, CategoryTheory.GrothendieckTopology.instIsContinuousOverStarOver, instIsContinuousCompId_1, TopologicalSpace.Opens.instIsContinuousCompGrothendieckTopology, instIsContinuousOfPreservesOneHypercovers, CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver, isContinuous_of_coverPreserving, isContinuous_id, IsCoverDense.isContinuous, 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
PreservesOneHypercovers 📖	MathDef	—
sheafPushforwardContinuous 📖	CompOp	55 math math: CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_val_app, SheafOfModules.pushforward_assoc, IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, sheafPushforwardContinuousIso_inv, IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous, sheafPushforwardContinuousComp'_inv_app_val_app, SheafOfModules.pushforwardNatIso_inv, CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_val_app, SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous, sheafAdjunctionCocontinuous_counit_app_val, sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app, sheafPushforwardContinuousNatTrans_app_val, sheafPushforwardContinuous_map_val_app, IsCoverDense.faithful_sheafPushforwardContinuous, SheafOfModules.pushforwardComp_inv_app_val_app, SheafOfModules.pushforwardNatTrans_id, sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, IsDenseSubsite.sheafEquiv_inverse, sheafPushforwardContinuous_obj_val_map, SheafOfModules.conjugateEquiv_pullbackComp_inv, sheafPushforwardContinuousComp_inv_app_val_app, sheafPushforwardContinuousComp_hom_app_val_app, sheafPushforwardContinuous_obj_val_obj, SheafOfModules.pushforward_map_val, SheafOfModules.pushforwardComp_hom_app_val_app, sheafPushforwardContinuousId_hom_app_val_app, sheafPushforwardContinuousId'_inv_app_val_app, toSheafify_pullbackSheafificationCompatibility, SheafOfModules.pushforwardCongr_symm, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, SheafOfModules.pullback_assoc, CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_val_app, sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app, SheafOfModules.pushforwardNatTrans_app_val_app, sheafPushforwardContinuousIso_hom, CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_val_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_val_app, sheafPushforwardContinuousId_inv_app_val_app, SheafOfModules.pushforwardNatTrans_app_val_app_apply, sheafAdjunctionCocontinuous_homEquiv_apply_val, sheafPushforwardContinuousId'_hom_app_val_app, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app, SheafOfModules.pushforwardNatIso_hom, CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app, pushforwardContinuousSheafificationCompatibility_hom_app_val, IsDenseSubsite.full_sheafPushforwardContinuous, sheafPushforwardContinuousComp'_hom_app_val_app, CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_val_app, sheafAdjunctionCocontinuous_unit_app_val, SheafOfModules.pushforward_obj_val, IsDenseSubsite.faithful_sheafPushforwardContinuous, SheafOfModules.pushforwardNatTrans_comp, IsCoverDense.full_sheafPushforwardContinuous
sheafPushforwardContinuousComp 📖	CompOp	2 math math: sheafPushforwardContinuousComp_inv_app_val_app, sheafPushforwardContinuousComp_hom_app_val_app
sheafPushforwardContinuousComp' 📖	CompOp	2 math math: sheafPushforwardContinuousComp'_inv_app_val_app, sheafPushforwardContinuousComp'_hom_app_val_app
sheafPushforwardContinuousCompSheafToPresheafIso 📖	CompOp	2 math math: sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app, sheafPushforwardContinuousCompSheafToPresheafIso_hom_app_app
sheafPushforwardContinuousId 📖	CompOp	2 math math: sheafPushforwardContinuousId_hom_app_val_app, sheafPushforwardContinuousId_inv_app_val_app
sheafPushforwardContinuousId' 📖	CompOp	2 math math: sheafPushforwardContinuousId'_inv_app_val_app, sheafPushforwardContinuousId'_hom_app_val_app
sheafPushforwardContinuousIso 📖	CompOp	2 math math: sheafPushforwardContinuousIso_inv, sheafPushforwardContinuousIso_hom
sheafPushforwardContinuousNatTrans 📖	CompOp	9 math math: sheafPushforwardContinuousIso_inv, SheafOfModules.pushforwardNatIso_inv, sheafPushforwardContinuousNatTrans_app_val, 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
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.Sheaf.cond
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.Sheaf.val	—	op_comp_isSheaf_of_types CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.Sheaf.cond
op_comp_isSheaf_of_preservesOneHypercovers 📖	mathematical	PreservesOneHypercovers 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.Sheaf.val	—	IsContinuous.op_comp_isSheaf_of_types
sheafPushforwardContinuousComp'_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf comp sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.hom CategoryTheory.Functor category 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardContinuous comp CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.inv CategoryTheory.Functor category 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.Sheaf.instCategorySheaf CategoryTheory.Functor category comp sheafPushforwardContinuous CategoryTheory.sheafToPresheaf CategoryTheory.Iso.hom whiskeringLeft op sheafPushforwardContinuousCompSheafToPresheafIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.val Opposite.op Opposite.unop	—	—
sheafPushforwardContinuousCompSheafToPresheafIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor category comp sheafPushforwardContinuous CategoryTheory.sheafToPresheaf CategoryTheory.Iso.inv whiskeringLeft op sheafPushforwardContinuousCompSheafToPresheafIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Sheaf.val Opposite.op Opposite.unop	—	—
sheafPushforwardContinuousComp_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf comp sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.hom CategoryTheory.Functor category isContinuous_comp sheafPushforwardContinuousComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op Opposite.unop	—	isContinuous_comp
sheafPushforwardContinuousComp_inv_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf comp sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.inv CategoryTheory.Functor category isContinuous_comp sheafPushforwardContinuousComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Opposite.op Opposite.unop	—	isContinuous_comp
sheafPushforwardContinuousId'_hom_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardContinuous id CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.hom CategoryTheory.Functor category 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf id sheafPushforwardContinuous CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.inv CategoryTheory.Functor category 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_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardContinuous id isContinuous_id CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.hom CategoryTheory.Functor category sheafPushforwardContinuousId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isContinuous_id
sheafPushforwardContinuousId_inv_app_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardContinuous id isContinuous_id CategoryTheory.Sheaf.Hom.val CategoryTheory.Iso.inv CategoryTheory.Functor category sheafPushforwardContinuousId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isContinuous_id
sheafPushforwardContinuousIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf category sheafPushforwardContinuous sheafPushforwardContinuousIso sheafPushforwardContinuousNatTrans CategoryTheory.Iso.inv	—	—
sheafPushforwardContinuousIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf category sheafPushforwardContinuous sheafPushforwardContinuousIso sheafPushforwardContinuousNatTrans CategoryTheory.Iso.hom	—	—
sheafPushforwardContinuousNatTrans_app_val 📖	mathematical	—	CategoryTheory.Sheaf.Hom.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardContinuous CategoryTheory.NatTrans.app sheafPushforwardContinuousNatTrans whiskerRight Opposite CategoryTheory.Category.opposite op CategoryTheory.NatTrans.op CategoryTheory.Sheaf.val	—	—
sheafPushforwardContinuous_map_val_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite obj CategoryTheory.Functor category whiskeringLeft op CategoryTheory.Sheaf.val CategoryTheory.Sheaf.Hom.val comp op_comp_isSheaf map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardContinuous Opposite.op Opposite.unop	—	op_comp_isSheaf
sheafPushforwardContinuous_obj_val_map 📖	mathematical	—	map Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val obj CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPushforwardContinuous Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.Hom.unop	—	—
sheafPushforwardContinuous_obj_val_obj 📖	mathematical	—	obj Opposite CategoryTheory.Category.opposite CategoryTheory.Sheaf.val CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf 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.Sheaf.val	—	—

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.PreOneHypercover.map	—	—

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