One

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

Statistics

Metric	Count
Definitions oneHypercover, preOneHypercover, OneHypercover, instCategory, inter, isLimitMultifork, isoMk, mk', multiforkLift, toPreOneHypercover, toZeroHypercover, trivial, PreOneHypercover, comp, h₁, id, mapMulticospan, mapMultiforkOfIsLimit, s₁, s₁', toHom, I₁, I₁', Y, Y', congrIndexOneOfEq, congrIndexOneOfEqIso, equivalenceMulticospanOfIso, forkOfIsColimit, instCategory, instUniqueLMulticospanShapeSigmaOfIsColimit, instUniqueRMulticospanShapeSigmaOfIsColimit, inter, interFst, interLift, interSnd, isLimitEquivOfIso, isLimitMultiforkEquivIsLimitFork, isLimitSigmaOfIsColimitEquiv, isoMk, multicospanIndex, multicospanShape, multifork, oneToZero, p₁, p₂, sieve₁, sieve₁', sigmaOfIsColimit, toPreZeroHypercover, toPullback, trivial, refineOneHypercover, toPreOneHypercover, toOneHypercover	55
Theorems oneHypercover_toPreOneHypercover, preOneHypercover_I₀, preOneHypercover_I₁, preOneHypercover_X, preOneHypercover_Y, preOneHypercover_f, preOneHypercover_p₁, preOneHypercover_p₂, preOneHypercover_sieve₀, preOneHypercover_sieve₁, comp_h₀, comp_h₁, comp_s₀, comp_s₁, id_h₀, id_h₁, id_s₀, id_s₁, instNonempty, inter_toPreOneHypercover, isoMk_hom, isoMk_inv, 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', ext'_iff, ext_iff, id_h₀, id_h₁, id_s₀, id_s₁, mapMulticospan_map, mapMulticospan_obj, mapMultiforkOfIsLimit_comp, mapMultiforkOfIsLimit_comp_assoc, mapMultiforkOfIsLimit_id, mapMultiforkOfIsLimit_ι, mapMultiforkOfIsLimit_ι_assoc, w₁₁, w₁₁_assoc, w₁₂, w₁₂_assoc, ext, Y'_apply, comp_h₀, comp_h₁, comp_s₀, comp_s₁, congrIndexOneOfEqIso_hom_naturality, congrIndexOneOfEqIso_hom_naturality_assoc, congrIndexOneOfEqIso_hom_p₁, congrIndexOneOfEqIso_hom_p₁_assoc, congrIndexOneOfEqIso_inv_naturality, congrIndexOneOfEqIso_inv_naturality_assoc, congrIndexOneOfEqIso_inv_p₁, congrIndexOneOfEqIso_inv_p₁_assoc, congrIndexOneOfEqIso_inv_p₂, congrIndexOneOfEqIso_inv_p₂_assoc, congrIndexOneOfEqIso_refl, congrIndexOneOfEq_congrFun, congrIndexOneOfEq_equiv, congrIndexOneOfEq_naturality, congrIndexOneOfEq_refl, congrIndexOneOfEq_trans, equivalenceMulticospanOfIso_functor, equivalenceMulticospanOfIso_inverse, forkOfIsColimit_pt, forkOfIsColimit_ι_map_inj, forkOfIsColimit_ι_map_inj_assoc, hom_inv_h₀, hom_inv_h₀_assoc, hom_inv_h₁, hom_inv_h₁_assoc, hom_inv_s₀_apply, hom_inv_s₁_apply, id_h₀, id_h₁, id_s₀, id_s₁, instIsIsoH₀Hom, instIsIsoH₀Inv, instIsIsoH₁Hom, instIsIsoH₁Inv, instNonempty, interFst_s₁, interFst_toHom, interSnd_s₁, interSnd_toHom, inter_I₁, inter_Y, inter_p₁, inter_p₂, inter_toPreZeroHypercover, inv_hom_h₀, inv_hom_h₀_assoc, inv_hom_h₁, inv_hom_h₁_assoc, inv_hom_s₀_apply, inv_hom_s₁_apply, isoMk_aux, isoMk_aux_assoc, isoMk_hom_h₀, isoMk_hom_h₁, isoMk_hom_s₀, isoMk_hom_s₁, isoMk_inv_h₀, isoMk_inv_h₁, isoMk_inv_s₀, isoMk_inv_s₁, 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, refineOneHypercover_I₁, refineOneHypercover_Y, refineOneHypercover_p₁, refineOneHypercover_p₂, refineOneHypercover_toPreZeroHypercover, sieve₁'_refineOneHypercover, toPreOneHypercover_I₁, toPreOneHypercover_Y, toPreOneHypercover_p₁, toPreOneHypercover_p₂, toPreOneHypercover_toPreZeroHypercover, toOneHypercover_toPreOneHypercover, instHasPullbacksRefineOneHypercover, instHasPullbacksToPreOneHypercover, sieve₁'_toPreOneHypercover_eq_top	165
Total	220

CategoryTheory

Definitions

