Zero

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

Statistics

Metric	Count
Definitions PreZeroHypercover, HasPullbacks, comp, h₀, id, s₀, I₀, X, add, bind, empty, f, fromShrink, instCategory, instUniqueI₀Singleton, inter, interFst, interLift, interSnd, isoMk, map, presieve₀, pullbackCoverOfLeft, pullbackCoverOfLeftIsoPullback₁, pullbackCoverOfRight, pullbackCoverOfRightIsoPullback₂, pullbackIso, pullback₁, pullback₂, reindex, restrictIndex, restrictIndexHom, shrink, sieve₀, sigmaOfIsColimit, singleton, sum, sumInl, sumInr, sumLift, toShrink, RespectsIso, ZeroHypercover, restrictFun, add, bind, instCategory, inter, isoMk, map, pullbackCoverOfLeft, pullbackCoverOfRight, pullback₁, pullback₂, reindex, restrictIndexOfSmall, singleton, sum, toPreZeroHypercover, weaken, preZeroHypercover	61
Theorems comp_h₀, comp_s₀, ext, ext', ext'_iff, ext_iff, id_h₀, id_s₀, sieve₀_le_sieve₀, w₀, w₀_assoc, add_I₀, add_X_none, add_X_some, add_f_nome, add_f_some, bind_I₀, bind_X, bind_f, comp_h₀, comp_s₀, empty_I₀, empty_X, empty_f, ext, ext_iff, hom_inv_h₀, hom_inv_h₀_assoc, hom_inv_s₀_apply, id_h₀, id_s₀, inj_sigmaOfIsColimit_f, inj_sigmaOfIsColimit_f_assoc, instIsEmptyI₀Empty, instIsIsoH₀Hom, instIsIsoH₀Inv, interFst_h₀, interFst_s₀, interLift_h₀, interLift_s₀, interSnd_h₀, interSnd_s₀, inter_I₀, inter_X, inter_def, inter_f, inv_hom_h₀, inv_hom_h₀_assoc, inv_hom_h₀_comp_f, inv_hom_h₀_comp_f_assoc, inv_hom_s₀_apply, inv_inv_h₀_comp_f, inv_inv_h₀_comp_f_assoc, isoMk_hom_h₀, isoMk_hom_s₀, isoMk_inv_h₀, isoMk_inv_s₀, map_I₀, map_X, map_f, presieve₀_add, presieve₀_empty, presieve₀_eq_presieve₀_iff, presieve₀_f, presieve₀_map, presieve₀_mem_iff_of_iso, presieve₀_mem_of_iso, presieve₀_pullback₁, presieve₀_reindex, presieve₀_restrictIndex_equiv, presieve₀_restrictIndex_le, presieve₀_shrink, presieve₀_sigmaOfIsColimit, presieve₀_singleton, presieve₀_sum, pullbackCoverOfLeft_I₀, pullbackCoverOfLeft_X, pullbackCoverOfLeft_f, pullbackCoverOfRight_I₀, pullbackCoverOfRight_X, pullbackCoverOfRight_f, pullbackIso_hom_h₀, pullbackIso_hom_s₀, pullbackIso_inv_h₀, pullbackIso_inv_s₀, pullback₁_I₀, pullback₁_X, pullback₁_f, pullback₂_I₀, pullback₂_X, pullback₂_f, reindex_I₀, reindex_X, reindex_f, restrictIndexHom_h₀, restrictIndexHom_s₀, restrictIndex_I₀, restrictIndex_X, restrictIndex_f, shrink_I₀, shrink_X, shrink_eq_shrink_of_presieve₀_eq_presieve₀, shrink_f, sieve₀_eq_of_iso, sieve₀_f, sigmaOfIsColimit_I₀, sigmaOfIsColimit_X, sigmaOfIsColimit_f, singleton_I₀, singleton_X, singleton_f, sumInl_h₀, sumInl_s₀, sumInr_h₀, sumInr_s₀, sumLift_h₀, sumLift_s₀, sum_I₀, sum_X, sum_X_inl, sum_X_inr, sum_f, sum_f_inl, sum_f_inr, of_forall_exists_iso, of_iso, inf, zeroHypercoverSmall, exists_restrictIndex_mem, mem₀, add_toPreZeroHypercover, bind_toPreZeroHypercover, comp_h₀, comp_s₀, id_h₀, id_s₀, instHasPullbackFOfHasPullbacksPresieve₀, instHasPullbackFOfHasPullbacksPresieve₀_1, instHasPullbacksPresieve₀OfHasPullbacks, instSmall, instSmallOfSmallI₀, instSmallPullback₁, inter_toPreZeroHypercover, isoMk_hom, isoMk_inv, map_toPreZeroHypercover, mem₀, presieve₀_mem_of_iso, pullbackCoverOfLeft_toPreZeroHypercover, pullbackCoverOfRight_toPreZeroHypercover, pullback₁_toPreZeroHypercover, pullback₂_toPreZeroHypercover, reindex_toPreZeroHypercover, restrictIndexOfSmall_toPreZeroHypercover, singleton_toPreZeroHypercover, sum_toPreZeroHypercover, weaken_toPreZeroHypercover, instRespectsIsoOfIsStableUnderBaseChange, instSmallComap, instSmallOfSmall, le_of_zeroHypercover, mem_iff_exists_zeroHypercover, exists_eq_preZeroHypercover, preZeroHypercover_I₀, preZeroHypercover_X, preZeroHypercover_f, presieve₀_preZeroHypercover	167
Total	228

CategoryTheory

Definitions

Name	Category	Theorems
PreZeroHypercover 📖	CompData	37 math math: PreZeroHypercover.isoMk_hom_h₀, PreZeroHypercover.inv_hom_h₀, PreZeroHypercover.inv_hom_h₀_comp_f_assoc, PreZeroHypercover.inv_hom_s₀_apply, PreOneHypercover.oneToZero_obj, AlgebraicGeometry.Scheme.Cover.comp_app, PreZeroHypercover.instIsIsoH₀Hom, Precoverage.ZeroHypercover.isoMk_hom, Presieve.exists_eq_preZeroHypercover, PreZeroHypercover.inv_hom_h₀_comp_f, PreZeroHypercover.inv_inv_h₀_comp_f, AlgebraicGeometry.Scheme.Cover.comp_idx_apply, PreZeroHypercover.isoMk_hom_s₀, AlgebraicGeometry.Scheme.Cover.id_idx_apply, PreOneHypercover.isoMk_inv_h₁, PreZeroHypercover.pullbackIso_hom_h₀, PreZeroHypercover.inv_hom_h₀_assoc, PreZeroHypercover.pullbackIso_hom_s₀, PreZeroHypercover.comp_s₀, PreOneHypercover.isoMk_inv_s₁, AlgebraicGeometry.Scheme.Cover.id_app, AlgebraicGeometry.Scheme.isClosedUnderIsomorphisms_quasiCompactCover, Precoverage.ZeroHypercover.isoMk_inv, PreZeroHypercover.hom_inv_h₀_assoc, PreZeroHypercover.instIsIsoH₀Inv, PreZeroHypercover.inv_inv_h₀_comp_f_assoc, PreZeroHypercover.hom_inv_s₀_apply, PreOneHypercover.oneToZero_map, PreZeroHypercover.comp_h₀, PreZeroHypercoverFamily.mem_precoverage_iff, PreZeroHypercover.hom_inv_h₀, PreZeroHypercover.id_h₀, PreZeroHypercover.pullbackIso_inv_h₀, PreZeroHypercover.isoMk_inv_h₀, PreZeroHypercover.isoMk_inv_s₀, PreZeroHypercover.id_s₀, PreZeroHypercover.pullbackIso_inv_s₀

CategoryTheory.PreZeroHypercover

Definitions

