One

📁 Source: Mathlib/CategoryTheory/Sites/Hypercover/One.lean

Statistics

Metric	Count
Definitions oneHypercover, preOneHypercover, OneHypercover, amalgamate, instCategory, inter, isLimitMultifork, isoMk, mk', multiforkLift, toPreOneHypercover, toZeroHypercover, trivial, PreOneHypercover, comp, h₁, id, mapMultiforkOfIsLimit, s₁, s₁', toHom, I₁, I₁', Y, Y', forkOfIsColimit, instCategory, instUniqueLMulticospanShapeSigmaOfIsColimit, instUniqueRMulticospanShapeSigmaOfIsColimit, inter, interFst, interLift, interSnd, isLimitMultiforkEquivIsLimitFork, isLimitSigmaOfIsColimitEquiv, multicospanIndex, multicospanShape, multifork, oneToZero, p₁, p₂, sieve₁, sieve₁', sigmaOfIsColimit, toPreZeroHypercover, toPullback, trivial, toPreOneHypercover, toOneHypercover	49
Theorems oneHypercover_toPreOneHypercover, preOneHypercover_I₀, preOneHypercover_I₁, preOneHypercover_X, preOneHypercover_Y, preOneHypercover_f, preOneHypercover_p₁, preOneHypercover_p₂, preOneHypercover_sieve₀, preOneHypercover_sieve₁, arrowsCompatible, comp_h₀, comp_h₁, comp_s₀, comp_s₁, id_h₀, id_h₁, id_s₀, id_s₁, instNonempty, inter_toPreOneHypercover, isSheafFor_presieve₀, isoMk_hom, isoMk_inv, map_amalgamate, mem_sieve₁', mem₀, mem₁, mk'_toPreOneHypercover, multiforkLift_map, multiforkLift_map_assoc, toZeroHypercover_toPreZeroHypercover, trivial_toPreOneHypercover, comp_h₀, comp_h₁, comp_s₀, comp_s₁, ext, ext_iff, id_h₀, id_h₁, id_s₀, id_s₁, mapMultiforkOfIsLimit_ι, mapMultiforkOfIsLimit_ι_assoc, w₁₁, w₁₁_assoc, w₁₂, w₁₂_assoc, Y'_apply, comp_h₀, comp_h₁, comp_s₀, comp_s₁, forkOfIsColimit_pt, forkOfIsColimit_ι_map_inj, forkOfIsColimit_ι_map_inj_assoc, id_h₀, id_h₁, id_s₀, id_s₁, instNonempty, interFst_s₁, interFst_toHom, interSnd_s₁, interSnd_toHom, inter_I₁, inter_Y, inter_p₁, inter_p₂, inter_toPreZeroHypercover, multicospanIndex_fst, multicospanIndex_left, multicospanIndex_right, multicospanIndex_snd, multicospanShape_L, multicospanShape_R, multicospanShape_fst, multicospanShape_snd, multifork_ι, oneToZero_map, oneToZero_obj, p₁_sigmaOfIsColimit, p₁_sigmaOfIsColimit_assoc, p₂_sigmaOfIsColimit, p₂_sigmaOfIsColimit_assoc, sieve₀_trivial, sieve₁'_eq_sieve₁, sieve₁_apply, sieve₁_eq_pullback_sieve₁', sieve₁_inter, sieve₁_trivial, sigmaOfIsColimit_Y, sigmaOfIsColimit_toPreZeroHypercover, trivial_I₁, trivial_Y, trivial_p₁, trivial_p₂, trivial_toPreZeroHypercover, w, ext_of_isSeparatedFor, toPreOneHypercover_I₁, toPreOneHypercover_Y, toPreOneHypercover_p₁, toPreOneHypercover_p₂, toPreOneHypercover_toPreZeroHypercover, toOneHypercover_toPreOneHypercover, instHasPullbacksToPreOneHypercover, sieve₁'_toPreOneHypercover_eq_top	109
Total	158

CategoryTheory

Definitions

Name	Category	Theorems
PreOneHypercover 📖	CompData	13 math math: PreOneHypercover.comp_s₀, GrothendieckTopology.OneHypercover.isoMk_inv, GrothendieckTopology.OneHypercover.isoMk_hom, PreOneHypercover.oneToZero_obj, PreOneHypercover.id_h₀, PreOneHypercover.id_s₁, PreOneHypercover.comp_s₁, PreOneHypercover.instNonempty, PreOneHypercover.id_s₀, PreOneHypercover.oneToZero_map, PreOneHypercover.comp_h₀, PreOneHypercover.id_h₁, PreOneHypercover.comp_h₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasPullbacksToPreOneHypercover 📖	mathematical	PreZeroHypercover.HasPullbacks	PreOneHypercover.toPreZeroHypercover PreZeroHypercover.toPreOneHypercover	—	—
sieve₁'_toPreOneHypercover_eq_top 📖	mathematical	PreZeroHypercover.HasPullbacks	PreOneHypercover.sieve₁' PreZeroHypercover.toPreOneHypercover instHasPullbacksToPreOneHypercover Top.top Sieve Limits.pullback PreZeroHypercover.X PreOneHypercover.toPreZeroHypercover PreZeroHypercover.f OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	instHasPullbacksToPreOneHypercover eq_top_iff Presieve.ofArrows.mk' Limits.pullback.hom_ext Category.id_comp Limits.pullback.lift_fst_snd Category.comp_id

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
OneHypercover 📖	CompData	13 math math: OneHypercover.comp_h₁, OneHypercover.isoMk_inv, OneHypercover.isoMk_hom, OneHypercover.instNonempty, OneHypercover.id_s₁, OneHypercover.id_h₀, OneHypercover.id_s₀, OneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.Homotopy.map_eq_map, OneHypercover.comp_h₀, HOneHypercover.isCofiltered_of_hasPullbacks, OneHypercover.comp_s₀, OneHypercover.id_h₁