Name	Category	Theorems
PreOneHypercover 📖	CompData	40 math math: PreOneHypercover.inv_hom_h₀_assoc, PreOneHypercover.comp_s₀, GrothendieckTopology.OneHypercover.isoMk_inv, PreOneHypercover.hom_inv_h₁_assoc, GrothendieckTopology.OneHypercover.isoMk_hom, PreOneHypercover.oneToZero_obj, PreOneHypercover.id_h₀, PreOneHypercover.instIsIsoH₁Hom, PreOneHypercover.hom_inv_h₀, PreOneHypercover.isoMk_inv_h₁, PreOneHypercover.equivalenceMulticospanOfIso_inverse, PreOneHypercover.id_s₁, PreOneHypercover.exists_nonempty_homotopy, PreOneHypercover.hom_inv_s₁_apply, PreOneHypercover.isoMk_hom_h₀, PreOneHypercover.isoMk_inv_s₁, PreOneHypercover.inv_hom_h₀, PreOneHypercover.equivalenceMulticospanOfIso_functor, PreOneHypercover.comp_s₁, PreOneHypercover.inv_hom_s₁_apply, PreOneHypercover.inv_hom_h₁_assoc, PreOneHypercover.instNonempty, PreOneHypercover.id_s₀, PreOneHypercover.hom_inv_h₁, PreOneHypercover.oneToZero_map, PreOneHypercover.instIsIsoH₀Inv, PreOneHypercover.isoMk_hom_s₁, PreOneHypercover.instIsIsoH₀Hom, PreOneHypercover.instIsIsoH₁Inv, PreOneHypercover.isoMk_inv_s₀, PreOneHypercover.comp_h₀, PreOneHypercover.isoMk_hom_s₀, PreOneHypercover.id_h₁, PreOneHypercover.inv_hom_s₀_apply, PreOneHypercover.hom_inv_h₀_assoc, PreOneHypercover.inv_hom_h₁, PreOneHypercover.comp_h₁, PreOneHypercover.hom_inv_s₀_apply, PreOneHypercover.isoMk_inv_h₀, PreOneHypercover.isoMk_hom_h₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasPullbacksRefineOneHypercover 📖	mathematical	PreZeroHypercover.HasPullbacks	PreZeroHypercover.HasPullbacks PreOneHypercover.toPreZeroHypercover PreZeroHypercover.refineOneHypercover	—	—
instHasPullbacksToPreOneHypercover 📖	mathematical	PreZeroHypercover.HasPullbacks	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	16 math math: OneHypercover.comp_h₁, OneHypercover.isoMk_inv, OneHypercover.isoMk_hom, OneHypercover.instNonempty, OneHypercover.exists_nonempty_homotopy, OneHypercoverFamily.exists_oneHypercover, OneHypercover.id_s₁, OneHypercoverFamily.IsGenerating.le, 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
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	47 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.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, f_glueMorphisms, IsPreservedBy.mem₁, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, id_s₁, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, map_toPreOneHypercover, IsPreservedBy.mem₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, id_h₀, id_s₀, f_glueMorphisms_assoc, comp_s₁, trivial_toPreOneHypercover, AlgebraicGeometry.Scheme.GlueData.oneHypercover_X, inter_toPreOneHypercover, 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₁, AlgebraicGeometry.Scheme.affineOneHypercover_toPreOneHypercover_toPreZeroHypercover, CategoryTheory.GrothendieckTopology.Cover.oneHypercover_toPreOneHypercover, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, isStronglySheafFor, toZeroHypercover_toPreZeroHypercover, multiforkLift_map_assoc, id_h₁, mem₁, isStronglySeparatedFor
toZeroHypercover 📖	CompOp	1 math math: toZeroHypercover_toPreZeroHypercover
trivial 📖	CompOp	1 math math: trivial_toPreOneHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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₁	toPreOneHypercover inter CategoryTheory.PreOneHypercover.inter	—	—
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	—	—
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₁ toPreOneHypercover	—	—
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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj 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 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj 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	70 math math: congrIndexOneOfEqIso_hom_p₁, AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₁, forkOfIsColimit_ι_map_inj_assoc, trivial_I₁, isoMk_aux, forkOfIsColimit_pt, p₁_sigmaOfIsColimit_assoc, inter_I₁, hom_inv_h₁_assoc, multicospanIndex_fst, cylinder_X, cylinderHom_h₁, congrIndexOneOfEqIso_inv_p₁, CategoryTheory.PreZeroHypercover.refineOneHypercover_I₁, CategoryTheory.PreZeroHypercover.saturate_I₁, multicospanIndex_right, congrIndexOneOfEqIso_inv_p₁_assoc, isoMk_aux_assoc, CategoryTheory.PreZeroHypercover.toPreOneHypercover_I₁, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₁, multicospanShape_fst, congrIndexOneOfEqIso_inv_p₂_assoc, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₁, multicospanIndex_snd, congrIndexOneOfEqIso_hom_naturality, congrIndexOneOfEq_naturality, p₁_sigmaOfIsColimit, congrIndexOneOfEqIso_inv_naturality, Hom.ext'_iff, isoMk_inv_h₁, congrIndexOneOfEqIso_refl, congrIndexOneOfEqIso_hom_naturality_assoc, congrIndexOneOfEq_trans, congrIndexOneOfEq_equiv, cylinder_I₀, inter_p₂, hom_inv_s₁_apply, Y'_apply, isoMk_inv_s₁, cylinder_f, congrIndexOneOfEqIso_inv_p₂, inv_hom_s₁_apply, inv_hom_h₁_assoc, cylinder_I₁, hom_inv_h₁, congrIndexOneOfEq_congrFun, multicospanShape_snd, isoMk_hom_s₁, sieve₁_apply, inter_Y, sieve₁'_cylinder, congrIndexOneOfEqIso_hom_p₁_assoc, interSnd_s₁, toPullback_cylinder, inter_p₁, cylinder_p₁, cylinder_p₂, cylinderHom_s₁, interFst_s₁, forkOfIsColimit_ι_map_inj, cylinderHom_s₀, p₂_sigmaOfIsColimit, congrIndexOneOfEq_refl, p₂_sigmaOfIsColimit_assoc, inv_hom_h₁, map_I₁, cylinderHom_h₀, congrIndexOneOfEqIso_inv_naturality_assoc, cylinder_Y, isoMk_hom_h₁
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	68 math math: congrIndexOneOfEqIso_hom_p₁, isoMk_aux, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_Y, Homotopy.wl, Hom.w₁₁, hom_inv_h₁_assoc, multicospanIndex_fst, cylinderHom_h₁, congrIndexOneOfEqIso_inv_p₁, multicospanIndex_right, congrIndexOneOfEqIso_inv_p₁_assoc, isoMk_aux_assoc, Homotopy.wl_assoc, congrIndexOneOfEqIso_inv_p₂_assoc, multicospanIndex_snd, instIsIsoH₁Hom, map_p₁, congrIndexOneOfEqIso_hom_naturality, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₁, p₁_sigmaOfIsColimit, congrIndexOneOfEqIso_inv_naturality, Hom.ext'_iff, isoMk_inv_h₁, congrIndexOneOfEqIso_refl, congrIndexOneOfEqIso_hom_naturality_assoc, inter_p₂, Y'_apply, congrIndexOneOfEqIso_inv_p₂, inv_hom_h₁_assoc, hom_inv_h₁, w, sigmaOfIsColimit_Y, Hom.w₁₂_assoc, sieve₁_apply, CategoryTheory.PreZeroHypercover.refineOneHypercover_Y, inter_Y, Hom.id_h₁, instIsIsoH₁Inv, sieve₁'_cylinder, congrIndexOneOfEqIso_hom_p₁_assoc, toPullback_cylinder, Hom.w₁₂, inter_p₁, 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₂, inv_hom_h₁, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₁, CategoryTheory.PreZeroHypercover.saturate_Y, comp_h₁, cylinderHom_h₀, congrIndexOneOfEqIso_inv_naturality_assoc, cylinder_Y, isoMk_hom_h₁, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₁
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
congrIndexOneOfEq 📖	CompOp	27 math math: congrIndexOneOfEqIso_hom_p₁, isoMk_aux, hom_inv_h₁_assoc, congrIndexOneOfEqIso_inv_p₁, congrIndexOneOfEqIso_inv_p₁_assoc, isoMk_aux_assoc, congrIndexOneOfEqIso_inv_p₂_assoc, congrIndexOneOfEqIso_hom_naturality, congrIndexOneOfEq_naturality, congrIndexOneOfEqIso_inv_naturality, Hom.ext'_iff, isoMk_inv_h₁, congrIndexOneOfEqIso_refl, congrIndexOneOfEqIso_hom_naturality_assoc, congrIndexOneOfEq_trans, congrIndexOneOfEq_equiv, hom_inv_s₁_apply, isoMk_inv_s₁, congrIndexOneOfEqIso_inv_p₂, inv_hom_s₁_apply, inv_hom_h₁_assoc, hom_inv_h₁, congrIndexOneOfEq_congrFun, congrIndexOneOfEqIso_hom_p₁_assoc, congrIndexOneOfEq_refl, inv_hom_h₁, congrIndexOneOfEqIso_inv_naturality_assoc
congrIndexOneOfEqIso 📖	CompOp	19 math math: congrIndexOneOfEqIso_hom_p₁, isoMk_aux, hom_inv_h₁_assoc, congrIndexOneOfEqIso_inv_p₁, congrIndexOneOfEqIso_inv_p₁_assoc, isoMk_aux_assoc, congrIndexOneOfEqIso_inv_p₂_assoc, congrIndexOneOfEqIso_hom_naturality, congrIndexOneOfEqIso_inv_naturality, Hom.ext'_iff, isoMk_inv_h₁, congrIndexOneOfEqIso_refl, congrIndexOneOfEqIso_hom_naturality_assoc, congrIndexOneOfEqIso_inv_p₂, inv_hom_h₁_assoc, hom_inv_h₁, congrIndexOneOfEqIso_hom_p₁_assoc, inv_hom_h₁, congrIndexOneOfEqIso_inv_naturality_assoc
equivalenceMulticospanOfIso 📖	CompOp	2 math math: equivalenceMulticospanOfIso_inverse, equivalenceMulticospanOfIso_functor
forkOfIsColimit 📖	CompOp	3 math math: forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, forkOfIsColimit_ι_map_inj
instCategory 📖	CompOp	38 math math: inv_hom_h₀_assoc, comp_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_inv, hom_inv_h₁_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_hom, oneToZero_obj, id_h₀, instIsIsoH₁Hom, hom_inv_h₀, isoMk_inv_h₁, equivalenceMulticospanOfIso_inverse, id_s₁, hom_inv_s₁_apply, isoMk_hom_h₀, isoMk_inv_s₁, inv_hom_h₀, equivalenceMulticospanOfIso_functor, comp_s₁, inv_hom_s₁_apply, inv_hom_h₁_assoc, id_s₀, hom_inv_h₁, oneToZero_map, instIsIsoH₀Inv, isoMk_hom_s₁, instIsIsoH₀Hom, instIsIsoH₁Inv, isoMk_inv_s₀, comp_h₀, isoMk_hom_s₀, id_h₁, inv_hom_s₀_apply, hom_inv_h₀_assoc, inv_hom_h₁, comp_h₁, hom_inv_s₀_apply, isoMk_inv_h₀, isoMk_hom_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₁
isLimitEquivOfIso 📖	CompOp	—
isLimitMultiforkEquivIsLimitFork 📖	CompOp	—
isLimitSigmaOfIsColimitEquiv 📖	CompOp	—
isoMk 📖	CompOp	8 math math: isoMk_inv_h₁, isoMk_hom_h₀, isoMk_inv_s₁, isoMk_hom_s₁, isoMk_inv_s₀, isoMk_hom_s₀, isoMk_inv_h₀, isoMk_hom_h₁
multicospanIndex 📖	CompOp	21 math math: Hom.mapMultiforkOfIsLimit_comp_assoc, multicospanIndex_fst, CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, multicospanIndex_right, multifork_ι, multicospanIndex_snd, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_apply_coe, multicospanIndex_left, CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff, Hom.mapMultiforkOfIsLimit_id, CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_symm_apply_val, Hom.mapMultiforkOfIsLimit_ι_assoc, Hom.mapMultiforkOfIsLimit_comp, CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_symm_apply_val, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, Hom.mapMultiforkOfIsLimit_ι, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, CategoryTheory.PreZeroHypercover.isLimit_saturate_type_iff, CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_apply_coe
multicospanShape 📖	CompOp	29 math math: Hom.mapMultiforkOfIsLimit_comp_assoc, 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, CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_apply_coe, multicospanShape_L, equivalenceMulticospanOfIso_inverse, multicospanShape_R, multicospanIndex_left, equivalenceMulticospanOfIso_functor, Hom.mapMulticospan_map, multicospanShape_snd, CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff, Hom.mapMultiforkOfIsLimit_id, CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_symm_apply_val, Hom.mapMultiforkOfIsLimit_ι_assoc, Hom.mapMultiforkOfIsLimit_comp, CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_symm_apply_val, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, Hom.mapMultiforkOfIsLimit_ι, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, CategoryTheory.PreZeroHypercover.isLimit_saturate_type_iff, CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_apply_coe, Hom.mapMulticospan_obj
multifork 📖	CompOp	6 math math: CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff, multifork_ι, CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers, CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff, CategoryTheory.PreZeroHypercover.isLimit_saturate_type_iff
oneToZero 📖	CompOp	2 math math: oneToZero_obj, oneToZero_map
p₁ 📖	CompOp	33 math math: congrIndexOneOfEqIso_hom_p₁, forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, Homotopy.wl, p₁_sigmaOfIsColimit_assoc, Hom.w₁₁, multicospanIndex_fst, trivial_p₁, cylinderHom_h₁, congrIndexOneOfEqIso_inv_p₁, congrIndexOneOfEqIso_inv_p₁_assoc, CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₁, Homotopy.wl_assoc, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁, map_p₁, p₁_sigmaOfIsColimit, inter_p₂, w, CategoryTheory.PreZeroHypercover.refineOneHypercover_p₁, CategoryTheory.PreZeroHypercover.saturate_p₁, sieve₁_apply, inter_Y, congrIndexOneOfEqIso_hom_p₁_assoc, toPullback_cylinder, inter_p₁, 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	28 math math: forkOfIsColimit_ι_map_inj_assoc, forkOfIsColimit_pt, cylinderHom_h₁, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_p₂, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂, CategoryTheory.PreZeroHypercover.refineOneHypercover_p₂, congrIndexOneOfEqIso_inv_p₂_assoc, multicospanIndex_snd, inter_p₂, congrIndexOneOfEqIso_inv_p₂, AlgebraicGeometry.Scheme.GlueData.oneHypercover_p₂, w, trivial_p₂, Hom.w₁₂_assoc, sieve₁_apply, CategoryTheory.PreZeroHypercover.saturate_p₂, 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	11 math math: CategoryTheory.Functor.OneHypercoverDenseData.mem₁, IsStronglySeparatedFor.isSeparatedFor_sieve₁, sieve₁'_eq_sieve₁, sieve₁_eq_pullback_sieve₁', CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁, CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁, IsStronglySheafFor.isSeparatedFor_sieve₁, sieve₁_apply, sieve₁_inter, sieve₁_trivial, CategoryTheory.GrothendieckTopology.OneHypercover.mem₁
sieve₁' 📖	CompOp	7 math math: CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', sieve₁'_eq_sieve₁, sieve₁_eq_pullback_sieve₁', sieve₀_cylinder, sieve₁'_cylinder, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, CategoryTheory.PreZeroHypercover.sieve₁'_refineOneHypercover
sigmaOfIsColimit 📖	CompOp	6 math math: p₁_sigmaOfIsColimit_assoc, p₁_sigmaOfIsColimit, sigmaOfIsColimit_Y, sigmaOfIsColimit_toPreZeroHypercover, p₂_sigmaOfIsColimit, p₂_sigmaOfIsColimit_assoc
toPreZeroHypercover 📖	CompOp	166 math math: congrIndexOneOfEqIso_hom_p₁, forkOfIsColimit_ι_map_inj_assoc, CategoryTheory.PreZeroHypercover.toPreOneHypercover_toPreZeroHypercover, Hom.comp_s₁, isoMk_aux, inv_hom_h₀_assoc, Hom.ext_iff, forkOfIsColimit_pt, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, comp_s₀, Homotopy.wl, p₁_sigmaOfIsColimit_assoc, inter_I₁, Hom.w₁₁, CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, hom_inv_h₁_assoc, multicospanIndex_fst, cylinder_X, cylinderHom_h₁, Hom.comp_h₀, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₀, congrIndexOneOfEqIso_inv_p₁, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, IsStronglySheafFor.isSheafFor_presieve₀, map_I₀, oneToZero_obj, map_X, multicospanIndex_right, congrIndexOneOfEqIso_inv_p₁_assoc, isoMk_aux_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', Homotopy.wl_assoc, multicospanShape_fst, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₀, congrIndexOneOfEqIso_inv_p₂_assoc, multifork_ι, trivial_toPreZeroHypercover, id_h₀, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₀, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f, multicospanIndex_snd, instIsIsoH₁Hom, sieve₁'_eq_sieve₁, map_p₁, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₀, Hom.comp_s₀, congrIndexOneOfEqIso_hom_naturality, sieve₁_eq_pullback_sieve₁', congrIndexOneOfEq_naturality, hom_inv_h₀, inter_toPreZeroHypercover, interSnd_toHom, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac, CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms, p₁_sigmaOfIsColimit, congrIndexOneOfEqIso_inv_naturality, Hom.ext'_iff, isoMk_inv_h₁, congrIndexOneOfEqIso_refl, multicospanShape_L, congrIndexOneOfEqIso_hom_naturality_assoc, congrIndexOneOfEq_trans, congrIndexOneOfEq_equiv, IsStronglySheafFor.map_amalgamate, CategoryTheory.PreZeroHypercover.refineOneHypercover_toPreZeroHypercover, cylinder_I₀, inter_p₂, IsStronglySeparatedFor.arrowsCompatible, hom_inv_s₁_apply, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, Y'_apply, interFst_toHom, multicospanIndex_left, isoMk_hom_h₀, isoMk_inv_s₁, inv_hom_h₀, cylinder_f, congrIndexOneOfEqIso_inv_p₂, comp_s₁, inv_hom_s₁_apply, inv_hom_h₁_assoc, cylinder_I₁, CategoryTheory.instHasPullbacksToPreOneHypercover, Hom.mapMulticospan_map, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, id_s₀, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₀, hom_inv_h₁, w, CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₀, Hom.id_h₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X, sieve₀_cylinder, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_X, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀, congrIndexOneOfEq_congrFun, instIsIsoH₀Inv, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_f, CategoryTheory.GrothendieckTopology.OneHypercover.id_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁, multicospanShape_snd, isoMk_hom_s₁, instIsIsoH₀Hom, Hom.w₁₂_assoc, sieve₁_apply, AlgebraicGeometry.Scheme.GlueData.oneHypercover_X, inter_Y, instIsIsoH₁Inv, isoMk_inv_s₀, sieve₁'_cylinder, congrIndexOneOfEqIso_hom_p₁_assoc, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, interSnd_s₁, toPullback_cylinder, sigmaOfIsColimit_toPreZeroHypercover, AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀, Hom.w₁₂, inter_p₁, IsStronglySeparatedFor.isSeparatedFor_presieve₀, comp_h₀, Homotopy.wr, AlgebraicGeometry.Scheme.GlueData.oneHypercover_f, CategoryTheory.PreZeroHypercover.saturate_toPreZeroHypercover, sieve₁_inter, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₀, cylinder_p₁, isoMk_hom_s₀, Hom.mapMultiforkOfIsLimit_ι_assoc, cylinder_p₂, map_f, cylinderHom_s₁, Hom.comp_h₁, inv_hom_s₀_apply, AlgebraicGeometry.Scheme.affineOneHypercover_toPreOneHypercover_toPreZeroHypercover, interFst_s₁, forkOfIsColimit_ι_map_inj, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₀, cylinderHom_s₀, Hom.mapMultiforkOfIsLimit_ι, sieve₀_trivial, p₂_sigmaOfIsColimit, CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover_toPreZeroHypercover, Hom.w₁₁_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, hom_inv_h₀_assoc, congrIndexOneOfEq_refl, p₂_sigmaOfIsColimit_assoc, Homotopy.wr_assoc, map_p₂, inv_hom_h₁, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₀, comp_h₁, Hom.id_s₀, cylinderHom_h₀, congrIndexOneOfEqIso_inv_naturality_assoc, hom_inv_s₀_apply, cylinder_Y, isoMk_inv_h₀, CategoryTheory.instHasPullbacksRefineOneHypercover, isoMk_hom_h₁, Hom.mapMulticospan_obj
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	—	—
congrIndexOneOfEqIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.Iso.hom congrIndexOneOfEqIso CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
congrIndexOneOfEqIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.Iso.hom congrIndexOneOfEqIso CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' congrIndexOneOfEqIso_hom_naturality
congrIndexOneOfEqIso_hom_p₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.Iso.hom congrIndexOneOfEqIso p₁ CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
congrIndexOneOfEqIso_hom_p₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.Iso.hom congrIndexOneOfEqIso CategoryTheory.PreZeroHypercover.X toPreZeroHypercover p₁ CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' congrIndexOneOfEqIso_hom_p₁
congrIndexOneOfEqIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.Iso.inv congrIndexOneOfEqIso CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
congrIndexOneOfEqIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.Iso.inv congrIndexOneOfEqIso CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' congrIndexOneOfEqIso_inv_naturality
congrIndexOneOfEqIso_inv_p₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.Iso.inv congrIndexOneOfEqIso p₁ CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
congrIndexOneOfEqIso_inv_p₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.Iso.inv congrIndexOneOfEqIso CategoryTheory.PreZeroHypercover.X toPreZeroHypercover p₁ CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' congrIndexOneOfEqIso_inv_p₁
congrIndexOneOfEqIso_inv_p₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.Iso.inv congrIndexOneOfEqIso p₂ CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
congrIndexOneOfEqIso_inv_p₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.Iso.inv congrIndexOneOfEqIso CategoryTheory.PreZeroHypercover.X toPreZeroHypercover p₂ CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' congrIndexOneOfEqIso_inv_p₂
congrIndexOneOfEqIso_refl 📖	mathematical	—	congrIndexOneOfEqIso CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover CategoryTheory.Iso.refl Y DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq	—	—
congrIndexOneOfEq_congrFun 📖	mathematical	DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq	DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover	—	congrIndexOneOfEq_refl
congrIndexOneOfEq_equiv 📖	mathematical	—	DFunLike.coe Equiv I₁ CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover EquivLike.toFunLike Equiv.instEquivLike Equiv.symm congrIndexOneOfEq Equiv.symm_apply_apply	—	Equiv.injective Equiv.symm_apply_apply congrIndexOneOfEq_naturality Equiv.apply_symm_apply
congrIndexOneOfEq_naturality 📖	mathematical	—	DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover	—	congrIndexOneOfEq_refl
congrIndexOneOfEq_refl 📖	mathematical	—	congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover Equiv.refl I₁	—	—
congrIndexOneOfEq_trans 📖	mathematical	—	DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover	—	congrIndexOneOfEq_refl
equivalenceMulticospanOfIso_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Limits.WalkingMulticospan multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory equivalenceMulticospanOfIso Hom.mapMulticospan CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory	—	—
equivalenceMulticospanOfIso_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Limits.WalkingMulticospan multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory equivalenceMulticospanOfIso Hom.mapMulticospan CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory	—	—
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.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.Limits.Cofan.IsColimit.desc I₁ p₁ p₂ forkOfIsColimit CategoryTheory.Limits.Fork.ι CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Limits.Cofan.IsColimit.fac
forkOfIsColimit_ι_map_inj_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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.Limits.Cofan.IsColimit.desc I₁ p₁ p₂ forkOfIsColimit CategoryTheory.Limits.Fork.ι CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
hom_inv_h₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.eqToHom	—	Hom.ext'_iff CategoryTheory.Iso.hom_inv_id hom_inv_s₀_apply CategoryTheory.eqToHom_naturality CategoryTheory.Category.comp_id
hom_inv_h₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.Iso.inv CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_h₀
hom_inv_h₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory Hom.s₁ CategoryTheory.Iso.inv Hom.h₁ DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ hom_inv_s₀_apply congrIndexOneOfEqIso CategoryTheory.eqToHom	—	hom_inv_s₀_apply Hom.ext'_iff CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp
hom_inv_h₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory Hom.s₁ Hom.h₁ CategoryTheory.Iso.inv DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ hom_inv_s₀_apply congrIndexOneOfEqIso CategoryTheory.eqToHom	—	hom_inv_s₀_apply CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_h₁
hom_inv_s₀_apply 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id
hom_inv_s₁_apply 📖	mathematical	—	Hom.s₁ CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.hom DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq	—	Hom.ext'_iff CategoryTheory.Iso.hom_inv_id
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	—	—
instIsIsoH₀Hom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover.Hom.h₀	—	hom_inv_s₀_apply hom_inv_h₀_assoc CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl CategoryTheory.Category.assoc CategoryTheory.eqToHom_naturality inv_hom_h₀_assoc
instIsIsoH₀Inv 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover.Hom.h₀	—	CategoryTheory.IsIso.of_isIso_fac_right instIsIsoH₀Hom CategoryTheory.instIsIsoEqToHom inv_hom_h₀
instIsIsoH₁Hom 📖	mathematical	—	CategoryTheory.IsIso Y CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory Hom.s₁ Hom.h₁	—	hom_inv_s₀_apply hom_inv_s₁_apply hom_inv_h₁_assoc CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.assoc congrIndexOneOfEqIso_hom_naturality CategoryTheory.eqToHom_naturality_assoc inv_hom_s₀_apply inv_hom_h₁_assoc
instIsIsoH₁Inv 📖	mathematical	—	CategoryTheory.IsIso Y CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory Hom.s₁ Hom.h₁	—	CategoryTheory.IsIso.of_isIso_fac_right inv_hom_s₀_apply instIsIsoH₁Hom CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.instIsIsoEqToHom inv_hom_h₁
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₀ toPreZeroHypercover	—	—
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 toPreZeroHypercover	—	—
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₀ toPreZeroHypercover	—	—
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 toPreZeroHypercover	—	—
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₀ toPreZeroHypercover	—	—
inter_Y 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	Y inter CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X p₁ CategoryTheory.PreZeroHypercover.f	—	—
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 Y CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁ CategoryTheory.PreZeroHypercover.X DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.bind CategoryTheory.PreZeroHypercover.pullback₁ CategoryTheory.PreZeroHypercover.f EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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 Y CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover I₁ CategoryTheory.PreZeroHypercover.X DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.bind CategoryTheory.PreZeroHypercover.pullback₁ CategoryTheory.PreZeroHypercover.f EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁ CategoryTheory.CategoryStruct.id	—	—
inter_toPreZeroHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁	toPreZeroHypercover inter CategoryTheory.PreZeroHypercover.inter	—	—
inv_hom_h₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.eqToHom	—	Hom.ext'_iff CategoryTheory.Iso.inv_hom_id inv_hom_s₀_apply CategoryTheory.eqToHom_naturality CategoryTheory.Category.comp_id
inv_hom_h₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.Hom.s₀ Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.Iso.hom CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_h₀
inv_hom_h₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory Hom.s₁ CategoryTheory.Iso.hom Hom.h₁ DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ inv_hom_s₀_apply congrIndexOneOfEqIso CategoryTheory.eqToHom	—	inv_hom_s₀_apply Hom.ext'_iff CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp
inv_hom_h₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory Hom.s₁ Hom.h₁ CategoryTheory.Iso.hom DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ inv_hom_s₀_apply congrIndexOneOfEqIso CategoryTheory.eqToHom	—	inv_hom_s₀_apply CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_h₁
inv_hom_s₀_apply 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id
inv_hom_s₁_apply 📖	mathematical	—	Hom.s₁ CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.inv DFunLike.coe Equiv I₁ EquivLike.toFunLike Equiv.instEquivLike congrIndexOneOfEq	—	Hom.ext'_iff CategoryTheory.Iso.inv_hom_id
isoMk_aux 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover EquivLike.toFunLike Equiv.instEquivLike I₁ Equiv.symm congrIndexOneOfEq Equiv.symm_apply_apply CategoryTheory.Iso.hom CategoryTheory.Iso.inv congrIndexOneOfEqIso CategoryTheory.eqToHom	—	Equiv.symm_apply_apply congrIndexOneOfEqIso_inv_naturality_assoc CategoryTheory.eqToHom_trans_assoc congrIndexOneOfEq_equiv CategoryTheory.eqToHom_iso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
isoMk_aux_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover EquivLike.toFunLike Equiv.instEquivLike I₁ CategoryTheory.Iso.hom Equiv.symm congrIndexOneOfEq Equiv.symm_apply_apply CategoryTheory.Iso.inv congrIndexOneOfEqIso CategoryTheory.eqToHom	—	Equiv.symm_apply_apply CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoMk_aux
isoMk_hom_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory isoMk CategoryTheory.PreZeroHypercover.X DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ EquivLike.toFunLike Equiv.instEquivLike	—	—
isoMk_hom_h₁ 📖	mathematical	—	Hom.h₁ CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory isoMk Y DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover EquivLike.toFunLike Equiv.instEquivLike I₁	—	—
isoMk_hom_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory isoMk DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ EquivLike.toFunLike Equiv.instEquivLike	—	—
isoMk_hom_s₁ 📖	mathematical	—	Hom.s₁ CategoryTheory.Iso.hom CategoryTheory.PreOneHypercover instCategory isoMk DFunLike.coe Equiv I₁ CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover EquivLike.toFunLike Equiv.instEquivLike	—	—
isoMk_inv_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory isoMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.eqToHom	—	—
isoMk_inv_h₁ 📖	mathematical	—	Hom.h₁ CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory isoMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover EquivLike.toFunLike Equiv.instEquivLike Equiv.symm I₁ congrIndexOneOfEq CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.instCategory CategoryTheory.PreZeroHypercover.isoMk congrIndexOneOfEqIso CategoryTheory.eqToHom	—	—
isoMk_inv_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover Hom.toHom CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory isoMk DFunLike.coe Equiv CategoryTheory.PreZeroHypercover.I₀ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—
isoMk_inv_s₁ 📖	mathematical	—	Hom.s₁ CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover instCategory isoMk DFunLike.coe Equiv I₁ CategoryTheory.PreZeroHypercover.I₀ toPreZeroHypercover EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.instCategory CategoryTheory.PreZeroHypercover.isoMk congrIndexOneOfEq	—	—
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.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f 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.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.hasPullbackHorizPaste Y CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p₁ CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd CategoryTheory.Sieve.bind CategoryTheory.Sieve.arrows CategoryTheory.Limits.pullback.fst 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	9 math math: comp_s₁, mapMultiforkOfIsLimit_comp_assoc, comp_h₀, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks, CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy, comp_s₀, CategoryTheory.PreOneHypercover.exists_nonempty_homotopy, comp_h₁, mapMultiforkOfIsLimit_comp
h₁ 📖	CompOp	23 math math: ext_iff, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, w₁₁, CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc, CategoryTheory.PreOneHypercover.cylinderHom_h₁, CategoryTheory.PreOneHypercover.instIsIsoH₁Hom, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₁, ext'_iff, CategoryTheory.PreOneHypercover.isoMk_inv_h₁, CategoryTheory.PreOneHypercover.inv_hom_h₁_assoc, CategoryTheory.PreOneHypercover.hom_inv_h₁, w₁₂_assoc, id_h₁, CategoryTheory.PreOneHypercover.instIsIsoH₁Inv, w₁₂, comp_h₁, CategoryTheory.PreOneHypercover.id_h₁, w₁₁_assoc, CategoryTheory.PreOneHypercover.inv_hom_h₁, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₁, CategoryTheory.PreOneHypercover.comp_h₁, CategoryTheory.PreOneHypercover.isoMk_hom_h₁, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₁
id 📖	CompOp	6 math math: CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks, id_h₀, id_s₁, mapMultiforkOfIsLimit_id, id_h₁, id_s₀
mapMulticospan 📖	CompOp	4 math math: CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso_inverse, CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso_functor, mapMulticospan_map, mapMulticospan_obj
mapMultiforkOfIsLimit 📖	CompOp	6 math math: CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq, mapMultiforkOfIsLimit_comp_assoc, mapMultiforkOfIsLimit_id, mapMultiforkOfIsLimit_ι_assoc, mapMultiforkOfIsLimit_comp, mapMultiforkOfIsLimit_ι
s₁ 📖	CompOp	32 math math: comp_s₁, ext_iff, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, w₁₁, CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc, CategoryTheory.PreOneHypercover.instIsIsoH₁Hom, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₁, ext'_iff, CategoryTheory.PreOneHypercover.id_s₁, CategoryTheory.PreOneHypercover.hom_inv_s₁_apply, CategoryTheory.PreOneHypercover.isoMk_inv_s₁, CategoryTheory.PreOneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.inv_hom_s₁_apply, CategoryTheory.PreOneHypercover.inv_hom_h₁_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.id_s₁, CategoryTheory.PreOneHypercover.hom_inv_h₁, id_s₁, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.isoMk_hom_s₁, w₁₂_assoc, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_snd, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_obj, CategoryTheory.PreOneHypercover.instIsIsoH₁Inv, CategoryTheory.PreOneHypercover.interSnd_s₁, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_fst, w₁₂, CategoryTheory.PreOneHypercover.cylinderHom_s₁, comp_h₁, CategoryTheory.PreOneHypercover.interFst_s₁, w₁₁_assoc, CategoryTheory.PreOneHypercover.inv_hom_h₁, CategoryTheory.PreOneHypercover.comp_h₁
s₁' 📖	CompOp	2 math math: mapMulticospan_map, mapMulticospan_obj
toHom 📖	CompOp	73 math math: comp_s₁, CategoryTheory.PreOneHypercover.inv_hom_h₀_assoc, ext_iff, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, CategoryTheory.PreOneHypercover.comp_s₀, CategoryTheory.PreOneHypercover.Homotopy.wl, w₁₁, CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc, CategoryTheory.PreOneHypercover.cylinder_X, CategoryTheory.PreOneHypercover.cylinderHom_h₁, comp_h₀, CategoryTheory.PreOneHypercover.Homotopy.wl_assoc, CategoryTheory.PreOneHypercover.id_h₀, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₀, CategoryTheory.PreOneHypercover.instIsIsoH₁Hom, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₀, comp_s₀, CategoryTheory.PreOneHypercover.hom_inv_h₀, CategoryTheory.PreOneHypercover.interSnd_toHom, ext'_iff, CategoryTheory.PreOneHypercover.cylinder_I₀, CategoryTheory.PreOneHypercover.hom_inv_s₁_apply, CategoryTheory.PreOneHypercover.interFst_toHom, CategoryTheory.PreOneHypercover.isoMk_hom_h₀, CategoryTheory.PreOneHypercover.inv_hom_h₀, CategoryTheory.PreOneHypercover.cylinder_f, CategoryTheory.PreOneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.inv_hom_s₁_apply, CategoryTheory.PreOneHypercover.inv_hom_h₁_assoc, CategoryTheory.PreOneHypercover.cylinder_I₁, mapMulticospan_map, CategoryTheory.PreOneHypercover.id_s₀, CategoryTheory.PreOneHypercover.hom_inv_h₁, id_h₀, CategoryTheory.PreOneHypercover.sieve₀_cylinder, CategoryTheory.PreOneHypercover.oneToZero_map, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀, CategoryTheory.PreOneHypercover.instIsIsoH₀Inv, CategoryTheory.GrothendieckTopology.OneHypercover.id_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.instIsIsoH₀Hom, w₁₂_assoc, CategoryTheory.PreOneHypercover.instIsIsoH₁Inv, CategoryTheory.PreOneHypercover.isoMk_inv_s₀, 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₁, CategoryTheory.PreOneHypercover.isoMk_hom_s₀, mapMultiforkOfIsLimit_ι_assoc, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.PreOneHypercover.cylinderHom_s₁, comp_h₁, CategoryTheory.PreOneHypercover.inv_hom_s₀_apply, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₀, CategoryTheory.PreOneHypercover.cylinderHom_s₀, mapMultiforkOfIsLimit_ι, w₁₁_assoc, CategoryTheory.PreOneHypercover.hom_inv_h₀_assoc, CategoryTheory.PreOneHypercover.Homotopy.wr_assoc, CategoryTheory.PreOneHypercover.inv_hom_h₁, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₀, CategoryTheory.PreOneHypercover.comp_h₁, id_s₀, CategoryTheory.PreOneHypercover.cylinderHom_h₀, CategoryTheory.PreOneHypercover.hom_inv_s₀_apply, CategoryTheory.PreOneHypercover.cylinder_Y, CategoryTheory.PreOneHypercover.isoMk_inv_h₀, mapMulticospan_obj

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' 📖	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom CategoryTheory.PreZeroHypercover.Hom.h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.eqToHom s₁ DFunLike.coe Equiv CategoryTheory.PreOneHypercover.I₁ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.PreOneHypercover.congrIndexOneOfEq h₁ CategoryTheory.PreOneHypercover.Y CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso	—	—	CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_refl CategoryTheory.Category.comp_id CategoryTheory.PreOneHypercover.congrIndexOneOfEq_refl CategoryTheory.PreZeroHypercover.Hom.ext'
ext'_iff 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom h₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreOneHypercover.Y s₁ DFunLike.coe Equiv CategoryTheory.PreOneHypercover.I₁ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.PreOneHypercover.congrIndexOneOfEq CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.Iso.inv CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso CategoryTheory.eqToHom	—	CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_refl CategoryTheory.Category.comp_id ext'
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	—	—
mapMulticospan_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.WalkingMulticospan CategoryTheory.PreOneHypercover.multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory mapMulticospan Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.WalkingMulticospan.left CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom CategoryTheory.Limits.WalkingMulticospan.right s₁' CategoryTheory.Limits.WalkingMulticospan.Hom.id CategoryTheory.Limits.WalkingMulticospan.Hom.fst CategoryTheory.Limits.WalkingMulticospan.Hom.snd	—	—
mapMulticospan_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingMulticospan CategoryTheory.PreOneHypercover.multicospanShape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory mapMulticospan CategoryTheory.Limits.WalkingMulticospan.left CategoryTheory.PreZeroHypercover.Hom.s₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover toHom CategoryTheory.Limits.WalkingMulticospan.right s₁'	—	—
mapMultiforkOfIsLimit_comp 📖	mathematical	—	mapMultiforkOfIsLimit comp 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.Multifork.IsLimit.hom_ext mapMultiforkOfIsLimit_ι CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc mapMultiforkOfIsLimit_ι_assoc
mapMultiforkOfIsLimit_comp_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 comp	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMultiforkOfIsLimit_comp
mapMultiforkOfIsLimit_id 📖	mathematical	—	mapMultiforkOfIsLimit id CategoryTheory.Limits.Multifork.IsLimit.lift CategoryTheory.PreOneHypercover.multicospanShape CategoryTheory.PreOneHypercover.multicospanIndex CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.Multifork.ι CategoryTheory.Limits.Multifork.condition	—	CategoryTheory.Limits.Multifork.IsLimit.hom_ext CategoryTheory.Limits.Multifork.condition mapMultiforkOfIsLimit_ι CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Limits.Multifork.IsLimit.fac
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.PreOneHypercover.I₁'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	CategoryTheory.PreZeroHypercover.I₀ CategoryTheory.PreOneHypercover.toPreZeroHypercover CategoryTheory.PreOneHypercover.I₁ DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.PreOneHypercover.congrIndexOneOfEq	—	—	CategoryTheory.PreOneHypercover.congrIndexOneOfEq_refl