Name	Category	Theorems
HasPullbacks 📖	MathDef	2 math math: CategoryTheory.instHasPullbacksToPreOneHypercover, CategoryTheory.instHasPullbacksRefineOneHypercover
I₀ 📖	CompOp	251 math math: isoMk_hom_h₀, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc, AlgebraicGeometry.Scheme.coverOfIsIso_I₀, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_I₀, sum_f_inr, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_X, CategoryTheory.PreOneHypercover.isoMk_aux, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff, AlgebraicGeometry.Scheme.AffineCover.cover_I₀, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, CategoryTheory.PreOneHypercover.forkOfIsColimit_pt, AlgebraicGeometry.Scheme.Cover.iUnion_range, CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit_assoc, CategoryTheory.PreOneHypercover.inter_I₁, sigmaOfIsColimit_X, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_I₀, CategoryTheory.PreOneHypercover.multicospanIndex_fst, sum_f_inl, CategoryTheory.PreOneHypercover.cylinder_X, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_I₀, CategoryTheory.PreOneHypercover.cylinderHom_h₁, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj, singleton_I₀, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_I₀, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₀, AlgebraicGeometry.Scheme.affineOpenCover_I₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_I₀, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_I₀, refineOneHypercover_I₁, CategoryTheory.PreOneHypercover.map_I₀, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, AlgebraicGeometry.Scheme.affineOpenCover_idx, map_I₀, CategoryTheory.PreOneHypercover.multicospanIndex_right, reindex_I₀, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, interLift_h₀, CategoryTheory.PreOneHypercover.isoMk_aux_assoc, AlgebraicGeometry.Scheme.Cover.mkOfCovers_I₀, AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, add_f_nome, CategoryTheory.PreOneHypercover.multicospanShape_fst, instIsEmptyI₀Empty, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, restrictIndex_X, interLift_s₀, CategoryTheory.Presieve.preZeroHypercover_I₀, CategoryTheory.PreOneHypercover.multicospanIndex_snd, AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_ι, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, sum_X_inl, inj_sigmaOfIsColimit_f_assoc, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, reindex_f, isoMk_hom_s₀, AlgebraicGeometry.Scheme.Cover.trans_id, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_naturality, CategoryTheory.PreOneHypercover.congrIndexOneOfEq_naturality, pullback₂_I₀, AlgebraicGeometry.Scheme.directedAffineCover_I₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase_assoc, AlgebraicGeometry.Scheme.Pullback.gluing_J, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered, add_X_none, AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, reindex_X, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit, AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_naturality, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, sectionsSaturateEquiv_apply_coe, AlgebraicGeometry.Scheme.Cover.gluedCover_J, sumLift_s₀, CategoryTheory.PreOneHypercover.Hom.ext'_iff, CategoryTheory.PreOneHypercover.isoMk_inv_h₁, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_refl, CategoryTheory.PreOneHypercover.multicospanShape_L, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_naturality_assoc, CategoryTheory.PreOneHypercover.congrIndexOneOfEq_trans, pullbackCoverOfLeft_I₀, CategoryTheory.PreOneHypercover.congrIndexOneOfEq_equiv, AlgebraicGeometry.Scheme.Cover.toSigma_s₀, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, inter_f, interFst_s₀, pullback₁_I₀, CategoryTheory.PreOneHypercover.cylinder_I₀, CategoryTheory.PreOneHypercover.inter_p₂, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible, bind_f, AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_map, sum_X, CategoryTheory.PreOneHypercover.Y'_apply, pullbackIso_hom_s₀, interSnd_h₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, CategoryTheory.PreOneHypercover.isoMk_hom_h₀, AlgebraicGeometry.Scheme.Cover.sigma_X, add_I₀, CategoryTheory.PreOneHypercover.isoMk_inv_s₁, AlgebraicGeometry.Scheme.Cover.nonempty_of_nonempty, CategoryTheory.PreOneHypercover.cylinder_f, pullbackCoverOfRight_I₀, AlgebraicGeometry.instSurjectiveDescI₀SchemeF, add_X_some, presieve₀_sigmaOfIsColimit, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_I₀, AlgebraicGeometry.Scheme.Cover.ulift_I₀, CategoryTheory.PreOneHypercover.inv_hom_h₁_assoc, presieve₀_pullback₁, CategoryTheory.PreOneHypercover.cylinder_I₁, CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover, AlgebraicGeometry.Scheme.Cover.mem_propQCTopology, AlgebraicGeometry.Scheme.Cover.exists_of_trans_eq_trans, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_I₀, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₀, CategoryTheory.PreOneHypercover.hom_inv_h₁, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, AlgebraicGeometry.Scheme.Cover.pushforwardIso_f, AlgebraicGeometry.Scheme.Cover.copy_I₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f, inter_X, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.Scheme.Cover.Hom.sigma_h₀, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, CategoryTheory.PreOneHypercover.sieve₀_cylinder, AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id, AlgebraicGeometry.Scheme.Cover.toSigma_h₀, restrictIndex_I₀, AlgebraicGeometry.Scheme.directedAffineCover_trans, CategoryTheory.PreOneHypercover.congrIndexOneOfEq_congrFun, sumInl_s₀, inj_sigmaOfIsColimit_f, inter_def, AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, CategoryTheory.PreOneHypercover.multicospanShape_snd, CategoryTheory.PreOneHypercover.isoMk_hom_s₁, AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_pt, AlgebraicGeometry.Scheme.Cover.exists_eq, ext_iff, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, bind_X, AlgebraicGeometry.sigmaOpenCover_I₀, AlgebraicGeometry.Scheme.Cover.Hom.sigma_s₀, CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff, AlgebraicGeometry.Scheme.Cover.sigma_I₀, AlgebraicGeometry.Scheme.Cover.pushforwardIso_I₀, AlgebraicGeometry.Scheme.Cover.trans_comp, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, CategoryTheory.PreOneHypercover.inter_Y, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_I₀, Hom.id_s₀, sumLift_h₀, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, CategoryTheory.PreOneHypercover.isoMk_inv_s₀, AlgebraicGeometry.Scheme.Hom.cover_I₀, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_I₀, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, AlgebraicGeometry.Scheme.OpenCover.restrict_I₀, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_I₀, CategoryTheory.PreOneHypercover.interSnd_s₁, CategoryTheory.PreOneHypercover.toPullback_cylinder, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, AlgebraicGeometry.Scheme.Cover.presieve₀_sigma, AlgebraicGeometry.Scheme.GlueData.oneHypercover_I₀, AlgebraicGeometry.Scheme.Cover.pushforwardIso_X, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, Hom.comp_h₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, interFst_h₀, CategoryTheory.PreOneHypercover.inter_p₁, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, sum_I₀, AlgebraicGeometry.Scheme.mem_pretopology_iff, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_I₀, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, bind_I₀, AlgebraicGeometry.Scheme.GlueData.openCover_I₀, sumInr_s₀, CategoryTheory.PreOneHypercover.sieve₁_inter, sectionsSaturateEquiv_symm_apply_val, CategoryTheory.PreOneHypercover.cylinder_p₁, sigmaOfIsColimit_I₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, CategoryTheory.PreOneHypercover.isoMk_hom_s₀, CategoryTheory.PreOneHypercover.cylinder_p₂, TopCat.exists_mem_zeroHypercover_range, CategoryTheory.PreOneHypercover.cylinderHom_s₁, AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f, AlgebraicGeometry.quasiCompactCover_iff, isoMk_inv_h₀, inter_I₀, AlgebraicGeometry.Scheme.Cover.mem_pretopology, CategoryTheory.PreOneHypercover.interFst_s₁, isoMk_inv_s₀, Hom.comp_s₀, sectionsEquivOfHasPullbacks_symm_apply_val, presieve₀_restrictIndex_equiv, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj, AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected, sigmaOfIsColimit_f, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, CategoryTheory.PreOneHypercover.cylinderHom_s₀, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X, add_f_some, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, shrink_I₀, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_I₀, CategoryTheory.PreOneHypercover.congrIndexOneOfEq_refl, CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit_assoc, sum_f, empty_I₀, AlgebraicGeometry.Scheme.Cover.sigma_f, CategoryTheory.PreOneHypercover.inv_hom_h₁, sum_X_inr, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor, CategoryTheory.PreOneHypercover.cylinderHom_h₀, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, sectionsEquivOfHasPullbacks_apply_coe, CategoryTheory.PreOneHypercover.cylinder_Y, CategoryTheory.PreOneHypercover.isoMk_inv_h₀, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, CategoryTheory.PreOneHypercover.isoMk_hom_h₁, pullbackIso_inv_s₀, interSnd_s₀
X 📖	CompOp	400 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_p₁, isoMk_hom_h₀, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc, inv_hom_h₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_X, AlgebraicGeometry.instIsAffineXSchemeCover, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover, pullbackCoverOfRight_X, pullback₁_X, CategoryTheory.PreOneHypercover.inv_hom_h₀_assoc, AlgebraicGeometry.instIsLocallyArtinianXScheme, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc, CategoryTheory.PreOneHypercover.forkOfIsColimit_pt, AlgebraicGeometry.Scheme.Cover.iUnion_range, CategoryTheory.PreOneHypercover.Homotopy.wl, inv_hom_h₀_comp_f_assoc, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc, CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit_assoc, CategoryTheory.PreOneHypercover.Hom.w₁₁, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst, AlgebraicGeometry.sigmaOpenCover_X, sigmaOfIsColimit_X, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, CategoryTheory.PreOneHypercover.multicospanIndex_fst, AlgebraicGeometry.Scheme.Cover.copy_X, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X, CategoryTheory.PreOneHypercover.cylinder_X, CategoryTheory.PreOneHypercover.cylinderHom_h₁, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, CategoryTheory.PreOneHypercover.Hom.comp_h₀, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰S, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₁, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle, AlgebraicGeometry.Scheme.Cover.gluedCover_t, AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.Cover.gluedCover_U, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, refineOneHypercover_I₁, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected_assoc, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd, AlgebraicGeometry.Scheme.Cover.comp_app, instIsIsoH₀Hom, CategoryTheory.PreOneHypercover.map_X, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, pullback₂_X, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₁_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, inv_hom_h₀_comp_f, toPreOneHypercover_p₁, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected, interLift_h₀, inv_inv_h₀_comp_f, AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff, AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback, AlgebraicGeometry.IsLocalAtSource.iff_of_openCover, CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', singleton_X, restrictIndexHom_h₀, Hom.id_h₀, CategoryTheory.PreOneHypercover.Homotopy.wl_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, CategoryTheory.Precoverage.ZeroHypercover.id_h₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, AlgebraicGeometry.Scheme.Pullback.cocycle, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, refineOneHypercover_p₂, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₂_assoc, AlgebraicGeometry.instIsAffineXSchemeAffineCover, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, restrictIndex_X, AlgebraicGeometry.Scheme.Hom.cover_X, CategoryTheory.PreOneHypercover.multifork_ι, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc, CategoryTheory.PreOneHypercover.id_h₀, toSaturateOfHasPullbacks_h₀, AlgebraicGeometry.Scheme.Cover.gluedCover_V, CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback, AlgebraicGeometry.HasAffineProperty.iff_of_openCover, Hom.w₀, CategoryTheory.PreOneHypercover.multicospanIndex_snd, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Cover.ulift_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst, AlgebraicGeometry.Scheme.Cover.covers, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀, sum_X_inl, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, AlgebraicGeometry.QuasiCompactCover.exists_hom, CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁, inj_sigmaOfIsColimit_f_assoc, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, CategoryTheory.PreOneHypercover.map_p₁, CategoryTheory.Presieve.preZeroHypercover_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst, AlgebraicGeometry.Scheme.isAffine_affineBasisCover, AlgebraicGeometry.Scheme.Cover.trans_id, AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source, CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁', AlgebraicGeometry.Scheme.Pullback.t_snd, CategoryTheory.MorphismProperty.IsLocalAtSource.comp, CategoryTheory.PreOneHypercover.hom_inv_h₀, AlgebraicGeometry.Scheme.Pullback.gluing_f, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, AlgebraicGeometry.Scheme.Cover.Hom.w, add_X_none, reindex_X, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X, pullbackCoverOfLeft_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.Scheme.OpenCover.restrict_f, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.Scheme.Cover.mkOfCovers_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms, Hom.ext'_iff, CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit, AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, map_X, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, sectionsSaturateEquiv_apply_coe, pullbackCoverOfLeft_f, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, TopCat.isOpenEmbedding_f_zeroHypercover, pullback₂_f, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd, AlgebraicGeometry.Scheme.Cover.trans_map, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_X, CategoryTheory.PreOneHypercover.IsStronglySheafFor.map_amalgamate, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, inter_f, pullbackIso_hom_h₀, AlgebraicGeometry.QuasiCompactCover.instPullback₁Scheme, inv_hom_h₀_assoc, shrink_X, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, CategoryTheory.PreOneHypercover.inter_p₂, map_f, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible, AlgebraicGeometry.Scheme.GlueData.openCover_X, bind_f, AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, sum_X, AlgebraicGeometry.Scheme.directedAffineCover_X, AlgebraicGeometry.Scheme.Cover.property_trans, CategoryTheory.PreOneHypercover.multicospanIndex_left, interSnd_h₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, CategoryTheory.PreOneHypercover.isoMk_hom_h₀, AlgebraicGeometry.Scheme.Cover.sigma_X, AlgebraicGeometry.Scheme.Pullback.gluing_U, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst, CategoryTheory.PreOneHypercover.inv_hom_h₀, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₂, AlgebraicGeometry.Scheme.Cover.id_app, CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_X, AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionTrans, AlgebraicGeometry.instSurjectiveDescI₀SchemeF, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, add_X_some, presieve₀_sigmaOfIsColimit, presieve₀_pullback₁, CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover, AlgebraicGeometry.Scheme.Cover.mem_propQCTopology, AlgebraicGeometry.Scheme.Cover.exists_of_trans_eq_trans, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_X, empty_X, hom_inv_h₀_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, pullbackCoverOfRight_f, CategoryTheory.PreOneHypercover.w, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc, instIsIsoH₀Inv, CategoryTheory.PreOneHypercover.Hom.id_h₀, inv_inv_h₀_comp_f_assoc, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, AlgebraicGeometry.Scheme.Cover.pushforwardIso_f, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_X, CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover, inter_X, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.Scheme.Cover.gluedCover_f, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X, presieve₀_f, AlgebraicGeometry.Scheme.Cover.Hom.sigma_h₀, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, CategoryTheory.PreOneHypercover.sieve₀_cylinder, AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_X, comp_h₀, AlgebraicGeometry.Scheme.Cover.toSigma_h₀, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd, AlgebraicGeometry.Scheme.coverOfIsIso_X, CategoryTheory.PreOneHypercover.instIsIsoH₀Inv, inj_sigmaOfIsColimit_f, inter_def, AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.prop_trans, CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1, sumInr_h₀, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc, CategoryTheory.PreOneHypercover.instIsIsoH₀Hom, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, ext_iff, refineOneHypercover_p₁, AlgebraicGeometry.Scheme.AffineCover.cover_X, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd, hom_inv_h₀, AlgebraicGeometry.Scheme.affineBasisCover_obj, id_h₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, bind_X, CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff, AlgebraicGeometry.Scheme.instEtaleF, CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc, Hom.w₀_assoc, toSaturateOfHasPullbacks_s₁_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd, AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, CategoryTheory.PreOneHypercover.sieve₁_apply, toSaturateOfHasPullbacks_s₁_obj, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, AlgebraicGeometry.Scheme.Cover.trans_comp, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, AlgebraicGeometry.Scheme.GlueData.oneHypercover_X, refineOneHypercover_Y, CategoryTheory.PreOneHypercover.inter_Y, pullbackIso_inv_h₀, sumLift_h₀, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.Scheme.instWeaklyEtaleF, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_p₁_assoc, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.instIsLocallyNoetherianXScheme, CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, Relation.w, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, AlgebraicGeometry.isLocallyArtinian_iff_openCover, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, AlgebraicGeometry.Scheme.instIsOpenImmersionF, toSaturateOfHasPullbacks_s₁_fst, sumInl_h₀, CategoryTheory.PreOneHypercover.toPullback_cylinder, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd, sieve₀_f, AlgebraicGeometry.Scheme.Cover.presieve₀_sigma, AlgebraicGeometry.Scheme.Cover.pushforwardIso_X, CategoryTheory.ObjectProperty.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀, Hom.comp_h₀, CategoryTheory.PreOneHypercover.Hom.w₁₂, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, interFst_h₀, CategoryTheory.PreOneHypercover.inter_p₁, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.Cover.map_prop, AlgebraicGeometry.Scheme.Cover.LocallyDirected.w, CategoryTheory.PreOneHypercover.comp_h₀, AlgebraicGeometry.Scheme.Cover.Over.isOver_map, CategoryTheory.PreOneHypercover.Homotopy.wr, pullback₁_f, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.Scheme.mem_pretopology_iff, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, bind_I₀, AlgebraicGeometry.Scheme.Pullback.t_snd_assoc, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, CategoryTheory.PreOneHypercover.sieve₁_inter, sectionsSaturateEquiv_symm_apply_val, CategoryTheory.PreOneHypercover.cylinder_p₁, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι_assoc, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms_assoc, TopCat.exists_mem_zeroHypercover_range, CategoryTheory.PreOneHypercover.map_f, AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f, AlgebraicGeometry.Scheme.OpenCover.restrict_X, isoMk_inv_h₀, AlgebraicGeometry.Scheme.Cover.mem_pretopology, AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst, sectionsEquivOfHasPullbacks_symm_apply_val, toPreOneHypercover_Y, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj, AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc, sigmaOfIsColimit_f, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, CategoryTheory.PreOneHypercover.hom_inv_h₀_assoc, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, AlgebraicGeometry.Scheme.Cover.pullbackHom_map, shrink_I₀, AlgebraicGeometry.Scheme.isAffine_affineCover, CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit_assoc, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, sum_f, CategoryTheory.PreOneHypercover.Homotopy.wr_assoc, CategoryTheory.PreOneHypercover.map_p₂, CategoryTheory.Precoverage.ZeroHypercover.comp_h₀, toPreOneHypercover_p₂, AlgebraicGeometry.Scheme.Cover.sigma_f, fromSaturateOfHasPullbacks_h₀, sum_X_inr, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_X, CategoryTheory.PreOneHypercover.cylinderHom_h₀, AlgebraicGeometry.QuasiCompactCover.instPullback₂Scheme, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc, sectionsEquivOfHasPullbacks_apply_coe, CategoryTheory.PreOneHypercover.cylinder_Y, CategoryTheory.PreOneHypercover.isoMk_inv_h₀, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, fromSaturateOfHasPullbacks_h₁, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, sieve₁'_refineOneHypercover, AlgebraicGeometry.Scheme.isAffine_affineOpenCover
add 📖	CompOp	8 math math: add_f_nome, add_X_none, add_I₀, add_X_some, CategoryTheory.Precoverage.ZeroHypercover.add_toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.add_toPreZeroHypercover, add_f_some, presieve₀_add
bind 📖	CompOp	13 math math: interLift_h₀, inter_f, CategoryTheory.PreOneHypercover.inter_p₂, bind_f, interSnd_h₀, AlgebraicGeometry.QuasiCompactCover.instBindScheme, CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover, inter_X, inter_def, bind_X, interFst_h₀, CategoryTheory.PreOneHypercover.inter_p₁, bind_I₀
empty 📖	CompOp	5 math math: instIsEmptyI₀Empty, empty_f, presieve₀_empty, empty_X, empty_I₀
f 📖	CompOp	306 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc, sum_f_inr, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, pullbackCoverOfRight_X, pullback₁_X, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc, AlgebraicGeometry.Scheme.Cover.copy_f, AlgebraicGeometry.Scheme.Cover.iUnion_range, inv_hom_h₀_comp_f_assoc, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, sum_f_inl, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X, CategoryTheory.PreOneHypercover.cylinderHom_h₁, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle, AlgebraicGeometry.Scheme.Cover.gluedCover_t, AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map, refineOneHypercover_I₁, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected_assoc, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, pullback₂_X, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, inv_hom_h₀_comp_f, toPreOneHypercover_p₁, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected, interLift_h₀, inv_inv_h₀_comp_f, AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff, AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback, AlgebraicGeometry.IsLocalAtSource.iff_of_openCover, CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁', AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, add_f_nome, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, AlgebraicGeometry.Scheme.Pullback.cocycle, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, refineOneHypercover_p₂, AlgebraicGeometry.Scheme.GlueData.openCover_f, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, AlgebraicGeometry.Scheme.directedAffineCover_f, CategoryTheory.PreOneHypercover.multifork_ι, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.gluedCover_V, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f, AlgebraicGeometry.HasAffineProperty.iff_of_openCover, Hom.w₀, AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_f, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst, AlgebraicGeometry.Scheme.Cover.covers, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_f, CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁, inj_sigmaOfIsColimit_f_assoc, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, reindex_f, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst, AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source, CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁', AlgebraicGeometry.Scheme.Pullback.t_snd, CategoryTheory.MorphismProperty.IsLocalAtSource.comp, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase_assoc, AlgebraicGeometry.Scheme.Pullback.gluing_f, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, AlgebraicGeometry.Scheme.Cover.Hom.w, CategoryTheory.Presieve.preZeroHypercover_f, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X, pullbackCoverOfLeft_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.Scheme.OpenCover.restrict_f, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms, AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_openCover_map, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, sectionsSaturateEquiv_apply_coe, empty_f, AlgebraicGeometry.Scheme.AffineCover.cover_f, pullbackCoverOfLeft_f, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, TopCat.isOpenEmbedding_f_zeroHypercover, pullback₂_f, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd, AlgebraicGeometry.Scheme.Cover.trans_map, CategoryTheory.PreOneHypercover.IsStronglySheafFor.map_amalgamate, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, inter_f, pullbackIso_hom_h₀, AlgebraicGeometry.QuasiCompactCover.instPullback₁Scheme, singleton_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, CategoryTheory.PreOneHypercover.inter_p₂, map_f, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible, bind_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, interSnd_h₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, AlgebraicGeometry.Scheme.Pullback.gluing_U, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst, CategoryTheory.PreOneHypercover.cylinder_f, AlgebraicGeometry.Scheme.Hom.cover_f, CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.Cover.ulift_f, AlgebraicGeometry.instSurjectiveDescI₀SchemeF, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, presieve₀_sigmaOfIsColimit, presieve₀_pullback₁, CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover, AlgebraicGeometry.Scheme.Cover.mem_propQCTopology, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_f, pullbackCoverOfRight_f, CategoryTheory.PreOneHypercover.w, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc, inv_inv_h₀_comp_f_assoc, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, AlgebraicGeometry.Scheme.Cover.pushforwardIso_f, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f, inter_X, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.Scheme.Cover.gluedCover_f, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, presieve₀_f, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, CategoryTheory.PreOneHypercover.sieve₀_cylinder, restrictIndex_f, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd, inj_sigmaOfIsColimit_f, inter_def, CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_f, CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, ext_iff, refineOneHypercover_p₁, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff, AlgebraicGeometry.Scheme.instEtaleF, Hom.w₀_assoc, toSaturateOfHasPullbacks_s₁_snd, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, toSaturateOfHasPullbacks_s₁_obj, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, refineOneHypercover_Y, CategoryTheory.PreOneHypercover.inter_Y, pullbackIso_inv_h₀, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.Scheme.coverOfIsIso_f, AlgebraicGeometry.Scheme.instWeaklyEtaleF, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.sigmaOpenCover_f, CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, Relation.w, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, AlgebraicGeometry.Scheme.instIsOpenImmersionF, toSaturateOfHasPullbacks_s₁_fst, AlgebraicGeometry.Scheme.affineOpenCover_f, CategoryTheory.PreOneHypercover.toPullback_cylinder, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd, sieve₀_f, AlgebraicGeometry.Scheme.Cover.presieve₀_sigma, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, interFst_h₀, CategoryTheory.PreOneHypercover.inter_p₁, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.Cover.map_prop, AlgebraicGeometry.Scheme.Cover.LocallyDirected.w, AlgebraicGeometry.Scheme.Cover.Over.isOver_map, pullback₁_f, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd, AlgebraicGeometry.Scheme.Cover.mkOfCovers_f, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.Scheme.mem_pretopology_iff, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, AlgebraicGeometry.Scheme.Pullback.t_snd_assoc, AlgebraicGeometry.Scheme.GlueData.oneHypercover_f, CategoryTheory.PreOneHypercover.sieve₁_inter, sectionsSaturateEquiv_symm_apply_val, CategoryTheory.PreOneHypercover.cylinder_p₁, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms_assoc, TopCat.exists_mem_zeroHypercover_range, CategoryTheory.PreOneHypercover.map_f, AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f, AlgebraicGeometry.quasiCompactCover_iff, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.Scheme.Cover.mem_pretopology, AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, sectionsEquivOfHasPullbacks_symm_apply_val, toPreOneHypercover_Y, CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj, AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc, sigmaOfIsColimit_f, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X, CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, add_f_some, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, AlgebraicGeometry.Scheme.Cover.pullbackHom_map, shrink_I₀, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, sum_f, toPreOneHypercover_p₂, AlgebraicGeometry.Scheme.Cover.sigma_f, shrink_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_X, CategoryTheory.PreOneHypercover.cylinderHom_h₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase, AlgebraicGeometry.QuasiCompactCover.instPullback₂Scheme, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.ι_fromGlued, sectionsEquivOfHasPullbacks_apply_coe, CategoryTheory.PreOneHypercover.cylinder_Y, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, fromSaturateOfHasPullbacks_h₁, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, sieve₁'_refineOneHypercover
fromShrink 📖	CompOp	—
instCategory 📖	CompOp	35 math math: isoMk_hom_h₀, inv_hom_h₀, inv_hom_h₀_comp_f_assoc, inv_hom_s₀_apply, CategoryTheory.PreOneHypercover.oneToZero_obj, AlgebraicGeometry.Scheme.Cover.comp_app, instIsIsoH₀Hom, CategoryTheory.Precoverage.ZeroHypercover.isoMk_hom, inv_hom_h₀_comp_f, inv_inv_h₀_comp_f, AlgebraicGeometry.Scheme.Cover.comp_idx_apply, isoMk_hom_s₀, AlgebraicGeometry.Scheme.Cover.id_idx_apply, CategoryTheory.PreOneHypercover.isoMk_inv_h₁, pullbackIso_hom_h₀, inv_hom_h₀_assoc, pullbackIso_hom_s₀, comp_s₀, CategoryTheory.PreOneHypercover.isoMk_inv_s₁, AlgebraicGeometry.Scheme.Cover.id_app, AlgebraicGeometry.Scheme.isClosedUnderIsomorphisms_quasiCompactCover, CategoryTheory.Precoverage.ZeroHypercover.isoMk_inv, hom_inv_h₀_assoc, instIsIsoH₀Inv, inv_inv_h₀_comp_f_assoc, hom_inv_s₀_apply, CategoryTheory.PreOneHypercover.oneToZero_map, comp_h₀, hom_inv_h₀, id_h₀, pullbackIso_inv_h₀, isoMk_inv_h₀, isoMk_inv_s₀, id_s₀, pullbackIso_inv_s₀
instUniqueI₀Singleton 📖	CompOp	—
inter 📖	CompOp	12 math math: interLift_h₀, interLift_s₀, CategoryTheory.PreOneHypercover.inter_toPreZeroHypercover, inter_f, interFst_s₀, interSnd_h₀, inter_X, inter_def, CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover, interFst_h₀, inter_I₀, interSnd_s₀
interFst 📖	CompOp	3 math math: interFst_s₀, CategoryTheory.PreOneHypercover.interFst_toHom, interFst_h₀
interLift 📖	CompOp	2 math math: interLift_h₀, interLift_s₀
interSnd 📖	CompOp	3 math math: CategoryTheory.PreOneHypercover.interSnd_toHom, interSnd_h₀, interSnd_s₀
isoMk 📖	CompOp	6 math math: isoMk_hom_h₀, isoMk_hom_s₀, CategoryTheory.PreOneHypercover.isoMk_inv_h₁, CategoryTheory.PreOneHypercover.isoMk_inv_s₁, isoMk_inv_h₀, isoMk_inv_s₀
map 📖	CompOp	5 math math: map_I₀, presieve₀_map, map_X, map_f, CategoryTheory.Precoverage.ZeroHypercover.map_toPreZeroHypercover
presieve₀ 📖	CompOp	39 math math: AlgebraicGeometry.Scheme.mem_propQCPrecoverage_iff_exists_quasiCompactCover, presieve₀_mem_of_iso, CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_presieve₀, CategoryTheory.Presieve.exists_eq_preZeroHypercover, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, CategoryTheory.Precoverage.preZeroHypercoverFamily_property, isSheafFor_iff_of_iso, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small, presieve₀_mem_iff_of_iso, presieve₀_map, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks, presieve₀_restrictIndex_le, shrink_X, AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff, CategoryTheory.Presieve.presieve₀_preZeroHypercover, presieve₀_sigmaOfIsColimit, presieve₀_pullback₁, CategoryTheory.Precoverage.ZeroHypercover.presieve₀_mem_of_iso, presieve₀_empty, presieve₀_f, CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀, CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff, isLimit_toPreOneHypercover_type_iff, presieve₀_shrink, presieve₀_eq_presieve₀_iff, presieve₀_sum, CategoryTheory.Precoverage.RespectsIso.of_iso, CategoryTheory.Precoverage.ZeroHypercover.mem₀, AlgebraicGeometry.Scheme.Cover.presieve₀_sigma, presieve₀_singleton, CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.isSeparatedFor_presieve₀, presieve₀_mem_precoverage_iff, presieve₀_restrictIndex_equiv, presieve₀_add, presieve₀_reindex, isLimit_saturate_type_iff, shrink_f, AlgebraicGeometry.Scheme.Hom.presieve₀_cover
pullbackCoverOfLeft 📖	CompOp	4 math math: pullbackCoverOfLeft_X, pullbackCoverOfLeft_f, pullbackCoverOfLeft_I₀, CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft_toPreZeroHypercover
pullbackCoverOfLeftIsoPullback₁ 📖	CompOp	—
pullbackCoverOfRight 📖	CompOp	4 math math: pullbackCoverOfRight_X, CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight_toPreZeroHypercover, pullbackCoverOfRight_I₀, pullbackCoverOfRight_f
pullbackCoverOfRightIsoPullback₂ 📖	CompOp	—
pullbackIso 📖	CompOp	4 math math: pullbackIso_hom_h₀, pullbackIso_hom_s₀, pullbackIso_inv_h₀, pullbackIso_inv_s₀
pullback₁ 📖	CompOp	17 math math: CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, pullback₁_X, interLift_h₀, inter_f, pullbackIso_hom_h₀, AlgebraicGeometry.QuasiCompactCover.instPullback₁Scheme, pullback₁_I₀, CategoryTheory.PreOneHypercover.inter_p₂, pullbackIso_hom_s₀, interSnd_h₀, inter_X, inter_def, pullbackIso_inv_h₀, interFst_h₀, CategoryTheory.PreOneHypercover.inter_p₁, pullback₁_f, pullbackIso_inv_s₀
pullback₂ 📖	CompOp	10 math math: pullback₂_X, CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover, pullback₂_I₀, pullback₂_f, pullbackIso_hom_h₀, pullbackIso_hom_s₀, presieve₀_pullback₁, pullbackIso_inv_h₀, AlgebraicGeometry.QuasiCompactCover.instPullback₂Scheme, pullbackIso_inv_s₀
reindex 📖	CompOp	6 math math: reindex_I₀, reindex_f, reindex_X, inter_def, CategoryTheory.Precoverage.ZeroHypercover.reindex_toPreZeroHypercover, presieve₀_reindex
restrictIndex 📖	CompOp	10 math math: CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem, restrictIndexHom_h₀, restrictIndexHom_s₀, restrictIndex_X, CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover, presieve₀_restrictIndex_le, restrictIndex_f, CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀, restrictIndex_I₀, presieve₀_restrictIndex_equiv
restrictIndexHom 📖	CompOp	2 math math: restrictIndexHom_h₀, restrictIndexHom_s₀
shrink 📖	CompOp	8 math math: AlgebraicGeometry.Scheme.quasiCompactCover_shrink_iff, shrink_X, CategoryTheory.PreZeroHypercoverFamily.iff_shrink, presieve₀_shrink, presieve₀_eq_presieve₀_iff, shrink_I₀, shrink_eq_shrink_of_presieve₀_eq_presieve₀, shrink_f
sieve₀ 📖	CompOp	15 math math: CategoryTheory.GrothendieckTopology.OneHypercover.mem₀, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', CategoryTheory.Functor.OneHypercoverDenseData.mem₀, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, CategoryTheory.PreOneHypercover.sieve₀_cylinder, sieve₀_eq_of_iso, sieve₀_f, CategoryTheory.PreOneHypercover.sieve₀_trivial, Hom.sieve₀_le_sieve₀, sieve₁'_refineOneHypercover
sigmaOfIsColimit 📖	CompOp	7 math math: sigmaOfIsColimit_X, inj_sigmaOfIsColimit_f_assoc, presieve₀_sigmaOfIsColimit, inj_sigmaOfIsColimit_f, CategoryTheory.PreOneHypercover.sigmaOfIsColimit_toPreZeroHypercover, sigmaOfIsColimit_I₀, sigmaOfIsColimit_f
singleton 📖	CompOp	7 math math: singleton_I₀, singleton_X, CategoryTheory.PreOneHypercover.trivial_toPreZeroHypercover, singleton_f, CategoryTheory.Precoverage.ZeroHypercover.singleton_toPreZeroHypercover, AlgebraicGeometry.QuasiCompactCover.singleton, presieve₀_singleton
sum 📖	CompOp	17 math math: sum_f_inr, sum_f_inl, sum_X_inl, sumLift_s₀, CategoryTheory.Precoverage.ZeroHypercover.sum_toPreZeroHypercover, sum_X, sumInl_s₀, AlgebraicGeometry.QuasiCompactCover.instSumScheme_1, sumInr_h₀, presieve₀_sum, sumLift_h₀, sumInl_h₀, sum_I₀, sumInr_s₀, sum_f, sum_X_inr, AlgebraicGeometry.QuasiCompactCover.instSumScheme
sumInl 📖	CompOp	2 math math: sumInl_s₀, sumInl_h₀
sumInr 📖	CompOp	2 math math: sumInr_h₀, sumInr_s₀
sumLift 📖	CompOp	2 math math: sumLift_s₀, sumLift_h₀
toShrink 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_I₀ 📖	mathematical	—	I₀ add	—	—
add_X_none 📖	mathematical	—	X add I₀	—	—
add_X_some 📖	mathematical	—	X add I₀	—	—
add_f_nome 📖	mathematical	—	f add I₀	—	—
add_f_some 📖	mathematical	—	f add I₀	—	—
bind_I₀ 📖	mathematical	—	I₀ bind X	—	—
bind_X 📖	mathematical	—	X bind I₀	—	—
bind_f 📖	mathematical	—	f bind CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X I₀	—	—
comp_h₀ 📖	mathematical	—	Hom.h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory X Hom.s₀	—	—
comp_s₀ 📖	mathematical	—	Hom.s₀ CategoryTheory.CategoryStruct.comp CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
empty_I₀ 📖	mathematical	—	I₀ empty	—	—
empty_X 📖	mathematical	—	X empty	—	—
empty_f 📖	mathematical	—	f empty Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	I₀ X f	—	—	—
ext_iff 📖	mathematical	—	I₀ X f	—	ext
hom_inv_h₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.s₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory CategoryTheory.Iso.inv 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 X Hom.s₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory Hom.h₀ CategoryTheory.Iso.inv CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_h₀
hom_inv_s₀_apply 📖	mathematical	—	Hom.s₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id
id_h₀ 📖	mathematical	—	Hom.h₀ CategoryTheory.CategoryStruct.id CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory X	—	—
id_s₀ 📖	mathematical	—	Hom.s₀ CategoryTheory.CategoryStruct.id CategoryTheory.PreZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
inj_sigmaOfIsColimit_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₀ CategoryTheory.discreteCategory CategoryTheory.Discrete.functor f sigmaOfIsColimit	—	CategoryTheory.Limits.Cofan.IsColimit.fac
inj_sigmaOfIsColimit_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₀ CategoryTheory.discreteCategory CategoryTheory.Discrete.functor f sigmaOfIsColimit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inj_sigmaOfIsColimit_f
instIsEmptyI₀Empty 📖	mathematical	—	IsEmpty I₀ empty	—	—
instIsIsoH₀Hom 📖	mathematical	—	CategoryTheory.IsIso X Hom.s₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory 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 X Hom.s₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory Hom.h₀	—	CategoryTheory.IsIso.of_isIso_fac_right instIsIsoH₀Hom CategoryTheory.instIsIsoEqToHom inv_hom_h₀
interFst_h₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.h₀ inter interFst CategoryTheory.Limits.pullback.fst X I₀ DFunLike.coe Equiv bind pullback₁ f EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd	—	—
interFst_s₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.s₀ inter interFst I₀	—	—
interLift_h₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.h₀ inter interLift CategoryTheory.Limits.pullback.lift X I₀ DFunLike.coe Equiv bind pullback₁ f EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd Hom.s₀	—	—
interLift_s₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.s₀ inter interLift I₀	—	—
interSnd_h₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.h₀ inter interSnd CategoryTheory.Limits.pullback.snd X I₀ DFunLike.coe Equiv bind pullback₁ f EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd	—	—
interSnd_s₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.s₀ inter interSnd I₀	—	—
inter_I₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	I₀ inter	—	—
inter_X 📖	mathematical	CategoryTheory.Limits.HasPullback X f	X inter CategoryTheory.Limits.pullback I₀ DFunLike.coe Equiv EquivLike.toFunLike bind pullback₁ f Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd	—	—
inter_def 📖	mathematical	CategoryTheory.Limits.HasPullback X f	inter reindex bind pullback₁ X f I₀ Equiv.symm Equiv.sigmaEquivProd	—	—
inter_f 📖	mathematical	CategoryTheory.Limits.HasPullback X f	f inter CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback X I₀ DFunLike.coe Equiv EquivLike.toFunLike bind pullback₁ Equiv.instEquivLike Equiv.symm Equiv.sigmaEquivProd CategoryTheory.Limits.pullback.fst	—	—
inv_hom_h₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.s₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory CategoryTheory.Iso.hom 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 X Hom.s₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory Hom.h₀ CategoryTheory.Iso.hom CategoryTheory.eqToHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_h₀
inv_hom_h₀_comp_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.s₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory CategoryTheory.inv Hom.h₀ instIsIsoH₀Hom f	—	instIsIsoH₀Hom Hom.w₀
inv_hom_h₀_comp_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.s₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory CategoryTheory.inv Hom.h₀ instIsIsoH₀Hom f	—	instIsIsoH₀Hom CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_h₀_comp_f
inv_hom_s₀_apply 📖	mathematical	—	Hom.s₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id
inv_inv_h₀_comp_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.s₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory CategoryTheory.inv Hom.h₀ instIsIsoH₀Inv f	—	instIsIsoH₀Inv Hom.w₀
inv_inv_h₀_comp_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.s₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory CategoryTheory.inv Hom.h₀ instIsIsoH₀Inv f	—	instIsIsoH₀Inv CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_inv_h₀_comp_f
isoMk_hom_h₀ 📖	mathematical	—	Hom.h₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory isoMk X DFunLike.coe Equiv I₀ EquivLike.toFunLike Equiv.instEquivLike	—	—
isoMk_hom_s₀ 📖	mathematical	—	Hom.s₀ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory isoMk DFunLike.coe Equiv I₀ EquivLike.toFunLike Equiv.instEquivLike	—	—
isoMk_inv_h₀ 📖	mathematical	—	Hom.h₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory isoMk CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X DFunLike.coe Equiv I₀ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.eqToHom	—	—
isoMk_inv_s₀ 📖	mathematical	—	Hom.s₀ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory isoMk DFunLike.coe Equiv I₀ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	—
map_I₀ 📖	mathematical	—	I₀ CategoryTheory.Functor.obj map	—	—
map_X 📖	mathematical	—	X CategoryTheory.Functor.obj map	—	—
map_f 📖	mathematical	—	f CategoryTheory.Functor.obj map CategoryTheory.Functor.map X	—	—
presieve₀_add 📖	mathematical	—	presieve₀ add CategoryTheory.Presieve SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve CategoryTheory.Presieve.singleton	—	presieve₀_reindex presieve₀_sum presieve₀_singleton
presieve₀_empty 📖	mathematical	—	presieve₀ empty Bot.bot CategoryTheory.Presieve OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
presieve₀_eq_presieve₀_iff 📖	mathematical	—	presieve₀ shrink	—	shrink_eq_shrink_of_presieve₀_eq_presieve₀ presieve₀_shrink
presieve₀_f 📖	mathematical	—	presieve₀ X f	—	—
presieve₀_map 📖	mathematical	—	presieve₀ CategoryTheory.Functor.obj map CategoryTheory.Presieve.map	—	CategoryTheory.Presieve.map_ofArrows
presieve₀_mem_iff_of_iso 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings presieve₀	—	presieve₀_mem_of_iso
presieve₀_mem_of_iso 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings presieve₀	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings presieve₀	—	CategoryTheory.Precoverage.RespectsIso.of_forall_exists_iso instIsIsoH₀Hom inv_hom_h₀_comp_f instIsIsoH₀Inv inv_inv_h₀_comp_f
presieve₀_pullback₁ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	presieve₀ pullback₂ CategoryTheory.Presieve.pullbackArrows CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback I₀ X f	—	le_antisymm CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback CategoryTheory.Presieve.hasPullback
presieve₀_reindex 📖	mathematical	—	presieve₀ reindex	—	presieve₀_restrictIndex_equiv
presieve₀_restrictIndex_equiv 📖	mathematical	—	presieve₀ restrictIndex DFunLike.coe Equiv I₀ EquivLike.toFunLike Equiv.instEquivLike	—	le_antisymm Equiv.surjective
presieve₀_restrictIndex_le 📖	mathematical	—	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve presieve₀ restrictIndex	—	CategoryTheory.Presieve.ofArrows_le_iff
presieve₀_shrink 📖	mathematical	—	presieve₀ shrink	—	CategoryTheory.Presieve.presieve₀_preZeroHypercover
presieve₀_sigmaOfIsColimit 📖	mathematical	—	presieve₀ sigmaOfIsColimit CategoryTheory.Presieve.singleton CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₀ CategoryTheory.discreteCategory CategoryTheory.Discrete.functor X CategoryTheory.Limits.Cofan.IsColimit.desc f	—	CategoryTheory.Presieve.ofArrows_pUnit
presieve₀_singleton 📖	mathematical	—	presieve₀ singleton CategoryTheory.Presieve.singleton	—	CategoryTheory.Presieve.ofArrows_pUnit
presieve₀_sum 📖	mathematical	—	presieve₀ sum CategoryTheory.Presieve SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve	—	presieve₀.eq_1 le_antisymm
pullbackCoverOfLeft_I₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	I₀ CategoryTheory.Limits.pullback pullbackCoverOfLeft	—	—
pullbackCoverOfLeft_X 📖	mathematical	CategoryTheory.Limits.HasPullback X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	X CategoryTheory.Limits.pullback pullbackCoverOfLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	—	—
pullbackCoverOfLeft_f 📖	mathematical	CategoryTheory.Limits.HasPullback X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	f CategoryTheory.Limits.pullback pullbackCoverOfLeft CategoryTheory.Limits.pullback.map X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
pullbackCoverOfRight_I₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	I₀ CategoryTheory.Limits.pullback pullbackCoverOfRight	—	—
pullbackCoverOfRight_X 📖	mathematical	CategoryTheory.Limits.HasPullback X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	X CategoryTheory.Limits.pullback pullbackCoverOfRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	—	—
pullbackCoverOfRight_f 📖	mathematical	CategoryTheory.Limits.HasPullback X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct f	f CategoryTheory.Limits.pullback pullbackCoverOfRight CategoryTheory.Limits.pullback.map X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
pullbackIso_hom_h₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.h₀ pullback₁ pullback₂ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory pullbackIso CategoryTheory.Limits.pullback X f CategoryTheory.Limits.pullbackSymmetry	—	—
pullbackIso_hom_s₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.s₀ pullback₁ pullback₂ CategoryTheory.Iso.hom CategoryTheory.PreZeroHypercover instCategory pullbackIso I₀	—	—
pullbackIso_inv_h₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.h₀ pullback₂ pullback₁ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory pullbackIso CategoryTheory.Limits.pullback X f CategoryTheory.Limits.pullbackSymmetry	—	—
pullbackIso_inv_s₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	Hom.s₀ pullback₂ pullback₁ CategoryTheory.Iso.inv CategoryTheory.PreZeroHypercover instCategory pullbackIso I₀	—	—
pullback₁_I₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	I₀ pullback₁	—	—
pullback₁_X 📖	mathematical	CategoryTheory.Limits.HasPullback X f	X pullback₁ CategoryTheory.Limits.pullback f	—	—
pullback₁_f 📖	mathematical	CategoryTheory.Limits.HasPullback X f	f pullback₁ CategoryTheory.Limits.pullback.fst X	—	—
pullback₂_I₀ 📖	mathematical	CategoryTheory.Limits.HasPullback X f	I₀ pullback₂	—	—
pullback₂_X 📖	mathematical	CategoryTheory.Limits.HasPullback X f	X pullback₂ CategoryTheory.Limits.pullback f	—	—
pullback₂_f 📖	mathematical	CategoryTheory.Limits.HasPullback X f	f pullback₂ CategoryTheory.Limits.pullback.snd X	—	—
reindex_I₀ 📖	mathematical	—	I₀ reindex	—	—
reindex_X 📖	mathematical	—	X reindex DFunLike.coe Equiv I₀ EquivLike.toFunLike Equiv.instEquivLike	—	—
reindex_f 📖	mathematical	—	f reindex DFunLike.coe Equiv I₀ EquivLike.toFunLike Equiv.instEquivLike	—	—
restrictIndexHom_h₀ 📖	mathematical	—	Hom.h₀ restrictIndex restrictIndexHom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
restrictIndexHom_s₀ 📖	mathematical	—	Hom.s₀ restrictIndex restrictIndexHom	—	—
restrictIndex_I₀ 📖	mathematical	—	I₀ restrictIndex	—	—
restrictIndex_X 📖	mathematical	—	X restrictIndex I₀	—	—
restrictIndex_f 📖	mathematical	—	f restrictIndex	—	—
shrink_I₀ 📖	mathematical	—	I₀ shrink Set.Elem Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set.range X f	—	CategoryTheory.Presieve.uncurry_ofArrows
shrink_X 📖	mathematical	—	X shrink Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership CategoryTheory.Presieve.uncurry presieve₀	—	—
shrink_eq_shrink_of_presieve₀_eq_presieve₀ 📖	mathematical	presieve₀	shrink	—	shrink.eq_1
shrink_f 📖	mathematical	—	f shrink Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership CategoryTheory.Presieve.uncurry presieve₀	—	—
sieve₀_eq_of_iso 📖	mathematical	—	sieve₀	—	le_antisymm Hom.sieve₀_le_sieve₀
sieve₀_f 📖	mathematical	—	CategoryTheory.Sieve.arrows sieve₀ X f	—	CategoryTheory.Category.id_comp
sigmaOfIsColimit_I₀ 📖	mathematical	—	I₀ sigmaOfIsColimit	—	—
sigmaOfIsColimit_X 📖	mathematical	—	X sigmaOfIsColimit CategoryTheory.Limits.Cocone.pt CategoryTheory.Discrete I₀ CategoryTheory.discreteCategory CategoryTheory.Discrete.functor	—	—
sigmaOfIsColimit_f 📖	mathematical	—	f sigmaOfIsColimit CategoryTheory.Limits.Cofan.IsColimit.desc I₀ X	—	—
singleton_I₀ 📖	mathematical	—	I₀ singleton	—	—
singleton_X 📖	mathematical	—	X singleton	—	—
singleton_f 📖	mathematical	—	f singleton	—	—
sumInl_h₀ 📖	mathematical	—	Hom.h₀ sum sumInl CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
sumInl_s₀ 📖	mathematical	—	Hom.s₀ sum sumInl I₀	—	—
sumInr_h₀ 📖	mathematical	—	Hom.h₀ sum sumInr CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
sumInr_s₀ 📖	mathematical	—	Hom.s₀ sum sumInr I₀	—	—
sumLift_h₀ 📖	mathematical	—	Hom.h₀ sum sumLift Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X I₀ Hom.s₀	—	—
sumLift_s₀ 📖	mathematical	—	Hom.s₀ sum sumLift I₀	—	—
sum_I₀ 📖	mathematical	—	I₀ sum	—	—
sum_X 📖	mathematical	—	X sum I₀	—	—
sum_X_inl 📖	mathematical	—	X sum I₀	—	—
sum_X_inr 📖	mathematical	—	X sum I₀	—	—
sum_f 📖	mathematical	—	f sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct I₀ X	—	—
sum_f_inl 📖	mathematical	—	f sum I₀	—	—
sum_f_inr 📖	mathematical	—	f sum I₀	—	—