CategoryTheory.GrothendieckTopology.Cover

Definitions

Name	Category	Theorems
oneHypercover 📖	CompOp	1 math math: oneHypercover_toPreOneHypercover
preOneHypercover 📖	CompOp	10 math math: preOneHypercover_Y, preOneHypercover_I₀, preOneHypercover_p₂, preOneHypercover_sieve₀, preOneHypercover_I₁, preOneHypercover_p₁, preOneHypercover_f, preOneHypercover_sieve₁, preOneHypercover_X, oneHypercover_toPreOneHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
oneHypercover_toPreOneHypercover 📖	mathematical	—	CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover oneHypercover preOneHypercover	—	—
preOneHypercover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover preOneHypercover Arrow	—	—
preOneHypercover_I₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.I₁ preOneHypercover Arrow.Relation	—	—
preOneHypercover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover preOneHypercover Arrow.Y	—	—
preOneHypercover_Y 📖	mathematical	—	CategoryTheory.PreOneHypercover.Y preOneHypercover Arrow.Relation.Z	—	—
preOneHypercover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f CategoryTheory.PreOneHypercover.toPreZeroHypercover preOneHypercover Arrow.f	—	—
preOneHypercover_p₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.p₁ preOneHypercover Arrow.Relation.g₁	—	—
preOneHypercover_p₂ 📖	mathematical	—	CategoryTheory.PreOneHypercover.p₂ preOneHypercover Arrow.Relation.g₂	—	—
preOneHypercover_sieve₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.sieve₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover preOneHypercover CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	—	CategoryTheory.Sieve.ext CategoryTheory.Sieve.downward_closed Arrow.hf
preOneHypercover_sieve₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Arrow.Y Arrow.f	CategoryTheory.PreOneHypercover.sieve₁ preOneHypercover Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Sieve.ext

CategoryTheory.GrothendieckTopology.OneHypercover

Definitions