CategoryTheory.PreZeroHypercover

Definitions

Name	Category	Theorems
refineOneHypercover 📖	CompOp	7 math math: refineOneHypercover_I₁, refineOneHypercover_p₂, refineOneHypercover_toPreZeroHypercover, refineOneHypercover_p₁, refineOneHypercover_Y, CategoryTheory.instHasPullbacksRefineOneHypercover, sieve₁'_refineOneHypercover
toPreOneHypercover 📖	CompOp	22 math math: toPreOneHypercover_toPreZeroHypercover, toPreOneHypercover_p₁, toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks, toPreOneHypercover_I₁, toSaturateOfHasPullbacks_h₀, fromSaturateOfHasPullbacks_s₁, CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover_toPreOneHypercover, toSaturateOfHasPullbacks_s₀, toSaturateOfHasPullbacks_h₁, CategoryTheory.instHasPullbacksToPreOneHypercover, isLimit_toPreOneHypercover_type_iff, toSaturateOfHasPullbacks_s₁_snd, toSaturateOfHasPullbacks_s₁_obj, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, toSaturateOfHasPullbacks_s₁_fst, sectionsEquivOfHasPullbacks_symm_apply_val, toPreOneHypercover_Y, fromSaturateOfHasPullbacks_s₀, toPreOneHypercover_p₂, fromSaturateOfHasPullbacks_h₀, sectionsEquivOfHasPullbacks_apply_coe, fromSaturateOfHasPullbacks_h₁

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
refineOneHypercover_I₁ 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.I₁ refineOneHypercover I₀ CategoryTheory.Limits.pullback X f	—	—
refineOneHypercover_Y 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.Y refineOneHypercover X CategoryTheory.Limits.pullback f	—	—
refineOneHypercover_p₁ 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.p₁ refineOneHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.pullback f CategoryTheory.Limits.pullback.fst	—	—
refineOneHypercover_p₂ 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.p₂ refineOneHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.pullback f CategoryTheory.Limits.pullback.snd	—	—
refineOneHypercover_toPreZeroHypercover 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.toPreZeroHypercover refineOneHypercover	—	—
sieve₁'_refineOneHypercover 📖	mathematical	HasPullbacks	CategoryTheory.PreOneHypercover.sieve₁' refineOneHypercover CategoryTheory.instHasPullbacksRefineOneHypercover sieve₀ CategoryTheory.Limits.pullback X f	—	CategoryTheory.instHasPullbacksRefineOneHypercover CategoryTheory.PreOneHypercover.sieve₁'.eq_1 CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.PreOneHypercover.w
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 toPreZeroHypercover	—	—

---

← Back to Index