CategoryTheory.PreZeroHypercover.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	2 math math: comp_h₀, comp_s₀
h₀ 📖	CompOp	72 math math: CategoryTheory.PreZeroHypercover.isoMk_hom_h₀, CategoryTheory.PreZeroHypercover.inv_hom_h₀, CategoryTheory.PreOneHypercover.inv_hom_h₀_assoc, CategoryTheory.PreOneHypercover.Hom.ext_iff, CategoryTheory.PreOneHypercover.Homotopy.wl, CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f_assoc, CategoryTheory.PreOneHypercover.Hom.w₁₁, CategoryTheory.PreOneHypercover.cylinderHom_h₁, CategoryTheory.PreOneHypercover.Hom.comp_h₀, AlgebraicGeometry.Scheme.Cover.comp_app, CategoryTheory.PreZeroHypercover.instIsIsoH₀Hom, CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f, CategoryTheory.PreZeroHypercover.interLift_h₀, CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f, CategoryTheory.PreZeroHypercover.restrictIndexHom_h₀, id_h₀, CategoryTheory.PreOneHypercover.Homotopy.wl_assoc, CategoryTheory.Precoverage.ZeroHypercover.id_h₀, CategoryTheory.PreOneHypercover.id_h₀, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₀, w₀, AlgebraicGeometry.QuasiCompactCover.exists_hom, CategoryTheory.PreOneHypercover.hom_inv_h₀, AlgebraicGeometry.Scheme.Cover.Hom.w, ext'_iff, ext_iff, CategoryTheory.PreZeroHypercover.pullbackIso_hom_h₀, CategoryTheory.PreZeroHypercover.inv_hom_h₀_assoc, CategoryTheory.PreZeroHypercover.interSnd_h₀, CategoryTheory.PreOneHypercover.isoMk_hom_h₀, CategoryTheory.PreOneHypercover.inv_hom_h₀, AlgebraicGeometry.Scheme.Cover.id_app, CategoryTheory.PreZeroHypercover.hom_inv_h₀_assoc, CategoryTheory.PreZeroHypercover.instIsIsoH₀Inv, CategoryTheory.PreOneHypercover.Hom.id_h₀, CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f_assoc, AlgebraicGeometry.Scheme.Cover.Hom.sigma_h₀, CategoryTheory.PreOneHypercover.sieve₀_cylinder, CategoryTheory.PreZeroHypercover.comp_h₀, AlgebraicGeometry.Scheme.Cover.toSigma_h₀, CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀, CategoryTheory.PreOneHypercover.instIsIsoH₀Inv, CategoryTheory.PreZeroHypercover.sumInr_h₀, CategoryTheory.PreOneHypercover.instIsIsoH₀Hom, CategoryTheory.PreZeroHypercover.hom_inv_h₀, CategoryTheory.PreZeroHypercover.id_h₀, CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc, w₀_assoc, CategoryTheory.PreZeroHypercover.pullbackIso_inv_h₀, CategoryTheory.PreZeroHypercover.sumLift_h₀, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, CategoryTheory.PreZeroHypercover.sumInl_h₀, CategoryTheory.PreOneHypercover.toPullback_cylinder, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀, comp_h₀, CategoryTheory.PreOneHypercover.Hom.w₁₂, CategoryTheory.PreZeroHypercover.interFst_h₀, CategoryTheory.PreOneHypercover.comp_h₀, CategoryTheory.PreOneHypercover.Homotopy.wr, CategoryTheory.PreOneHypercover.cylinder_p₁, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι_assoc, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.PreZeroHypercover.isoMk_inv_h₀, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι, CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc, CategoryTheory.PreOneHypercover.hom_inv_h₀_assoc, CategoryTheory.PreOneHypercover.Homotopy.wr_assoc, CategoryTheory.Precoverage.ZeroHypercover.comp_h₀, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₀, CategoryTheory.PreOneHypercover.cylinderHom_h₀, CategoryTheory.PreOneHypercover.cylinder_Y, CategoryTheory.PreOneHypercover.isoMk_inv_h₀
id 📖	CompOp	2 math math: id_h₀, id_s₀
s₀ 📖	CompOp	111 math math: CategoryTheory.PreOneHypercover.Hom.comp_s₁, CategoryTheory.PreZeroHypercover.inv_hom_h₀, CategoryTheory.PreOneHypercover.inv_hom_h₀_assoc, CategoryTheory.PreOneHypercover.Hom.ext_iff, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁, CategoryTheory.PreOneHypercover.comp_s₀, CategoryTheory.PreOneHypercover.Homotopy.wl, CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f_assoc, CategoryTheory.PreZeroHypercover.inv_hom_s₀_apply, CategoryTheory.PreOneHypercover.Hom.w₁₁, CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc, CategoryTheory.PreOneHypercover.cylinder_X, CategoryTheory.PreOneHypercover.cylinderHom_h₁, CategoryTheory.PreOneHypercover.Hom.comp_h₀, AlgebraicGeometry.Scheme.Cover.comp_app, CategoryTheory.PreZeroHypercover.instIsIsoH₀Hom, CategoryTheory.PreZeroHypercover.inv_hom_h₀_comp_f, CategoryTheory.PreZeroHypercover.interLift_h₀, CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f, AlgebraicGeometry.Scheme.Cover.comp_idx_apply, CategoryTheory.PreOneHypercover.Homotopy.wl_assoc, CategoryTheory.PreZeroHypercover.restrictIndexHom_s₀, CategoryTheory.PreZeroHypercover.interLift_s₀, w₀, CategoryTheory.PreOneHypercover.instIsIsoH₁Hom, AlgebraicGeometry.QuasiCompactCover.exists_hom, CategoryTheory.PreZeroHypercover.isoMk_hom_s₀, CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₀, CategoryTheory.PreOneHypercover.Hom.comp_s₀, CategoryTheory.PreOneHypercover.hom_inv_h₀, AlgebraicGeometry.Scheme.Cover.Hom.w, ext'_iff, ext_iff, AlgebraicGeometry.Scheme.Cover.id_idx_apply, CategoryTheory.PreZeroHypercover.sumLift_s₀, CategoryTheory.PreOneHypercover.Hom.ext'_iff, CategoryTheory.PreOneHypercover.isoMk_inv_h₁, AlgebraicGeometry.Scheme.Cover.toSigma_s₀, CategoryTheory.PreZeroHypercover.inv_hom_h₀_assoc, CategoryTheory.PreZeroHypercover.interFst_s₀, CategoryTheory.PreOneHypercover.cylinder_I₀, CategoryTheory.Precoverage.ZeroHypercover.id_s₀, CategoryTheory.PreOneHypercover.hom_inv_s₁_apply, CategoryTheory.PreZeroHypercover.pullbackIso_hom_s₀, CategoryTheory.PreZeroHypercover.comp_s₀, CategoryTheory.PreOneHypercover.isoMk_inv_s₁, CategoryTheory.PreOneHypercover.inv_hom_h₀, CategoryTheory.PreOneHypercover.cylinder_f, CategoryTheory.Precoverage.ZeroHypercover.comp_s₀, CategoryTheory.PreOneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.inv_hom_s₁_apply, CategoryTheory.PreOneHypercover.inv_hom_h₁_assoc, CategoryTheory.PreOneHypercover.cylinder_I₁, CategoryTheory.PreOneHypercover.Hom.mapMulticospan_map, CategoryTheory.PreZeroHypercover.hom_inv_h₀_assoc, CategoryTheory.PreOneHypercover.id_s₀, CategoryTheory.PreOneHypercover.hom_inv_h₁, CategoryTheory.PreZeroHypercover.instIsIsoH₀Inv, CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f_assoc, CategoryTheory.PreZeroHypercover.hom_inv_s₀_apply, AlgebraicGeometry.Scheme.Cover.Hom.sigma_h₀, CategoryTheory.PreOneHypercover.sieve₀_cylinder, CategoryTheory.PreZeroHypercover.comp_h₀, CategoryTheory.PreOneHypercover.instIsIsoH₀Inv, CategoryTheory.PreZeroHypercover.sumInl_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.id_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₁, CategoryTheory.PreOneHypercover.instIsIsoH₀Hom, CategoryTheory.PreZeroHypercover.hom_inv_h₀, AlgebraicGeometry.Scheme.Cover.Hom.sigma_s₀, CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc, w₀_assoc, id_s₀, CategoryTheory.PreZeroHypercover.sumLift_h₀, CategoryTheory.PreOneHypercover.instIsIsoH₁Inv, CategoryTheory.PreOneHypercover.isoMk_inv_s₀, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, CategoryTheory.PreOneHypercover.toPullback_cylinder, CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀, comp_h₀, CategoryTheory.PreOneHypercover.Hom.w₁₂, CategoryTheory.PreOneHypercover.comp_h₀, CategoryTheory.PreOneHypercover.Homotopy.wr, CategoryTheory.PreZeroHypercover.sumInr_s₀, CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₀, CategoryTheory.PreOneHypercover.cylinder_p₁, CategoryTheory.PreOneHypercover.isoMk_hom_s₀, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι_assoc, CategoryTheory.PreOneHypercover.cylinder_p₂, CategoryTheory.PreOneHypercover.cylinderHom_s₁, CategoryTheory.PreOneHypercover.Hom.comp_h₁, CategoryTheory.PreOneHypercover.inv_hom_s₀_apply, CategoryTheory.PreZeroHypercover.isoMk_inv_s₀, comp_s₀, CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₀, CategoryTheory.PreOneHypercover.cylinderHom_s₀, CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι, CategoryTheory.PreZeroHypercover.id_s₀, CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc, CategoryTheory.PreOneHypercover.hom_inv_h₀_assoc, CategoryTheory.PreOneHypercover.Homotopy.wr_assoc, CategoryTheory.Precoverage.ZeroHypercover.comp_h₀, CategoryTheory.PreOneHypercover.inv_hom_h₁, CategoryTheory.PreOneHypercover.comp_h₁, CategoryTheory.PreOneHypercover.Hom.id_s₀, CategoryTheory.PreOneHypercover.cylinderHom_h₀, CategoryTheory.PreOneHypercover.hom_inv_s₀_apply, CategoryTheory.PreOneHypercover.cylinder_Y, CategoryTheory.PreOneHypercover.Hom.mapMulticospan_obj, CategoryTheory.PreZeroHypercover.pullbackIso_inv_s₀, CategoryTheory.PreZeroHypercover.interSnd_s₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_h₀ 📖	mathematical	—	h₀ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X s₀ CategoryTheory.PreZeroHypercover.I₀	—	—
comp_s₀ 📖	mathematical	—	s₀ comp CategoryTheory.PreZeroHypercover.I₀	—	—
ext 📖	—	s₀ h₀	—	—	—
ext' 📖	—	s₀ h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.eqToHom	—	—	CategoryTheory.Category.comp_id
ext'_iff 📖	mathematical	—	s₀ h₀ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id ext'
ext_iff 📖	mathematical	—	s₀ h₀	—	ext
id_h₀ 📖	mathematical	—	h₀ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X	—	—
id_s₀ 📖	mathematical	—	s₀ id CategoryTheory.PreZeroHypercover.I₀	—	—
sieve₀_le_sieve₀ 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice CategoryTheory.PreZeroHypercover.sieve₀	—	CategoryTheory.Sieve.generate_le_iff CategoryTheory.Presieve.ofArrows_le_iff w₀ CategoryTheory.Sieve.downward_closed CategoryTheory.Sieve.le_generate
w₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X s₀ h₀ CategoryTheory.PreZeroHypercover.f	—	—
w₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.X s₀ h₀ CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w₀

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
RespectsIso 📖	CompData	1 math math: instRespectsIsoOfIsStableUnderBaseChange
ZeroHypercover 📖	CompData	7 math math: ZeroHypercover.isoMk_hom, ZeroHypercover.id_h₀, ZeroHypercover.id_s₀, ZeroHypercover.isoMk_inv, ZeroHypercover.comp_s₀, mem_iff_exists_zeroHypercover, ZeroHypercover.comp_h₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instRespectsIsoOfIsStableUnderBaseChange 📖	mathematical	—	RespectsIso	—	mem_coverings_of_isPullback CategoryTheory.Presieve.ofArrows_comp_eq_of_surjective CategoryTheory.PreZeroHypercover.hom_inv_s₀_apply CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.PreZeroHypercover.instIsIsoH₀Inv CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.PreZeroHypercover.Hom.w₀
instSmallComap 📖	mathematical	—	Small comap	—	le_rfl instSmallOfSmall CategoryTheory.Presieve.map_ofArrows ZeroHypercover.mem₀
instSmallOfSmall 📖	mathematical	—	ZeroHypercover.Small	—	ZeroHypercover.instSmall Small.zeroHypercoverSmall ZeroHypercover.mem₀
le_of_zeroHypercover 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings CategoryTheory.PreZeroHypercover.presieve₀ ZeroHypercover.toPreZeroHypercover	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	CategoryTheory.Presieve.exists_eq_preZeroHypercover
mem_iff_exists_zeroHypercover 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership coverings ZeroHypercover CategoryTheory.Presieve.ofArrows CategoryTheory.PreZeroHypercover.I₀ ZeroHypercover.toPreZeroHypercover CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Presieve.exists_eq_ofArrows ZeroHypercover.mem₀