Name	Category	Theorems
amalgamate 📖	CompOp	1 math math: map_amalgamate
instCategory 📖	CompOp	12 math math: comp_h₁, isoMk_inv, isoMk_hom, id_s₁, id_h₀, id_s₀, comp_s₁, CategoryTheory.PreOneHypercover.Homotopy.map_eq_map, comp_h₀, CategoryTheory.GrothendieckTopology.HOneHypercover.isCofiltered_of_hasPullbacks, comp_s₀, id_h₁
inter 📖	CompOp	1 math math: inter_toPreOneHypercover
isLimitMultifork 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_inv, isoMk_hom
mk' 📖	CompOp	1 math math: mk'_toPreOneHypercover
multiforkLift 📖	CompOp	2 math math: multiforkLift_map, multiforkLift_map_assoc
toPreOneHypercover 📖	CompOp	37 math math: AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₁, comp_h₁, mem₀, isoMk_inv, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff, isoMk_hom, multiforkLift_map, mem_sieve₁', exists_nonempty_homotopy, CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover_toPreOneHypercover, mk'_toPreOneHypercover, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, isSheafFor_presieve₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, id_s₁, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, map_toPreOneHypercover, IsPreservedBy.mem₀, id_h₀, id_s₀, comp_s₁, trivial_toPreOneHypercover, AlgebraicGeometry.Scheme.GlueData.oneHypercover_X, AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀, cylinder_toPreOneHypercover, comp_h₀, CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover_toPreOneHypercover, AlgebraicGeometry.Scheme.GlueData.oneHypercover_f, comp_s₀, AlgebraicGeometry.Scheme.GlueData.oneHypercover_Y, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₁, CategoryTheory.GrothendieckTopology.Cover.oneHypercover_toPreOneHypercover, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, toZeroHypercover_toPreZeroHypercover, multiforkLift_map_assoc, id_h₁
toZeroHypercover 📖	CompOp	1 math math: toZeroHypercover_toPreZeroHypercover
trivial 📖	CompOp	1 math math: trivial_toPreOneHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowsCompatible 📖	mathematical	CategoryTheory.Presieve.IsSeparated CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreOneHypercover.Y Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreOneHypercover.p₂	CategoryTheory.Presieve.Arrows.Compatible CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Presieve.IsSeparatedFor.ext mem₁ CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp
comp_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreOneHypercover.Hom.toHom CategoryTheory.CategoryStruct.comp CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.Hom.s₀	—	—
comp_h₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.Hom.h₁ toPreOneHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.Hom.toHom CategoryTheory.PreOneHypercover.Hom.s₁	—	—
comp_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreOneHypercover.Hom.toHom CategoryTheory.CategoryStruct.comp CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
comp_s₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.Hom.s₁ toPreOneHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.Hom.toHom	—	—
id_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreOneHypercover.Hom.toHom CategoryTheory.CategoryStruct.id CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.X	—	—
id_h₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.Hom.h₁ toPreOneHypercover CategoryTheory.CategoryStruct.id CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreOneHypercover.Y	—	—
id_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreOneHypercover.Hom.toHom CategoryTheory.CategoryStruct.id CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
id_s₁ 📖	mathematical	—	CategoryTheory.PreOneHypercover.Hom.s₁ toPreOneHypercover CategoryTheory.CategoryStruct.id CategoryTheory.GrothendieckTopology.OneHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
instNonempty 📖	mathematical	—	CategoryTheory.GrothendieckTopology.OneHypercover	—	—
inter_toPreOneHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreZeroHypercover.f CategoryTheory.PreOneHypercover.Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.p₁	inter CategoryTheory.PreOneHypercover.inter	—	—
isSheafFor_presieve₀ 📖	mathematical	CategoryTheory.Presieve.IsSheaf	CategoryTheory.Presieve.IsSheafFor CategoryTheory.PreZeroHypercover.presieve₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover	—	CategoryTheory.Presieve.isSheafFor_iff_generate mem₀
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.GrothendieckTopology.OneHypercover instCategory isoMk CategoryTheory.PreOneHypercover CategoryTheory.PreOneHypercover.instCategory toPreOneHypercover	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.GrothendieckTopology.OneHypercover instCategory isoMk CategoryTheory.PreOneHypercover CategoryTheory.PreOneHypercover.instCategory toPreOneHypercover	—	—
map_amalgamate 📖	mathematical	CategoryTheory.Presieve.IsSheaf CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreOneHypercover.Y Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreOneHypercover.p₂	CategoryTheory.PreZeroHypercover.f amalgamate	—	isSheafFor_presieve₀ amalgamate.eq_1 CategoryTheory.Presieve.IsSheafFor.valid_glue
mem_sieve₁' 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreZeroHypercover.f Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreOneHypercover.sieve₁'	—	CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁ mem₁ CategoryTheory.Limits.pullback.condition
mem₀ 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreZeroHypercover.sieve₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover	—	—
mem₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover CategoryTheory.PreZeroHypercover.f	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreOneHypercover.sieve₁	—	—
mk'_toPreOneHypercover 📖	mathematical	CategoryTheory.PreZeroHypercover.HasPullbacks CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.PreZeroHypercover.sieve₀ CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f CategoryTheory.PreOneHypercover.sieve₁'	toPreOneHypercover mk'	—	—
multiforkLift_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.PreOneHypercover.multicospanShape toPreOneHypercover CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.PreOneHypercover.multicospanIndex CategoryTheory.Sheaf.val CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover multiforkLift CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Presheaf.IsSheaf.amalgamateOfArrows_map CategoryTheory.Sheaf.cond mem₀
multiforkLift_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.PreOneHypercover.multicospanShape toPreOneHypercover CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.PreOneHypercover.multicospanIndex CategoryTheory.Sheaf.val CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op multiforkLift CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' multiforkLift_map
toZeroHypercover_toPreZeroHypercover 📖	mathematical	—	CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover CategoryTheory.GrothendieckTopology.toPrecoverage toZeroHypercover CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover	—	—
trivial_toPreOneHypercover 📖	mathematical	—	toPreOneHypercover trivial CategoryTheory.PreOneHypercover.trivial	—	—

CategoryTheory.PreOneHypercover

Definitions

Name	Category	Theorems
I₁ 📖	CompOp	39 math math: AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₁, forkOfIsColimit_ι_map_inj_assoc, trivial_I₁, forkOfIsColimit_pt, p₁_sigmaOfIsColimit_assoc, inter_I₁, multicospanIndex_fst, cylinder_X, cylinderHom_h₁, multicospanIndex_right, CategoryTheory.PreZeroHypercover.toPreOneHypercover_I₁, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₁, multicospanShape_fst, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₁, multicospanIndex_snd, p₁_sigmaOfIsColimit, cylinder_I₀, inter_p₂, Y'_apply, cylinder_f, cylinder_I₁, multicospanShape_snd, sieve₁_apply, inter_Y, sieve₁'_cylinder, interSnd_s₁, toPullback_cylinder, inter_p₁, cylinder_p₁, cylinder_p₂, cylinderHom_s₁, interFst_s₁, forkOfIsColimit_ι_map_inj, cylinderHom_s₀, p₂_sigmaOfIsColimit, p₂_sigmaOfIsColimit_assoc, map_I₁, cylinderHom_h₀, cylinder_Y
I₁' 📖	CompOp	9 math math: forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, p₁_sigmaOfIsColimit_assoc, p₁_sigmaOfIsColimit, multicospanShape_R, sigmaOfIsColimit_Y, forkOfIsColimit_ι_map_inj, p₂_sigmaOfIsColimit, p₂_sigmaOfIsColimit_assoc
Y 📖	CompOp	39 math math: CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_Y, Homotopy.wl, Hom.w₁₁, multicospanIndex_fst, cylinderHom_h₁, multicospanIndex_right, Homotopy.wl_assoc, multicospanIndex_snd, map_p₁, p₁_sigmaOfIsColimit, Y'_apply, w, sigmaOfIsColimit_Y, Hom.w₁₂_assoc, sieve₁_apply, Hom.id_h₁, sieve₁'_cylinder, toPullback_cylinder, Hom.w₁₂, Homotopy.wr, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_Y, sieve₁_inter, cylinder_p₁, AlgebraicGeometry.Scheme.GlueData.oneHypercover_Y, map_Y, cylinder_p₂, trivial_Y, Hom.comp_h₁, id_h₁, CategoryTheory.PreZeroHypercover.toPreOneHypercover_Y, p₂_sigmaOfIsColimit, Hom.w₁₁_assoc, Homotopy.wr_assoc, map_p₂, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₁, comp_h₁, cylinderHom_h₀, cylinder_Y
Y' 📖	CompOp	9 math math: forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, p₁_sigmaOfIsColimit_assoc, p₁_sigmaOfIsColimit, Y'_apply, sigmaOfIsColimit_Y, forkOfIsColimit_ι_map_inj, p₂_sigmaOfIsColimit, p₂_sigmaOfIsColimit_assoc
forkOfIsColimit 📖	CompOp	3 math math: forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, forkOfIsColimit_ι_map_inj
instCategory 📖	CompOp	12 math math: comp_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_inv, CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_hom, oneToZero_obj, id_h₀, id_s₁, comp_s₁, id_s₀, oneToZero_map, comp_h₀, id_h₁, comp_h₁
instUniqueLMulticospanShapeSigmaOfIsColimit 📖	CompOp	—
instUniqueRMulticospanShapeSigmaOfIsColimit 📖	CompOp	—
inter 📖	CompOp	11 math math: inter_I₁, inter_toPreZeroHypercover, interSnd_toHom, inter_p₂, interFst_toHom, inter_Y, CategoryTheory.GrothendieckTopology.OneHypercover.inter_toPreOneHypercover, interSnd_s₁, inter_p₁, sieve₁_inter, interFst_s₁
interFst 📖	CompOp	2 math math: interFst_toHom, interFst_s₁
interLift 📖	CompOp	—
interSnd 📖	CompOp	2 math math: interSnd_toHom, interSnd_s₁
isLimitMultiforkEquivIsLimitFork 📖	CompOp	—
isLimitSigmaOfIsColimitEquiv 📖	CompOp	—
multicospanIndex 📖	CompOp	12 math math: multicospanIndex_fst, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, multicospanIndex_right, multifork_ι, multicospanIndex_snd, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, multicospanIndex_left, Hom.mapMultiforkOfIsLimit_ι_assoc, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, Hom.mapMultiforkOfIsLimit_ι, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc
multicospanShape 📖	CompOp	16 math math: multicospanIndex_fst, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, multicospanIndex_right, multicospanShape_fst, multifork_ι, multicospanIndex_snd, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, multicospanShape_L, multicospanShape_R, multicospanIndex_left, multicospanShape_snd, Hom.mapMultiforkOfIsLimit_ι_assoc, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, Hom.mapMultiforkOfIsLimit_ι, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc
multifork 📖	CompOp	4 math math: CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff, multifork_ι, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff
oneToZero 📖	CompOp	2 math math: oneToZero_obj, oneToZero_map
p₁ 📖	CompOp	24 math math: forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, Homotopy.wl, p₁_sigmaOfIsColimit_assoc, Hom.w₁₁, multicospanIndex_fst, trivial_p₁, cylinderHom_h₁, CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₁, Homotopy.wl_assoc, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁, map_p₁, p₁_sigmaOfIsColimit, w, sieve₁_apply, toPullback_cylinder, sieve₁_inter, cylinder_p₁, cylinder_p₂, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₁, forkOfIsColimit_ι_map_inj, Hom.w₁₁_assoc, cylinder_Y, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_p₁
p₂ 📖	CompOp	24 math math: forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, cylinderHom_h₁, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_p₂, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂, multicospanIndex_snd, inter_p₂, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, w, trivial_p₂, Hom.w₁₂_assoc, sieve₁_apply, toPullback_cylinder, Hom.w₁₂, Homotopy.wr, cylinder_p₁, cylinder_p₂, forkOfIsColimit_ι_map_inj, p₂_sigmaOfIsColimit, p₂_sigmaOfIsColimit_assoc, Homotopy.wr_assoc, map_p₂, CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₂, cylinder_Y
sieve₁ 📖	CompOp	9 math math: CategoryTheory.Functor.OneHypercoverDenseData.mem₁, sieve₁'_eq_sieve₁, sieve₁_eq_pullback_sieve₁', CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁, CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁, sieve₁_apply, sieve₁_inter, sieve₁_trivial, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
sieve₁' 📖	CompOp	6 math math: CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', sieve₁'_eq_sieve₁, sieve₁_eq_pullback_sieve₁', sieve₀_cylinder, sieve₁'_cylinder, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top
sigmaOfIsColimit 📖	CompOp	6 math math: p₁_sigmaOfIsColimit_assoc, p₁_sigmaOfIsColimit, sigmaOfIsColimit_Y, sigmaOfIsColimit_toPreZeroHypercover, p₂_sigmaOfIsColimit, p₂_sigmaOfIsColimit_assoc
toPreZeroHypercover 📖	CompOp	94 math math: forkOfIsColimit_ι_map_inj_assoc, CategoryTheory.PreZeroHypercover.toPreOneHypercover_toPreZeroHypercover, Hom.comp_s₁, Hom.ext_iff, forkOfIsColimit_pt, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, comp_s₀, Homotopy.wl, p₁_sigmaOfIsColimit_assoc, Hom.w₁₁, CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, multicospanIndex_fst, cylinder_X, cylinderHom_h₁, Hom.comp_h₀, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₀, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, map_I₀, oneToZero_obj, map_X, multicospanIndex_right, CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', Homotopy.wl_assoc, multicospanShape_fst, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₀, multifork_ι, trivial_toPreZeroHypercover, id_h₀, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f, multicospanIndex_snd, sieve₁'_eq_sieve₁, map_p₁, Hom.comp_s₀, p₁_sigmaOfIsColimit, CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_presieve₀, multicospanShape_L, cylinder_I₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, Y'_apply, multicospanIndex_left, cylinder_f, comp_s₁, cylinder_I₁, CategoryTheory.instHasPullbacksToPreOneHypercover, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, id_s₀, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₀, w, CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₀, Hom.id_h₀, CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X, sieve₀_cylinder, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_X, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_f, CategoryTheory.GrothendieckTopology.OneHypercover.id_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁, multicospanShape_snd, Hom.w₁₂_assoc, sieve₁_apply, AlgebraicGeometry.Scheme.GlueData.oneHypercover_X, sieve₁'_cylinder, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, toPullback_cylinder, sigmaOfIsColimit_toPreZeroHypercover, AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀, Hom.w₁₂, comp_h₀, Homotopy.wr, AlgebraicGeometry.Scheme.GlueData.oneHypercover_f, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₀, cylinder_p₁, Hom.mapMultiforkOfIsLimit_ι_assoc, cylinder_p₂, map_f, cylinderHom_s₁, Hom.comp_h₁, forkOfIsColimit_ι_map_inj, cylinderHom_s₀, Hom.mapMultiforkOfIsLimit_ι, sieve₀_trivial, p₂_sigmaOfIsColimit, CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover_toPreZeroHypercover, Hom.w₁₁_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, p₂_sigmaOfIsColimit_assoc, Homotopy.wr_assoc, map_p₂, comp_h₁, Hom.id_s₀, cylinderHom_h₀, cylinder_Y
toPullback 📖	CompOp	7 math math: cylinderHom_h₁, sieve₁'_cylinder, toPullback_cylinder, cylinder_p₁, cylinder_p₂, cylinderHom_h₀, cylinder_Y
trivial 📖	CompOp	8 math math: trivial_I₁, trivial_p₁, trivial_toPreZeroHypercover, CategoryTheory.GrothendieckTopology.OneHypercover.trivial_toPreOneHypercover, trivial_p₂, trivial_Y, sieve₀_trivial, sieve₁_trivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Y'_apply 📖	mathematical	—	Y' Y CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁	—	—
comp_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ toPreZeroHypercover Hom.toHom CategoryTheory.CategoryStruct.comp CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.Hom.s₀	—	—
comp_h₁ 📖	mathematical	—	Hom.h₁ CategoryTheory.CategoryStruct.comp CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory Y CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom Hom.s₁	—	—
comp_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.CategoryStruct.comp CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
comp_s₁ 📖	mathematical	—	Hom.s₁ CategoryTheory.CategoryStruct.comp CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom	—	—
forkOfIsColimit_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.PreZeroHypercover.X I₁' Y' CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cofan.IsColimit.desc CategoryTheory.CategoryStruct.comp I₁ p₁ p₂ forkOfIsColimit	—	—
forkOfIsColimit_ι_map_inj 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.PreZeroHypercover.X I₁' Y' CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Cofan.IsColimit.desc I₁ p₁ p₂ forkOfIsColimit CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Limits.Cofan.IsColimit.fac
forkOfIsColimit_ι_map_inj_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.PreZeroHypercover.X I₁' Y' CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Cofan.IsColimit.desc I₁ p₁ p₂ forkOfIsColimit CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
id_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ toPreZeroHypercover Hom.toHom CategoryTheory.CategoryStruct.id CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.X	—	—
id_h₁ 📖	mathematical	—	Hom.h₁ CategoryTheory.CategoryStruct.id CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory Y	—	—
id_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.CategoryStruct.id CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
id_s₁ 📖	mathematical	—	Hom.s₁ CategoryTheory.CategoryStruct.id CategoryTheory.PreOneHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
instNonempty 📖	mathematical	—	CategoryTheory.PreOneHypercover	—	—
interFst_s₁ 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	Hom.s₁ inter interFst I₁ CategoryTheory.PreZeroHypercover.I₀	—	—
interFst_toHom 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	Hom.toHom inter interFst CategoryTheory.PreZeroHypercover.interFst	—	—
interSnd_s₁ 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	Hom.s₁ inter interSnd I₁ CategoryTheory.PreZeroHypercover.I₀	—	—
interSnd_toHom 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	Hom.toHom inter interSnd CategoryTheory.PreZeroHypercover.interSnd	—	—
inter_I₁ 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	I₁ inter CategoryTheory.PreZeroHypercover.I₀	—	—
inter_Y 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	inter CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.I₀ I₁	—	—
inter_p₁ 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	inter CategoryTheory.Limits.pullback.map CategoryTheory.PreZeroHypercover.I₀ I₁ DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.bind CategoryTheory.PreZeroHypercover.pullback₁ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd CategoryTheory.CategoryStruct.id	—	—
inter_p₂ 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	p₂ inter CategoryTheory.Limits.pullback.map CategoryTheory.PreZeroHypercover.I₀ I₁ DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.bind CategoryTheory.PreZeroHypercover.pullback₁ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd CategoryTheory.CategoryStruct.id	—	—
inter_toPreZeroHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	inter CategoryTheory.PreZeroHypercover.inter	—	—
multicospanIndex_fst 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.fst multicospanShape multicospanIndex CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.Limits.MulticospanShape.fst Y CategoryTheory.PreZeroHypercover.I₀ I₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct p₁	—	—
multicospanIndex_left 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.left multicospanShape multicospanIndex CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.PreZeroHypercover.X toPreZeroHypercover	—	—
multicospanIndex_right 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.right multicospanShape multicospanIndex CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op Y CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁	—	—
multicospanIndex_snd 📖	mathematical	—	CategoryTheory.Limits.MulticospanIndex.snd multicospanShape multicospanIndex CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.Limits.MulticospanShape.snd Y CategoryTheory.PreZeroHypercover.I₀ I₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct p₂	—	—
multicospanShape_L 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.L multicospanShape CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover	—	—
multicospanShape_R 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.R multicospanShape I₁'	—	—
multicospanShape_fst 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.fst multicospanShape CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁	—	—
multicospanShape_snd 📖	mathematical	—	CategoryTheory.Limits.MulticospanShape.snd multicospanShape CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁	—	—
multifork_ι 📖	mathematical	—	CategoryTheory.Limits.Multifork.ι multicospanShape multicospanIndex multifork CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.PreZeroHypercover.X toPreZeroHypercover Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	—
oneToZero_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.instCategory oneToZero Hom.toHom	—	—
oneToZero_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.instCategory oneToZero toPreZeroHypercover	—	—
p₁_sigmaOfIsColimit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y' CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₁' CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.PreZeroHypercover.X toPreZeroHypercover sigmaOfIsColimit p₁ Y CategoryTheory.PreZeroHypercover.I₀ I₁	—	CategoryTheory.Limits.Cofan.IsColimit.fac
p₁_sigmaOfIsColimit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y' CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₁' CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.PreZeroHypercover.X toPreZeroHypercover sigmaOfIsColimit p₁ CategoryTheory.PreZeroHypercover.I₀ I₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₁_sigmaOfIsColimit
p₂_sigmaOfIsColimit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y' CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₁' CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.PreZeroHypercover.X toPreZeroHypercover sigmaOfIsColimit p₂ Y CategoryTheory.PreZeroHypercover.I₀ I₁	—	CategoryTheory.Limits.Cofan.IsColimit.fac
p₂_sigmaOfIsColimit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y' CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₁' CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.PreZeroHypercover.X toPreZeroHypercover sigmaOfIsColimit p₂ CategoryTheory.PreZeroHypercover.I₀ I₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₂_sigmaOfIsColimit
sieve₀_trivial 📖	mathematical	—	CategoryTheory.PreZeroHypercover.sieve₀ toPreZeroHypercover trivial Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.PreZeroHypercover.sieve₀.eq_1 CategoryTheory.Sieve.ofArrows.eq_1 CategoryTheory.PreZeroHypercover.presieve₀.eq_1 CategoryTheory.PreZeroHypercover.presieve₀_singleton CategoryTheory.Sieve.generate_of_singleton_isSplitEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.IsIso.id
sieve₁'_eq_sieve₁ 📖	mathematical	—	sieve₁' sieve₁ CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Sieve.pullback_id CategoryTheory.Limits.pullback.condition sieve₁_eq_pullback_sieve₁' CategoryTheory.Limits.pullback.lift_fst_snd
sieve₁_apply 📖	mathematical	—	CategoryTheory.Sieve.arrows sieve₁ I₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Y CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.CategoryStruct.comp p₁ p₂	—	—
sieve₁_eq_pullback_sieve₁' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f	sieve₁ CategoryTheory.Sieve.pullback CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.lift sieve₁'	—	CategoryTheory.Sieve.ext CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π w CategoryTheory.eq_whisker
sieve₁_inter 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreZeroHypercover.f CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst	sieve₁ inter CategoryTheory.Limits.hasPullbackHorizPaste Y p₁ CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullback.snd CategoryTheory.Sieve.bind CategoryTheory.Sieve.arrows CategoryTheory.Sieve.pullback	—	CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Sieve.ext CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks w CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullback.condition_assoc Mathlib.Tactic.Reassoc.eq_whisker'
sieve₁_trivial 📖	mathematical	—	sieve₁ trivial Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.Sieve.ext CategoryTheory.Category.comp_id
sigmaOfIsColimit_Y 📖	mathematical	—	Y sigmaOfIsColimit CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₁' CategoryTheory.discreteCategory CategoryTheory.Discrete.functor Y'	—	—
sigmaOfIsColimit_toPreZeroHypercover 📖	mathematical	—	toPreZeroHypercover sigmaOfIsColimit CategoryTheory.PreZeroHypercover.sigmaOfIsColimit	—	—
trivial_I₁ 📖	mathematical	—	I₁ trivial	—	—
trivial_Y 📖	mathematical	—	Y trivial	—	—
trivial_p₁ 📖	mathematical	—	p₁ trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
trivial_p₂ 📖	mathematical	—	p₂ trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
trivial_toPreZeroHypercover 📖	mathematical	—	toPreZeroHypercover trivial CategoryTheory.PreZeroHypercover.singleton CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y CategoryTheory.PreZeroHypercover.X toPreZeroHypercover p₁ CategoryTheory.PreZeroHypercover.f p₂	—	—