CategoryTheory.Precoverage.RespectsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_forall_exists_iso 📖	mathematical	CategoryTheory.Iso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings	—	CategoryTheory.Iso.inv_hom_id_assoc le_antisymm of_iso
of_iso 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.PreZeroHypercover.presieve₀	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.PreZeroHypercover.presieve₀	—	—

CategoryTheory.Precoverage.Small

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings	CategoryTheory.Precoverage.Small CategoryTheory.Precoverage CategoryTheory.Precoverage.instMin	—	inf_le_left CategoryTheory.Precoverage.instSmallOfSmall CategoryTheory.Precoverage.ZeroHypercover.mem₀
zeroHypercoverSmall 📖	mathematical	—	CategoryTheory.Precoverage.ZeroHypercover.Small	—	—

CategoryTheory.Precoverage.ZeroHypercover

Definitions

Name	Category	Theorems
add 📖	CompOp	1 math math: add_toPreZeroHypercover
bind 📖	CompOp	3 math math: AlgebraicGeometry.Scheme.Cover.pushforwardIso_f, bind_toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.pushforwardIso_X
instCategory 📖	CompOp	9 math math: isoMk_hom, id_h₀, AlgebraicGeometry.QuasiCompactCover.exists_hom, AlgebraicGeometry.Scheme.Cover.sigmaFunctor_obj, id_s₀, isoMk_inv, comp_s₀, AlgebraicGeometry.Scheme.Cover.sigmaFunctor_map, comp_h₀
inter 📖	CompOp	1 math math: inter_toPreZeroHypercover
isoMk 📖	CompOp	2 math math: isoMk_hom, isoMk_inv
map 📖	CompOp	1 math math: map_toPreZeroHypercover
pullbackCoverOfLeft 📖	CompOp	1 math math: pullbackCoverOfLeft_toPreZeroHypercover
pullbackCoverOfRight 📖	CompOp	1 math math: pullbackCoverOfRight_toPreZeroHypercover
pullback₁ 📖	CompOp	20 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, pullback₁_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback, AlgebraicGeometry.HasAffineProperty.iff_of_openCover, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, instSmallPullback₁, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc, AlgebraicGeometry.Scheme.Cover.pullbackHom_map, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst
pullback₂ 📖	CompOp	1 math math: pullback₂_toPreZeroHypercover
reindex 📖	CompOp	1 math math: reindex_toPreZeroHypercover
restrictIndexOfSmall 📖	CompOp	1 math math: restrictIndexOfSmall_toPreZeroHypercover
singleton 📖	CompOp	1 math math: singleton_toPreZeroHypercover
sum 📖	CompOp	1 math math: sum_toPreZeroHypercover
toPreZeroHypercover 📖	CompOp	333 math math: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd, AlgebraicGeometry.Scheme.mem_propQCPrecoverage_iff_exists_quasiCompactCover, AlgebraicGeometry.Scheme.coverOfIsIso_I₀, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_I₀, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_X, AlgebraicGeometry.instIsAffineXSchemeCover, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc, AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, pullback₁_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc, AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover, AlgebraicGeometry.instIsLocallyArtinianXScheme, AlgebraicGeometry.QuasiCompactCover.of_finite, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_le_iff, Small.exists_restrictIndex_mem, AlgebraicGeometry.Scheme.AffineCover.cover_I₀, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc, AlgebraicGeometry.Scheme.instQuasiCompactCover, AlgebraicGeometry.Scheme.instQuasiCompactCoverQculift, AlgebraicGeometry.Scheme.Cover.copy_f, AlgebraicGeometry.Scheme.Cover.iUnion_range, AlgebraicGeometry.QuasiCompactCover.instCoverOfIsIso, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst, AlgebraicGeometry.sigmaOpenCover_X, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_I₀, AlgebraicGeometry.Scheme.Cover.copy_X, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X, pullbackCoverOfRight_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_I₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isPullback, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_I₀, AlgebraicGeometry.Scheme.instQuasiCompactCoverForgetQc, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰S, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle, AlgebraicGeometry.Scheme.affineOpenCover_I₀, AlgebraicGeometry.Scheme.Cover.gluedCover_t, AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_I₀, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_I₀, AlgebraicGeometry.Scheme.Cover.gluedCover_U, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected_assoc, AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover_toPreZeroHypercover, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom, CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd, isoMk_hom, AlgebraicGeometry.Scheme.affineOpenCover_idx, AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected, AlgebraicGeometry.Scheme.Cover.mkOfCovers_I₀, AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iff, AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback, AlgebraicGeometry.IsLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small, id_h₀, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_pt, AlgebraicGeometry.Scheme.Pullback.cocycle, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, AlgebraicGeometry.Scheme.GlueData.openCover_f, AlgebraicGeometry.instIsAffineXSchemeAffineCover, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_id, AlgebraicGeometry.Scheme.Hom.cover_X, AlgebraicGeometry.Scheme.directedAffineCover_f, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.gluedCover_V, restrictIndexOfSmall_toPreZeroHypercover, CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback, AlgebraicGeometry.HasAffineProperty.iff_of_openCover, AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_ι, AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc, AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, AlgebraicGeometry.Scheme.Cover.ulift_X, AlgebraicGeometry.QuasiCompactCover.instCoverOfIsAffineOfFiniteI₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_f, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_f, AlgebraicGeometry.QuasiCompactCover.exists_hom, instHasPullbacksPresieve₀OfHasPullbacks, toOneHypercover_toPreOneHypercover, pullback₂_toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst, AlgebraicGeometry.Scheme.isAffine_affineBasisCover, AlgebraicGeometry.Scheme.Cover.trans_id, AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp, AlgebraicGeometry.Scheme.Cover.exists_lift_trans_eq, AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f, CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source, AlgebraicGeometry.Scheme.Pullback.t_snd, CategoryTheory.MorphismProperty.IsLocalAtSource.comp, AlgebraicGeometry.Scheme.directedAffineCover_I₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase_assoc, AlgebraicGeometry.Scheme.Pullback.gluing_J, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered, AlgebraicGeometry.Scheme.Pullback.gluing_f, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc, AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, AlgebraicGeometry.ExistsHomHomCompEqCompAux.h𝒰X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc, AlgebraicGeometry.Scheme.OpenCover.restrict_f, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, AlgebraicGeometry.Scheme.Cover.mkOfCovers_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι, AlgebraicGeometry.Scheme.LocalRepresentability.glueData_openCover_map, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f, AlgebraicGeometry.Scheme.Cover.forgetQc_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans, AlgebraicGeometry.QuasiCompactCover.of_isOpenMap, AlgebraicGeometry.Scheme.AffineCover.cover_f, AlgebraicGeometry.Scheme.Cover.gluedCover_J, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone_ι_app, sum_toPreZeroHypercover, TopCat.isOpenEmbedding_f_zeroHypercover, AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd, AlgebraicGeometry.Scheme.Cover.trans_map, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst, AlgebraicGeometry.Scheme.Cover.toSigma_s₀, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc, AlgebraicGeometry.QuasiCompactCover.inst, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, id_s₀, AlgebraicGeometry.Scheme.GlueData.openCover_X, AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_map, AlgebraicGeometry.Scheme.directedAffineCover_X, AlgebraicGeometry.Scheme.Cover.property_trans, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, AlgebraicGeometry.Scheme.Cover.sigma_X, AlgebraicGeometry.Scheme.Pullback.gluing_U, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst, AlgebraicGeometry.Scheme.Cover.nonempty_of_nonempty, AlgebraicGeometry.Scheme.Hom.cover_f, CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_X, AlgebraicGeometry.Scheme.Cover.ulift_f, AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionTrans, isoMk_inv, AlgebraicGeometry.instSurjectiveDescI₀SchemeF, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap_assoc, comp_s₀, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_I₀, AlgebraicGeometry.Scheme.Cover.ulift_I₀, CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover, AlgebraicGeometry.Scheme.Cover.mem_propQCTopology, AlgebraicGeometry.Scheme.Cover.exists_of_trans_eq_trans, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_X, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_f, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_I₀, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms_assoc, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.Scheme.Cover.pushforwardIso_f, AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_X, AlgebraicGeometry.Scheme.Cover.copy_I₀, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f, bind_toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_X, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, AlgebraicGeometry.Scheme.Cover.gluedCover_f, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, pullbackCoverOfLeft_toPreZeroHypercover, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Cover.Hom.sigma_h₀, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id, AlgebraicGeometry.Scheme.Cover.toSigma_h₀, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc, Small.mem₀, AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.directedAffineCover_trans, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd, AlgebraicGeometry.Scheme.coverOfIsIso_X, AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans, AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, add_toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.prop_trans, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_pt, AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans_app_left, AlgebraicGeometry.Scheme.AffineCover.cover_X, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd, AlgebraicGeometry.Scheme.affineBasisCover_obj, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap_comp, AlgebraicGeometry.sigmaOpenCover_I₀, AlgebraicGeometry.Scheme.Cover.Hom.sigma_s₀, Hom.isSheafFor_iff, AlgebraicGeometry.Scheme.Cover.sigma_I₀, AlgebraicGeometry.Scheme.instEtaleF, AlgebraicGeometry.Scheme.Cover.pushforwardIso_I₀, reindex_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd, AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization_assoc, AlgebraicGeometry.Scheme.Cover.trans_comp, singleton_toPreZeroHypercover, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_I₀, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc, AlgebraicGeometry.Scheme.coverOfIsIso_f, AlgebraicGeometry.Scheme.instWeaklyEtaleF, AlgebraicGeometry.Scheme.Hom.cover_I₀, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd, inter_toPreZeroHypercover, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.instIsLocallyNoetherianXScheme, AlgebraicGeometry.sigmaOpenCover_f, f_glueMorphisms, AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc, AlgebraicGeometry.isLocallyArtinian_iff_openCover, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_I₀, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, AlgebraicGeometry.Scheme.OpenCover.restrict_I₀, mem₀, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_I₀, AlgebraicGeometry.QuasiCompactCover.homCover, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc, AlgebraicGeometry.Scheme.instIsOpenImmersionF, AlgebraicGeometry.Scheme.affineOpenCover_f, AlgebraicGeometry.Scheme.Pullback.t'_fst_snd, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_snd, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, AlgebraicGeometry.Scheme.Cover.presieve₀_sigma, AlgebraicGeometry.Scheme.Cover.pushforwardIso_X, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, CategoryTheory.ObjectProperty.iff_of_zeroHypercover, AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd, AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc, AlgebraicGeometry.Scheme.Cover.add_toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.Scheme.Cover.map_prop, AlgebraicGeometry.Scheme.Cover.LocallyDirected.w, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, AlgebraicGeometry.Scheme.Cover.Over.isOver_map, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd, AlgebraicGeometry.Scheme.Cover.mkOfCovers_f, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, AlgebraicGeometry.Scheme.mem_pretopology_iff, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_I₀, AlgebraicGeometry.Scheme.Pullback.t_snd_assoc, AlgebraicGeometry.Scheme.GlueData.openCover_I₀, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map, f_glueMorphisms_assoc, TopCat.exists_mem_zeroHypercover_range, AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f, AlgebraicGeometry.HasRingHomProperty.iff_of_source_openCover, map_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f, AlgebraicGeometry.Scheme.OpenCover.restrict_X, AlgebraicGeometry.Scheme.Cover.mem_pretopology, AlgebraicGeometry.Scheme.affineOneHypercover_toPreOneHypercover_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst, AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f, AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc, AlgebraicGeometry.Scheme.Cover.gluedCoverT'_fst_fst_assoc, AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionMapI₀FunctorOfLocallyDirected, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirectedHomBase_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj, CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_X, AlgebraicGeometry.Scheme.Pullback.lift_comp_ι, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_natTrans_app, AlgebraicGeometry.Scheme.Cover.pullbackHom_map, AlgebraicGeometry.Scheme.isAffine_affineCover, AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_I₀, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X, comp_h₀, AlgebraicGeometry.Scheme.Cover.sigma_f, weaken_toPreZeroHypercover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_X, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsOpenImmersionMapI₀Functor, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase, AlgebraicGeometry.Scheme.Pullback.diagonalCover_map, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc, AlgebraicGeometry.Scheme.Cover.ι_fromGlued, AlgebraicGeometry.Scheme.Hom.presieve₀_cover, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst, AlgebraicGeometry.Scheme.isAffine_affineOpenCover
weaken 📖	CompOp	1 math math: weaken_toPreZeroHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_toPreZeroHypercover 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve CategoryTheory.PreZeroHypercover.presieve₀ toPreZeroHypercover CategoryTheory.Presieve.singleton	toPreZeroHypercover add CategoryTheory.PreZeroHypercover.add	—	—
bind_toPreZeroHypercover 📖	mathematical	—	toPreZeroHypercover bind CategoryTheory.PreZeroHypercover.bind CategoryTheory.PreZeroHypercover.X	—	—
comp_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ toPreZeroHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.Precoverage.ZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.Hom.s₀	—	—
comp_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover CategoryTheory.CategoryStruct.comp CategoryTheory.Precoverage.ZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
id_h₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.h₀ toPreZeroHypercover CategoryTheory.CategoryStruct.id CategoryTheory.Precoverage.ZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.PreZeroHypercover.X	—	—
id_s₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.Hom.s₀ toPreZeroHypercover CategoryTheory.CategoryStruct.id CategoryTheory.Precoverage.ZeroHypercover CategoryTheory.Category.toCategoryStruct instCategory	—	—
instHasPullbackFOfHasPullbacksPresieve₀ 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Presieve.hasPullback
instHasPullbackFOfHasPullbacksPresieve₀_1 📖	mathematical	—	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Limits.hasPullback_symmetry instHasPullbackFOfHasPullbacksPresieve₀
instHasPullbacksPresieve₀OfHasPullbacks 📖	mathematical	—	CategoryTheory.Presieve.HasPullbacks CategoryTheory.PreZeroHypercover.presieve₀ toPreZeroHypercover	—	CategoryTheory.Precoverage.hasPullbacks_of_mem mem₀
instSmall 📖	mathematical	—	Small	—	CategoryTheory.Presieve.exists_eq_ofArrows CategoryTheory.Category.id_comp le_antisymm CategoryTheory.Presieve.ofArrows.mk' mem₀
instSmallOfSmallI₀ 📖	mathematical	—	Small	—	CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_equiv mem₀
instSmallPullback₁ 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f	Small pullback₁	—	mem₀
inter_toPreZeroHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f	toPreZeroHypercover inter CategoryTheory.PreZeroHypercover.inter	—	—
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Precoverage.ZeroHypercover instCategory isoMk CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.instCategory toPreZeroHypercover	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Precoverage.ZeroHypercover instCategory isoMk CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.instCategory toPreZeroHypercover	—	—
map_toPreZeroHypercover 📖	mathematical	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder CategoryTheory.Precoverage.comap	toPreZeroHypercover CategoryTheory.Functor.obj map CategoryTheory.PreZeroHypercover.map	—	—
mem₀ 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.PreZeroHypercover.presieve₀ toPreZeroHypercover	—	—
presieve₀_mem_of_iso 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.PreZeroHypercover.presieve₀	—	CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso mem₀
pullbackCoverOfLeft_toPreZeroHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.fst	toPreZeroHypercover CategoryTheory.Limits.pullback pullbackCoverOfLeft CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft	—	—
pullbackCoverOfRight_toPreZeroHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.Limits.pullback CategoryTheory.PreZeroHypercover.f CategoryTheory.Limits.pullback.snd	toPreZeroHypercover CategoryTheory.Limits.pullback pullbackCoverOfRight CategoryTheory.PreZeroHypercover.pullbackCoverOfRight	—	—
pullback₁_toPreZeroHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f	toPreZeroHypercover pullback₁ CategoryTheory.PreZeroHypercover.pullback₁	—	—
pullback₂_toPreZeroHypercover 📖	mathematical	CategoryTheory.Limits.HasPullback CategoryTheory.PreZeroHypercover.X toPreZeroHypercover CategoryTheory.PreZeroHypercover.f	toPreZeroHypercover pullback₂ CategoryTheory.PreZeroHypercover.pullback₂	—	—
reindex_toPreZeroHypercover 📖	mathematical	—	toPreZeroHypercover reindex CategoryTheory.PreZeroHypercover.reindex	—	—
restrictIndexOfSmall_toPreZeroHypercover 📖	mathematical	—	toPreZeroHypercover restrictIndexOfSmall CategoryTheory.PreZeroHypercover.restrictIndex Small.Index Small.restrictFun	—	—
singleton_toPreZeroHypercover 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.Presieve.singleton	toPreZeroHypercover singleton CategoryTheory.PreZeroHypercover.singleton	—	—
sum_toPreZeroHypercover 📖	mathematical	—	toPreZeroHypercover sum CategoryTheory.PreZeroHypercover.sum	—	—
weaken_toPreZeroHypercover 📖	mathematical	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder	toPreZeroHypercover weaken	—	—