CategoryTheory.PreOneHypercover.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	6 math math: comp_s₁, comp_h₀, CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy, comp_s₀, CategoryTheory.PreOneHypercover.exists_nonempty_homotopy, comp_h₁
h₁ 📖	CompOp	12 math math: ext_iff, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, w₁₁, CategoryTheory.PreOneHypercover.cylinderHom_h₁, w₁₂_assoc, id_h₁, w₁₂, comp_h₁, CategoryTheory.PreOneHypercover.id_h₁, w₁₁_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₁, CategoryTheory.PreOneHypercover.comp_h₁
id 📖	CompOp	4 math math: id_h₀, id_s₁, id_h₁, id_s₀
mapMultiforkOfIsLimit 📖	CompOp	3 math math: CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq, mapMultiforkOfIsLimit_ι_assoc, mapMultiforkOfIsLimit_ι
s₁ 📖	CompOp	17 math math: comp_s₁, ext_iff, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, w₁₁, CategoryTheory.PreOneHypercover.id_s₁, CategoryTheory.PreOneHypercover.comp_s₁, CategoryTheory.GrothendieckTopology.OneHypercover.id_s₁, id_s₁, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁, w₁₂_assoc, CategoryTheory.PreOneHypercover.interSnd_s₁, w₁₂, CategoryTheory.PreOneHypercover.cylinderHom_s₁, comp_h₁, CategoryTheory.PreOneHypercover.interFst_s₁, w₁₁_assoc, CategoryTheory.PreOneHypercover.comp_h₁
s₁' 📖	CompOp	—
toHom 📖	CompOp	46 math math: comp_s₁, ext_iff, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, CategoryTheory.PreOneHypercover.comp_s₀, CategoryTheory.PreOneHypercover.Homotopy.wl, w₁₁, CategoryTheory.PreOneHypercover.cylinder_X, CategoryTheory.PreOneHypercover.cylinderHom_h₁, comp_h₀, CategoryTheory.PreOneHypercover.Homotopy.wl_assoc, CategoryTheory.PreOneHypercover.id_h₀, comp_s₀, CategoryTheory.PreOneHypercover.interSnd_toHom, CategoryTheory.PreOneHypercover.cylinder_I₀, CategoryTheory.PreOneHypercover.interFst_toHom, CategoryTheory.PreOneHypercover.cylinder_f, CategoryTheory.PreOneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.cylinder_I₁, CategoryTheory.PreOneHypercover.id_s₀, id_h₀, CategoryTheory.PreOneHypercover.sieve₀_cylinder, CategoryTheory.PreOneHypercover.oneToZero_map, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀, CategoryTheory.GrothendieckTopology.OneHypercover.id_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁, w₁₂_assoc, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, CategoryTheory.PreOneHypercover.toPullback_cylinder, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀, w₁₂, CategoryTheory.PreOneHypercover.comp_h₀, CategoryTheory.PreOneHypercover.Homotopy.wr, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₀, CategoryTheory.PreOneHypercover.cylinder_p₁, mapMultiforkOfIsLimit_ι_assoc, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.PreOneHypercover.cylinderHom_s₁, comp_h₁, CategoryTheory.PreOneHypercover.cylinderHom_s₀, mapMultiforkOfIsLimit_ι, w₁₁_assoc, CategoryTheory.PreOneHypercover.Homotopy.wr_assoc, CategoryTheory.PreOneHypercover.comp_h₁, id_s₀, CategoryTheory.PreOneHypercover.cylinderHom_h₀, CategoryTheory.PreOneHypercover.cylinder_Y

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.Hom.s₀	—	—
comp_h₁ 📖	mathematical	—	h₁ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom s₁	—	—
comp_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom comp	—	—
comp_s₁ 📖	mathematical	—	s₁ comp CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom	—	—
ext 📖	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom CategoryTheory.PreZeroHypercover.Hom.h₀ s₁ h₁	—	—	—
ext_iff 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom CategoryTheory.PreZeroHypercover.Hom.h₀ s₁ h₁	—	ext
id_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X	—	—
id_h₁ 📖	mathematical	—	h₁ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y	—	—
id_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom id	—	—
id_s₁ 📖	mathematical	—	s₁ id	—	—
mapMultiforkOfIsLimit_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.PreOneHypercover.multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.PreOneHypercover.multicospanIndex CategoryTheory.Limits.MulticospanIndex.left mapMultiforkOfIsLimit CategoryTheory.Limits.Multifork.ι CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.PreZeroHypercover.X CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PreZeroHypercover.Hom.h₀	—	CategoryTheory.Limits.Multifork.IsLimit.fac
mapMultiforkOfIsLimit_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.PreOneHypercover.multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.PreOneHypercover.multicospanIndex mapMultiforkOfIsLimit CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Limits.Multifork.ι CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.PreZeroHypercover.X Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.PreZeroHypercover.Hom.h₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMultiforkOfIsLimit_ι
w₁₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom s₁ CategoryTheory.PreZeroHypercover.X h₁ CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreZeroHypercover.Hom.h₀	—	—
w₁₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom s₁ h₁ CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.p₁ CategoryTheory.PreZeroHypercover.Hom.h₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w₁₁
w₁₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom s₁ CategoryTheory.PreZeroHypercover.X h₁ CategoryTheory.PreOneHypercover.p₂ CategoryTheory.PreZeroHypercover.Hom.h₀	—	—
w₁₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom s₁ h₁ CategoryTheory.PreZeroHypercover.X CategoryTheory.PreOneHypercover.p₂ CategoryTheory.PreZeroHypercover.Hom.h₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w₁₂

CategoryTheory.PreZeroHypercover

Definitions

Name	Category	Theorems
toPreOneHypercover 📖	CompOp	8 math math: toPreOneHypercover_toPreZeroHypercover, toPreOneHypercover_p₁, toPreOneHypercover_I₁, CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover_toPreOneHypercover, CategoryTheory.instHasPullbacksToPreOneHypercover, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, toPreOneHypercover_Y, toPreOneHypercover_p₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_of_isSeparatedFor 📖	—	CategoryTheory.Presieve.IsSeparatedFor presieve₀ CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op X Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct f	—	—	CategoryTheory.Presieve.IsSeparatedFor.ext
toPreOneHypercover_I₁ 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.I₁ toPreOneHypercover	—	—
toPreOneHypercover_Y 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.Y toPreOneHypercover CategoryTheory.Limits.pullback X f	—	—
toPreOneHypercover_p₁ 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.p₁ toPreOneHypercover CategoryTheory.Limits.pullback.fst X f	—	—
toPreOneHypercover_p₂ 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.p₂ toPreOneHypercover CategoryTheory.Limits.pullback.snd X f	—	—
toPreOneHypercover_toPreZeroHypercover 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.toPreZeroHypercover toPreOneHypercover	—	—

CategoryTheory.Precoverage.ZeroHypercover

Definitions

Name	Category	Theorems
toOneHypercover 📖	CompOp	1 math math: toOneHypercover_toPreOneHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toOneHypercover_toPreOneHypercover 📖	mathematical	CategoryTheory.PreZeroHypercover.HasPullbacks toPreZeroHypercover	CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover CategoryTheory.Precoverage.toGrothendieck toOneHypercover CategoryTheory.PreZeroHypercover.toPreOneHypercover	—	—

---

← Back to Index