CategoryTheory.Precoverage.ZeroHypercover.Small

Definitions

Name	Category	Theorems
restrictFun 📖	CompOp	2 math math: CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover, mem₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_restrictIndex_mem 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.PreZeroHypercover.presieve₀ CategoryTheory.PreZeroHypercover.restrictIndex CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover	—	—
mem₀ 📖	mathematical	—	CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings CategoryTheory.PreZeroHypercover.presieve₀ CategoryTheory.PreZeroHypercover.restrictIndex CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover Index restrictFun	—	exists_restrictIndex_mem

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
preZeroHypercover 📖	CompOp	4 math math: preZeroHypercover_I₀, preZeroHypercover_X, preZeroHypercover_f, presieve₀_preZeroHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_preZeroHypercover 📖	mathematical	—	CategoryTheory.PreZeroHypercover CategoryTheory.PreZeroHypercover.presieve₀	—	presieve₀_preZeroHypercover
preZeroHypercover_I₀ 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ preZeroHypercover Set.Elem Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct uncurry	—	—
preZeroHypercover_X 📖	mathematical	—	CategoryTheory.PreZeroHypercover.X preZeroHypercover Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership uncurry	—	—
preZeroHypercover_f 📖	mathematical	—	CategoryTheory.PreZeroHypercover.f preZeroHypercover Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership uncurry	—	—
presieve₀_preZeroHypercover 📖	mathematical	—	CategoryTheory.PreZeroHypercover.presieve₀ preZeroHypercover	—	le_antisymm

---

← Back to Index