Sieves

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

Statistics

Metric	Count
Definitions Presieve, BindStruct, Y, f, g, FunctorPushforwardStructure, premap, preobj, HasPairwisePullbacks, HasPullbacks, bind, bindStruct, bindOfArrows, category, categoryMk, cocone, diagram, functorPullback, functorPushforward, getFunctorPushforwardStructure, hasPullbacks, instInhabited, map, ofArrows, idx, pullbackArrows, singleton, singleton', uncurry, Sieve, BindStruct, arrows, bind, essSurjFullFunctorGaloisInsertion, fullyFaithfulFunctorGaloisCoinsertion, functor, functorInclusion, functorPullback, functorPushforward, galoisCoinsertionOfMono, galoisInsertionOfIsSplitEpi, generate, giGenerate, inf, instCoeFunPresieve, instCompleteLattice, inter, natTransOfLe, ofArrows, h, i, ofObjects, ofTwoArrows, pullback, pushforward, sieveInhabited, sieveOfSubfunctor, sieveOfUliftSubfunctor, sup, toFunctor, toUliftFunctor, uliftFunctor, uliftFunctorInclusion, uliftNatTransOfLe, union, instCompleteLatticePresieve	66
Theorems bind, fac, fac_assoc, hf, hg, cover, fac, has_pullbacks, hasPullback, bindOfArrows_ofArrows, bind_comp, bind_ofArrows_le_bindOfArrows, exists_eq_ofArrows, functorPullback_id, functorPullback_mem, functorPushforward_comp, functorPushforward_overForget, hasPullback, image_mem_functorPushforward, instHasPairwisePullbacksOfHasPullbacks, instHasPullbackOfHasPairwisePullbacksOfArrows, instHasPullbacksOfArrowsOfHasPullback, instHasPullbacksOfHasPullbacks, instHasPullbacksSingletonOfHasPullback, map_functorPullback, map_id, map_map, map_monotone, map_ofArrows, map_singleton, eq_eqToHom_comp_hom_idx, hom_idx, mk', obj_idx, ofArrows_bind, ofArrows_category, ofArrows_comp_eq_of_surjective, ofArrows_comp_le, ofArrows_eq_ofArrows_uncurry, ofArrows_le_iff, ofArrows_of_unique, ofArrows_pUnit, ofArrows_pullback, ofArrows_surj, pullback_singleton, singleton_eq_iff_domain, singleton_self, uncurry_bind, uncurry_ofArrows, uncurry_pullbackArrows, uncurry_singleton, arrows_eq_top_iff, arrows_ext, arrows_generate_map_eq_functorPushforward, arrows_top, bind_apply, comp_mem_iff, downward_closed, exists_eq_ofArrows, ext, ext_iff, functorInclusion_app, functorInclusion_is_mono, functorInclusion_top_isIso, functorPullback_apply, functorPullback_arrows, functorPullback_bot, functorPullback_comp, functorPullback_id, functorPullback_inter, functorPullback_monotone, functorPullback_pullback, functorPullback_pushforward_le, functorPullback_top, functorPullback_union, functorPushforward_apply, functorPushforward_bot, functorPushforward_comp, functorPushforward_equivalence_eq_pullback, functorPushforward_extend_eq, functorPushforward_functor, functorPushforward_id, functorPushforward_inverse, functorPushforward_le_iff_le_functorPullback, functorPushforward_monotone, functorPushforward_ofObjects_le, functorPushforward_pullback_le, functorPushforward_top, functorPushforward_union, functor_galoisConnection, functor_map_coe, functor_obj, galoisConnection, generate_apply, generate_bot, generate_functorPullback_le, generate_le_iff, generate_map_eq_functorPushforward, generate_mono, generate_of_contains_isSplitEpi, generate_of_singleton_isSplitEpi, generate_sieve, generate_top, id_mem_iff_eq_top, image_mem_functorPushforward, inter_apply, le_functorPushforward_pullback, le_generate, le_pullback_bind, le_pushforward_pullback, mem_functorPushforward_functor, mem_functorPushforward_iff_of_full, mem_functorPushforward_iff_of_full_of_faithful, mem_functorPushforward_inverse, mem_iff_pullback_eq_top, mem_ofArrows_iff, mem_ofObjects_iff, natTransOfLe_app_coe, natTransOfLe_comm, exists, fac, fac_assoc, ofArrows_category, ofArrows_category', ofArrows_eq_ofObjects, ofArrows_eq_pullback_of_isPullback, ofArrows_le_ofObjects, ofArrows_mk, ofObjects_mono, pullbackArrows_comm, pullback_apply, pullback_comp, pullback_eq_top_of_mem, pullback_functorPushforward_equivalence_eq, pullback_id, pullback_inter, pullback_monotone, pullback_ofArrows_of_iso, pullback_ofObjects, pullback_ofObjects_eq_top, pullback_pushforward_le, pullback_top, pushforward_apply, pushforward_apply_comp, pushforward_comp, pushforward_le_bind_of_mem, pushforward_monotone, pushforward_union, sInf_apply, sSup_apply, sieveOfSubfunctor_apply, sieveOfSubfunctor_functorInclusion, sieveOfUliftSubfunctor_apply, sieveOfUliftSubfunctor_uliftFunctorInclusion, toFunctor_app_coe, toUliftFunctor_app_down_coe, top_apply, uliftFunctorInclusion_app, uliftFunctorInclusion_is_mono, uliftFunctorInclusion_top_isIso, uliftNatTransOfLe_app_down_coe, uliftNatTransOfLe_comm, union_apply, top_apply	164
Total	230

CategoryTheory

Definitions

Name	Category	Theorems
Presieve 📖	CompOp	68 math math: GrothendieckTopology.mem_toPretopology, Sieve.generate_mono, Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, Types.mem_jointlySurjectivePrecoverage_iff, MorphismProperty.ofArrows_mem_precoverage, AlgebraicGeometry.Scheme.bot_mem_precoverage, Presieve.map_functorPullback, Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff, Sieve.generate_bot, Precoverage.preZeroHypercoverFamily_property, Sieve.generate_top, Pretopology.mem_toGrothendieck, PreZeroHypercover.presieve₀_mem_iff_of_iso, Presieve.isSheafFor_top_sieve, Precoverage.mem_coverings_of_isIso, Presieve.ofArrows_le_iff, Precoverage.mem_finite_iff, Sieve.le_generate, top_apply, Sieve.arrows_eq_top_iff, Sieve.arrows_top, Presieve.ofArrows_comp_le, MorphismProperty.bot_mem_precoverage, PreZeroHypercover.presieve₀_restrictIndex_le, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_surjective, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff, Precoverage.HasIsos.mem_coverings_of_isIso, Types.singleton_mem_jointlySurjectivePrecoverage_iff, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Precoverage.mem_iff_exists_zeroHypercover, Precoverage.ZeroHypercover.presieve₀_mem_of_iso, ofGrothendieck_iff, Presieve.le_of_factorsThru_sieve, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, Precoverage.ofArrows_mem_finite, Pretopology.has_isos, Precoverage.ZeroHypercover.Small.mem₀, PreZeroHypercoverFamily.mem_precoverage_iff, Pretopology.mem_inf, GrothendieckTopology.mem_toPrecoverage_iff, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, Presieve.mem_comap_jointlySurjectivePrecoverage_iff, Pretopology.ofArrows_mem_finite, Pretopology.mem_sInf, PreZeroHypercover.presieve₀_sum, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, Precoverage.ZeroHypercover.mem₀, Presieve.isSeparatedFor_top, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, Pretopology.mem_toCoverage, Coverage.sup_covering, AlgebraicGeometry.Scheme.mem_pretopology_iff, Presieve.factorsThru_top, Sieve.generate_le_iff, AlgebraicGeometry.Scheme.Cover.mem_pretopology, PreZeroHypercover.presieve₀_mem_precoverage_iff, Pretopology.mem_ofGrothendieck, Pretopology.le_def, Presieve.isSheafFor_top, GrothendieckTopology.mem_toCoverage_iff, PreZeroHypercover.presieve₀_add, AlgebraicGeometry.Scheme.pretopology_cover, Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, Precoverage.mem_comap_iff
Sieve 📖	CompData	164 math math: AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, GrothendieckTopology.mem_toPretopology, GrothendieckTopology.ext_iff, Sieve.generate_mono, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, Sieve.overEquiv_pullback, Sieve.mem_iff_pullback_eq_top, Sieve.generate_functorPullback_le, GrothendieckTopology.OneHypercover.mem₀, Presheaf.imageSieve_app, Functor.OneHypercoverDenseData.mem₁, Sieve.functorPushforward_ofObjects_le, Functor.functorPushforward_imageSieve_mem, Sieve.pullback_monotone, Functor.closedSieves_obj, extensiveTopology.mem_sieves_iff_contains_colimit_cofan, GrothendieckTopology.monotone_close, Functor.functorPushforward_mem_iff, GrothendieckTopology.trivial_covering, GrothendieckTopology.arrow_intersect, GrothendieckTopology.intersection_covering_iff, AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, Sieve.top_apply, Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp, Sieve.overEquiv_le_overEquiv_iff, Sieve.functorPullback_bot, Sieve.pullback_pushforward_le, Sieve.generate_bot, Sieve.sSup_apply, Sieve.generate_top, GrothendieckTopology.OneHypercover.mem_sieve₁', Sieve.equalizer_self, Pretopology.mem_toGrothendieck, GrothendieckTopology.Cover.preOneHypercover_sieve₀, Coverage.mem_toGrothendieck_sieves_of_superset, GrothendieckTopology.top_mem, Functor.IsLocallyFull.functorPushforward_imageSieve_mem, Sieve.overEquiv_symm_iff, GrothendieckTopology.closureOperator_isClosed, Sieve.functorPushforward_over_map, Presheaf.equalizerSieve_self_eq_top, Functor.OneHypercoverDenseData.mem₁₀, Functor.is_cover_of_isCoverDense, GrothendieckTopology.mem_over_iff, regularTopology.mem_sieves_iff_hasEffectiveEpi, GrothendieckTopology.coversTop_iff_of_isTerminal, Functor.functorPushforward_equalizer_mem, GrothendieckTopology.Cover.preOneHypercover_sieve₁, Functor.IsDenseSubsite.equalizer_mem, Sieve.overEquiv_top, GrothendieckTopology.close_eq_top_iff_mem, Sieve.arrows_eq_top_iff, GrothendieckTopology.coe_copy, Sieve.arrows_top, Sieve.functorPullback_inter, Sieve.le_pullback_bind, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, Sieve.generate_of_singleton_isSplitEpi, Sieve.functorPullback_top, GrothendieckTopology.le_def, Sieve.overEquiv_symm_pullback, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, GrothendieckTopology.Cover.Arrow.hf, Precoverage.mem_toGrothendieck_iff, GrothendieckTopology.mem_sInf, GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁, generate_discretePresieve_mem, Sieve.le_pushforward_pullback, Sieve.functorPushforward_monotone, Pseudofunctor.isPrestackFor_iff_isSheafFor, coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, Precoverage.generate_mem_toGrothendieck, Functor.LocallyCoverDense.functorPushforward_functorPullback_mem, Functor.pushforward_cover_iff_cover_pullback, Functor.IsDenseSubsite.functorPushforward_mem_iff, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Presheaf.IsLocallyInjective.equalizerSieve_mem, Sieve.functorPullback_monotone, GrothendieckTopology.Cover.condition, Sieve.pullback_eq_top_of_mem, Functor.inducedTopology_sieves, ofGrothendieck_iff, GrothendieckTopology.dense_covering, Sieve.pullback_inter, GrothendieckTopology.OneHypercover.IsPreservedBy.mem₀, Functor.OneHypercoverDenseData.sieve_mem, Functor.OneHypercoverDenseData.mem₀, Functor.IsLocallyFaithful.functorPushforward_equalizer_mem, Sieve.ofObjects_mono, Sieve.functorPushforward_pullback_le, Sieve.overEquiv_symm_generate, GrothendieckTopology.bot_covering, GrothendieckTopology.mem_sieves_iff_coe, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, Presheaf.IsLocallySurjective.imageSieve_mem, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, Coverage.mem_toGrothendieck, Presheaf.equalizerSieve_mem, coherentTopology.mem_sieves_of_hasEffectiveEpiFamily, GrothendieckTopology.Cover.ext_iff, Sieve.functorPushforward_union, GrothendieckTopology.mem_toPrecoverage_iff, Sieve.le_functorPushforward_pullback, Sieve.functorPushforward_bot, Sieve.sInf_apply, GrothendieckTopology.le_close, Sieve.galoisConnection, Presieve.bind_ofArrows_le_bindOfArrows, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, Sieve.functor_galoisConnection, Sieve.pushforward_union, GrothendieckTopology.pullback_mem_iff_of_isIso, Functor.closedSieves_map_coe, Sieve.functorInclusion_top_isIso, GrothendieckTopology.covering_iff_covers_id, Sieve.pushforward_le_bind_of_mem, Sieve.overEquiv_symm_top, sieve₁'_toPreOneHypercover_eq_top, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, Sieve.functorPushforward_top, Sieve.functorPullback_pushforward_le, Sieve.functorPushforward_le_iff_le_functorPullback, Functor.IsCoverDense.is_cover, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, regularTopology.mem_sieves_of_hasEffectiveEpi, Sieve.union_apply, GrothendieckTopology.Cover.Arrow.to_middle_condition, GrothendieckTopology.top_mem', regularTopology.exists_effectiveEpi_iff_mem_induced, Presheaf.equalizerSieve_eq_top_iff, Sieve.inter_apply, AlgebraicGeometry.Scheme.grothendieckTopology_cover, Sieve.overEquiv_generate, Functor.imageSieve_map, Sieve.pullback_top, Sieve.uliftFunctorInclusion_top_isIso, Sieve.id_mem_iff_eq_top, coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, GrothendieckTopology.covers_iff, Sieve.pullback_ofObjects_eq_top, Sieve.pushforward_monotone, Sieve.generate_le_iff, Pseudofunctor.isPrestackFor_iff_isSheafFor', Functor.IsCoverDense.functorPullback_pushforward_covering, GrothendieckTopology.Cover.Arrow.from_middle_condition, Functor.mem_inducedTopology_sieves_iff, Pretopology.mem_ofGrothendieck, PreOneHypercover.sieve₀_trivial, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, GrothendieckTopology.mem_toCoverage_iff, PreOneHypercover.sieve₁_trivial, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, Functor.IsDenseSubsite.imageSieve_mem, Presheaf.imageSieve_mem, GrothendieckTopology.Cover.coe_pullback, discreteSieve_mem, Sieve.generate_of_contains_isSplitEpi, Sieve.overEquiv_iff, Sieve.ofArrows_le_ofObjects, GrothendieckTopology.OneHypercover.mem₁, PreZeroHypercover.Hom.sieve₀_le_sieve₀, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, Sieve.functorPullback_union, GrothendieckTopology.top_covering
instCompleteLatticePresieve 📖	CompOp	30 math math: Sieve.generate_mono, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, AlgebraicGeometry.Scheme.bot_mem_precoverage, Presieve.map_functorPullback, Sieve.generate_bot, Sieve.generate_top, Pretopology.mem_toGrothendieck, Presieve.isSheafFor_top_sieve, Presieve.ofArrows_le_iff, Sieve.le_generate, top_apply, Sieve.arrows_eq_top_iff, Sieve.arrows_top, Presieve.ofArrows_comp_le, MorphismProperty.bot_mem_precoverage, PreZeroHypercover.presieve₀_restrictIndex_le, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Presieve.le_of_factorsThru_sieve, Precoverage.sup_mem_coverings, Precoverage.IsStableUnderSup.sup_mem_coverings, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, PreZeroHypercover.presieve₀_sum, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, Presieve.isSeparatedFor_top, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, Presieve.factorsThru_top, Sieve.generate_le_iff, Presieve.isSheafFor_top, PreZeroHypercover.presieve₀_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
top_apply 📖	mathematical	—	Top.top Presieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLatticePresieve BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
BindStruct 📖	CompData	—
FunctorPushforwardStructure 📖	CompData	—
HasPairwisePullbacks 📖	CompData	4 math math: CategoryTheory.Precoverage.hasPairwisePullbacks_of_mem, instHasPairwisePullbacksOfHasPullbacks, HasPairwisePullbacks.map_of_preservesPairwisePullbacks, CategoryTheory.instHasPairwisePullbacksOfExtensive
HasPullbacks 📖	CompData	6 math math: instHasPullbacksOfArrowsOfHasPullback, CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks, instHasPullbacksOfHasPullbacks, CategoryTheory.Precoverage.hasPullbacks_of_mem, CategoryTheory.Precoverage.HasPullbacks.hasPullbacks_of_mem, instHasPullbacksSingletonOfHasPullback
bind 📖	CompOp	6 math math: uncurry_bind, CategoryTheory.Sieve.bind_apply, CategoryTheory.Pretopology.transitive, bind_comp, BindStruct.bind, ofArrows_bind
bindOfArrows 📖	CompData	4 math math: CategoryTheory.PreOneHypercover.sieve₀_cylinder, bind_ofArrows_le_bindOfArrows, CategoryTheory.GrothendieckTopology.bindOfArrows, bindOfArrows_ofArrows
category 📖	CompOp	22 math math: CategoryTheory.Sieve.ofArrows_category', CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, CategoryTheory.Sieve.ofArrows_category, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, ofArrows_category, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Pseudofunctor.isStackFor_iff, CategoryTheory.Presheaf.isSheaf_iff_isLimit, CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
categoryMk 📖	CompOp	1 math math: CategoryTheory.regularTopology.parallelPair_pullback_initial
cocone 📖	CompOp	11 math math: CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Presheaf.isSheaf_iff_isLimit, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
diagram 📖	CompOp	12 math math: CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Presheaf.isSheaf_iff_isLimit, CategoryTheory.Sieve.yonedaFamily_fromCocone_compatible, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
functorPullback 📖	CompOp	9 math math: functorPullback_mem, CategoryTheory.Sieve.generate_functorPullback_le, map_functorPullback, CategoryTheory.Sieve.functorPullback_arrows, functorPullback_id, CategoryTheory.Sieve.overEquiv_symm_generate, FamilyOfElements.Compatible.functorPullback, map_functorPullback_overForget, CategoryTheory.Sieve.functorPullback_apply
functorPushforward 📖	CompOp	10 math math: CategoryTheory.Sieve.mem_functorPushforward_iff_of_full, CategoryTheory.Sieve.functorPushforward_apply, CategoryTheory.Sieve.functorPushforward_extend_eq, FamilyOfElements.Compatible.functorPushforward, functorPushforward_overForget, CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward, image_mem_functorPushforward, CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful, CategoryTheory.Sieve.overEquiv_generate, functorPushforward_comp
getFunctorPushforwardStructure 📖	CompOp	—
hasPullbacks 📖	MathDef	—
instInhabited 📖	CompOp	—
map 📖	CompData	14 math math: map_functorPullback, HasPairwisePullbacks.map_of_preservesPairwisePullbacks, CategoryTheory.PreZeroHypercover.presieve₀_map, map_map, IsSheafFor.comp_iff_of_preservesPairwisePullbacks, map_ofArrows, functorPushforward_overForget, map_monotone, CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward, map_functorPullback_overForget, map_id, CategoryTheory.Sieve.generate_map_eq_functorPushforward, map_singleton, CategoryTheory.Precoverage.mem_comap_iff
ofArrows 📖	CompData	52 math math: instHasPullbacksOfArrowsOfHasPullback, exists_eq_ofArrows, ofArrows_comp_eq_of_surjective, ofArrows_eq_ofArrows_uncurry, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, CategoryTheory.MorphismProperty.ofArrows_mem_precoverage, ofArrows_mem_comap_jointlySurjectivePrecoverage_iff, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, ofArrows.mk', ofArrows_le_iff, CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, isSheafFor_arrows_iff, map_ofArrows, regular.single_epi, ofArrows_comp_le, AlgebraicGeometry.Scheme.exists_cover_of_mem_pretopology, ofArrows_category, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, FamilyOfElements.isAmalgamation_iff_ofArrows, isSheafFor_of_preservesProduct, CategoryTheory.Sieve.generateFamily_eq, CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover, CategoryTheory.instExtensiveOfArrowsι, ofArrows_pullback, Arrows.Compatible.familyOfElements_compatible, CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition, isSheafFor_over_map_op_comp_ofArrows_iff, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, CategoryTheory.Precoverage.ofArrows_mem_finite, CategoryTheory.PreOneHypercover.sieve₀_cylinder, ofArrows_of_unique, uncurry_ofArrows, AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff, CategoryTheory.Pretopology.ofArrows_mem_finite, ofArrows_pUnit, isSheafFor_arrows_iff_pullbacks, CategoryTheory.Sieve.effectiveEpimorphic_family, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, CategoryTheory.isSheaf_coherent, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, CategoryTheory.PreOneHypercover.toPullback_cylinder, Extensive.arrows_nonempty_isColimit, AlgebraicGeometry.Scheme.mem_pretopology_iff, ofArrows_bind, AlgebraicGeometry.Scheme.Cover.mem_pretopology, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_eq_ofArrows, AlgebraicGeometry.Scheme.pretopology_cover, CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, isSheafFor_ofArrows_iff_bijective_toCompabible, isSheafFor_ofArrows_comp_iff, bindOfArrows_ofArrows
pullbackArrows 📖	CompData	8 math math: CategoryTheory.PreZeroHypercover.presieve₀_pullback₁, ofArrows_pullback, CategoryTheory.Precoverage.pullbackArrows_mem, pullback_singleton, CategoryTheory.Sieve.pullbackArrows_comm, uncurry_pullbackArrows, FactorsThruAlong.pullbackArrows, CategoryTheory.Pretopology.pullbacks
singleton 📖	CompData	28 math math: isSeparatedFor_singleton, CategoryTheory.Sieve.generateSingleton_eq, FamilyOfElements.compatible_singleton_iff, isSheafFor_singleton, FamilyOfElements.singletonEquiv_symm_apply_self, FamilyOfElements.singletonEquiv_apply, CategoryTheory.Precoverage.mem_coverings_of_isIso, uncurry_singleton, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff, CategoryTheory.Sieve.effectiveEpimorphic_singleton, CategoryTheory.Sieve.generate_of_singleton_isSplitEpi, singleton_self, AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff, CategoryTheory.Precoverage.HasIsos.mem_coverings_of_isIso, CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff, pullback_singleton, FamilyOfElements.isAmalgamation_singleton_iff, CategoryTheory.Pretopology.has_isos, isSheafFor_singleton_iff_of_iso, ofArrows_of_unique, singleton_eq_iff_domain, ofArrows_pUnit, CategoryTheory.PreZeroHypercover.presieve₀_singleton, isSheafFor_singleton_iso, map_singleton, CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback, CategoryTheory.PreZeroHypercover.presieve₀_add, instHasPullbacksSingletonOfHasPullback
singleton' 📖	CompOp	—
uncurry 📖	CompOp	11 math math: ofArrows_eq_ofArrows_uncurry, uncurry_bind, preZeroHypercover_I₀, preZeroHypercover_X, CategoryTheory.Precoverage.mem_finite_iff, uncurry_singleton, preZeroHypercover_f, CategoryTheory.PreZeroHypercover.shrink_X, uncurry_ofArrows, uncurry_pullbackArrows, CategoryTheory.PreZeroHypercover.shrink_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bindOfArrows_ofArrows 📖	mathematical	—	bindOfArrows ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	le_antisymm
bind_comp 📖	mathematical	—	bind CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
bind_ofArrows_le_bindOfArrows 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.Sieve.instCompleteLattice CategoryTheory.Sieve.bind CategoryTheory.Sieve.arrows CategoryTheory.Sieve.ofArrows CategoryTheory.Sieve.pullback CategoryTheory.Sieve.ofArrows.i CategoryTheory.Sieve.ofArrows.h CategoryTheory.Sieve.generate bindOfArrows	—	CategoryTheory.Sieve.ofArrows.fac CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
exists_eq_ofArrows 📖	mathematical	—	ofArrows	—	le_antisymm
functorPullback_id 📖	mathematical	—	functorPullback CategoryTheory.Functor.id	—	—
functorPullback_mem 📖	mathematical	—	functorPullback CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
functorPushforward_comp 📖	mathematical	—	functorPushforward CategoryTheory.Functor.comp CategoryTheory.Functor.obj	—	Set.ext CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc
functorPushforward_overForget 📖	mathematical	—	functorPushforward CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget CategoryTheory.Sieve.arrows CategoryTheory.Functor.obj CategoryTheory.Sieve.generate map	—	le_antisymm
hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	HasPullbacks.hasPullback
image_mem_functorPushforward 📖	mathematical	—	functorPushforward CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp
instHasPairwisePullbacksOfHasPullbacks 📖	mathematical	—	HasPairwisePullbacks	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instHasPullbackOfHasPairwisePullbacksOfArrows 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	HasPairwisePullbacks.has_pullbacks
instHasPullbacksOfArrowsOfHasPullback 📖	mathematical	CategoryTheory.Limits.HasPullback	HasPullbacks ofArrows	—	—
instHasPullbacksOfHasPullbacks 📖	mathematical	—	HasPullbacks	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instHasPullbacksSingletonOfHasPullback 📖	mathematical	—	HasPullbacks singleton	—	—
map_functorPullback 📖	mathematical	—	CategoryTheory.Presieve CategoryTheory.Functor.obj Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve map functorPullback	—	—
map_id 📖	mathematical	—	map CategoryTheory.Functor.id	—	le_antisymm
map_map 📖	mathematical	—	map CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—
map_monotone 📖	mathematical	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve	CategoryTheory.Functor.obj map	—	—
map_ofArrows 📖	mathematical	—	map ofArrows CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	le_antisymm ofArrows_surj CategoryTheory.Category.id_comp map_map
map_singleton 📖	mathematical	—	map singleton CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	ofArrows_pUnit map_ofArrows
ofArrows_bind 📖	mathematical	—	bind ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	Set.ext bind_comp
ofArrows_category 📖	mathematical	—	ofArrows category CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom	—	le_antisymm
ofArrows_comp_eq_of_surjective 📖	mathematical	—	ofArrows	—	le_antisymm ofArrows_comp_le
ofArrows_comp_le 📖	mathematical	—	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve ofArrows	—	—
ofArrows_eq_ofArrows_uncurry 📖	mathematical	—	ofArrows Set.Elem Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct uncurry ofArrows.idx Set Set.instMembership	—	le_antisymm ofArrows.mk' ofArrows.obj_idx ofArrows.hom_idx CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp
ofArrows_le_iff 📖	mathematical	—	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve ofArrows	—	—
ofArrows_of_unique 📖	mathematical	—	ofArrows singleton Unique.instInhabited	—	le_antisymm ofArrows_le_iff Unique.instSubsingleton
ofArrows_pUnit 📖	mathematical	—	ofArrows singleton	—	ofArrows_of_unique
ofArrows_pullback 📖	mathematical	CategoryTheory.Limits.HasPullback	ofArrows CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd pullbackArrows instHasPullbacksOfArrowsOfHasPullback	—	instHasPullbacksOfArrowsOfHasPullback Set.ext hasPullback
ofArrows_surj 📖	mathematical	ofArrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp
pullback_singleton 📖	mathematical	—	pullbackArrows singleton instHasPullbacksSingletonOfHasPullback CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd	—	instHasPullbacksSingletonOfHasPullback Set.ext hasPullback
singleton_eq_iff_domain 📖	mathematical	—	singleton	—	—
singleton_self 📖	mathematical	—	singleton	—	—
uncurry_bind 📖	mathematical	—	uncurry bind Set.iUnion Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instMembership Set.image Sigma.map CategoryTheory.CategoryStruct.comp	—	Set.ext
uncurry_ofArrows 📖	mathematical	—	uncurry ofArrows Set.range Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	Set.ext
uncurry_pullbackArrows 📖	mathematical	—	uncurry pullbackArrows instHasPullbacksOfHasPullbacks Set.image Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd	—	Set.ext instHasPullbacksOfHasPullbacks CategoryTheory.Limits.hasLimitOfHasLimitsOfShape hasPullback
uncurry_singleton 📖	mathematical	—	uncurry singleton Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Set Set.instSingletonSet	—	Set.ext Set.mem_singleton_iff

CategoryTheory.Presieve.BindStruct

Definitions

Name	Category	Theorems
Y 📖	CompOp	4 math math: fac_assoc, hf, fac, hg
f 📖	CompOp	4 math math: fac_assoc, hf, fac, hg
g 📖	CompOp	3 math math: fac_assoc, fac, hg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind 📖	mathematical	—	CategoryTheory.Presieve.bind	—	hf hg fac
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y g f	—	—
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Y g f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
hf 📖	mathematical	—	Y f	—	—
hg 📖	mathematical	—	Y f hf g	—	—

CategoryTheory.Presieve.FunctorPushforwardStructure

Definitions

Name	Category	Theorems
premap 📖	CompOp	2 math math: fac, cover
preobj 📖	CompOp	2 math math: fac, cover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cover 📖	mathematical	—	preobj premap	—	—
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj preobj lift CategoryTheory.Functor.map premap	—	—

CategoryTheory.Presieve.HasPairwisePullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_pullbacks 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	—

CategoryTheory.Presieve.HasPullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPullback 📖	mathematical	—	CategoryTheory.Limits.HasPullback	—	—

CategoryTheory.Presieve.bind

Definitions

Name	Category	Theorems
bindStruct 📖	CompOp	—

CategoryTheory.Presieve.ofArrows

Definitions

Name	Category	Theorems
idx 📖	CompOp	4 math math: CategoryTheory.Presieve.ofArrows_eq_ofArrows_uncurry, eq_eqToHom_comp_hom_idx, hom_idx, obj_idx

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_eqToHom_comp_hom_idx 📖	mathematical	CategoryTheory.Presieve.ofArrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct idx CategoryTheory.eqToHom obj_idx	—	CategoryTheory.Presieve.ofArrows_surj
hom_idx 📖	mathematical	CategoryTheory.Presieve.ofArrows	idx CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom obj_idx	—	obj_idx eq_eqToHom_comp_hom_idx CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp
mk' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom	CategoryTheory.Presieve.ofArrows	—	CategoryTheory.Category.id_comp
obj_idx 📖	mathematical	CategoryTheory.Presieve.ofArrows	idx	—	CategoryTheory.Presieve.ofArrows_surj

CategoryTheory.Sieve

Definitions

Name	Category	Theorems
BindStruct 📖	CompOp	—
arrows 📖	CompOp	134 math math: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, CategoryTheory.Presieve.isSheafFor_pullback_iff, pullback_apply, CategoryTheory.Pseudofunctor.isPrestackFor', mem_functorPushforward_iff_of_full, CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition, functor_obj, CategoryTheory.Functor.OneHypercoverDenseData.sieve_apply, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, pushforward_apply, mem_iff_pullback_eq_top, CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, functorPushforward_apply, CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan, CategoryTheory.Presieve.isAmalgamation_sieveExtend, AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, top_apply, functorPullback_arrows, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, ofArrows_mk, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, bind_apply, mem_ofObjects_iff, equalizer_apply, ext_iff, ofArrows_category, sSup_apply, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, CategoryTheory.Equalizer.Sieve.w, CategoryTheory.Pretopology.mem_toGrothendieck, CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, comp_mem_iff, overEquiv_symm_iff, functorPushforward_extend_eq, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff, le_generate, CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi, CategoryTheory.Presheaf.IsSheaf.isSheafFor, CategoryTheory.GrothendieckTopology.bot_covers, CategoryTheory.GrothendieckTopology.close_apply, CategoryTheory.Presheaf.isSeparated_iff_subsingleton, CategoryTheory.discreteSieve_apply, arrows_eq_top_iff, arrows_top, generate_sieve, CategoryTheory.Pseudofunctor.IsStackFor_generate_iff, sieveOfUliftSubfunctor_apply, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Presieve.functorPushforward_overForget, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, CategoryTheory.Presheaf.imageSieve_apply, CategoryTheory.regularTopology.parallelPair_pullback_initial, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor, functorInclusion_app, CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, CategoryTheory.Presheaf.isSheaf_iff_isLimit, CategoryTheory.Presieve.isSheafFor_iff_generate, uliftNatTransOfLe_app_down_coe, CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, sieveOfSubfunctor_apply, TopCat.Presheaf.generateEquivalenceOpensLe_functor, uliftFunctorInclusion_app, mem_functorPushforward_inverse, CategoryTheory.GrothendieckTopology.dense_covering, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, yonedaFamily_fromCocone_compatible, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff, CategoryTheory.GrothendieckTopology.bind_covering, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, arrows_generate_map_eq_functorPushforward, AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff, CategoryTheory.PreOneHypercover.sieve₀_cylinder, CategoryTheory.GrothendieckTopology.Cover.ext_iff, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe, mem_functorPushforward_functor, sInf_apply, CategoryTheory.Pseudofunctor.IsPrestackFor_generate_iff, CategoryTheory.Presieve.restrict_extend, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, forallYonedaIsSheaf_iff_colimit, CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage, CategoryTheory.PreOneHypercover.sieve₁_apply, CategoryTheory.Pseudofunctor.isStackFor', natTransOfLe_app_coe, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology, CategoryTheory.Subfunctor.Subpresheaf.family_of_elements_compatible, CategoryTheory.Equalizer.Sieve.compatible_iff, CategoryTheory.presheafHom_isSheafFor, functor_map_coe, CategoryTheory.Presheaf.equalizerSieve_apply, CategoryTheory.GrothendieckTopology.covers_iff_mem_of_isClosed, CategoryTheory.Presieve.compatible_iff_sieveCompatible, CategoryTheory.PreZeroHypercover.sieve₀_f, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, union_apply, mem_functorPushforward_iff_of_full_of_faithful, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, CategoryTheory.GrothendieckTopology.Cover.Arrow.to_middle_condition, CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced, CategoryTheory.Presieve.extension_iff_amalgamation, inter_apply, CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend, mem_ofArrows_iff, CategoryTheory.Presheaf.isLimit_iff_isSheafFor, CategoryTheory.PreOneHypercover.sieve₁_inter, CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible, CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀_apply, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, id_mem_iff_eq_top, functorPullback_apply, CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, generate_le_iff, CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor', CategoryTheory.Equalizer.Sieve.SecondObj.ext_iff, CategoryTheory.GrothendieckTopology.Cover.Arrow.from_middle_condition, CategoryTheory.Subfunctor.family_of_elements_compatible, generate_apply, CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, CategoryTheory.Subfunctor.sieveOfSection_apply, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, CategoryTheory.Presieve.isSeparatedFor_iff_generate, CategoryTheory.GrothendieckTopology.Cover.coe_pullback, overEquiv_iff, TopCat.Presheaf.generateEquivalenceOpensLe_inverse, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
bind 📖	CompOp	8 math math: bind_apply, le_pullback_bind, CategoryTheory.GrothendieckTopology.bind_covering, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, pushforward_le_bind_of_mem, CategoryTheory.Presieve.isSheafFor_bind, CategoryTheory.Sheaf.isSheafFor_bind, CategoryTheory.PreOneHypercover.sieve₁_inter
essSurjFullFunctorGaloisInsertion 📖	CompOp	—
fullyFaithfulFunctorGaloisCoinsertion 📖	CompOp	—
functor 📖	CompOp	14 math math: functor_obj, sieveOfSubfunctor_functorInclusion, natTransOfLe_comm, functorInclusion_app, uliftNatTransOfLe_app_down_coe, CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend, functorInclusion_top_isIso, natTransOfLe_app_coe, CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend_assoc, functorInclusion_is_mono, functor_map_coe, CategoryTheory.Presieve.extension_iff_amalgamation, toFunctor_app_coe, toUliftFunctor_app_down_coe
functorInclusion 📖	CompOp	8 math math: sieveOfSubfunctor_functorInclusion, natTransOfLe_comm, functorInclusion_app, CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend, functorInclusion_top_isIso, CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend_assoc, functorInclusion_is_mono, CategoryTheory.Presieve.extension_iff_amalgamation
functorPullback 📖	CompOp	22 math math: generate_functorPullback_le, functorPullback_arrows, functorPullback_id, functorPullback_comp, functorPullback_bot, functorPullback_inter, functorPullback_top, functorPushforward_inverse, CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_mem, CategoryTheory.Functor.pushforward_cover_iff_cover_pullback, functorPullback_monotone, functorPullback_pullback, le_functorPushforward_pullback, functorPushforward_functor, functor_galoisConnection, functorPullback_pushforward_le, functorPushforward_le_iff_le_functorPullback, functorPullback_apply, CategoryTheory.Functor.cover_lift, CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering, CategoryTheory.Functor.IsCocontinuous.cover_lift, functorPullback_union
functorPushforward 📖	CompOp	35 math math: functorPushforward_ofObjects_le, CategoryTheory.Functor.functorPushforward_imageSieve_mem, functorPushforward_apply, CategoryTheory.Functor.functorPushforward_mem_iff, pullback_functorPushforward_equivalence_eq, functorPushforward_id, CategoryTheory.Functor.IsLocallyFull.functorPushforward_imageSieve_mem, functorPushforward_over_map, CategoryTheory.Functor.functorPushforward_equalizer_mem, functorPushforward_inverse, functorPushforward_monotone, functorPushforward_comp, CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_mem, CategoryTheory.Functor.pushforward_cover_iff_cover_pullback, CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff, mem_functorPushforward_inverse, CategoryTheory.Functor.inducedTopology_sieves, CategoryTheory.Functor.IsLocallyFaithful.functorPushforward_equalizer_mem, CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff, functorPushforward_pullback_le, functorPushforward_union, le_functorPushforward_pullback, generate_map_eq_functorPushforward, mem_functorPushforward_functor, CategoryTheory.CoverPreserving.cover_preserve, functorPushforward_bot, functorPushforward_functor, functor_galoisConnection, functorPushforward_top, functorPullback_pushforward_le, functorPushforward_le_iff_le_functorPullback, CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering, CategoryTheory.Functor.mem_inducedTopology_sieves_iff, image_mem_functorPushforward, functorPushforward_equivalence_eq_pullback
galoisCoinsertionOfMono 📖	CompOp	—
galoisInsertionOfIsSplitEpi 📖	CompOp	—
generate 📖	CompOp	58 math math: TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj, CategoryTheory.GrothendieckTopology.mem_toPretopology, generate_mono, TopCat.Presheaf.generateEquivalenceOpensLe_unitIso, ofArrows_category', generate_functorPullback_le, CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage, CategoryTheory.Presieve.isAmalgamation_sieveExtend, generateSingleton_eq, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as, generate_bot, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom, generate_top, CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve, functorPushforward_extend_eq, CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff, le_generate, generate_sieve, CategoryTheory.Pseudofunctor.IsStackFor_generate_iff, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, generate_of_singleton_isSplitEpi, TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom, CategoryTheory.Presieve.functorPushforward_overForget, CategoryTheory.generate_discretePresieve_mem, CategoryTheory.Precoverage.generate_mem_toGrothendieck, CategoryTheory.Presieve.isSheafFor_iff_generate, generateFamily_eq, TopCat.Presheaf.generateEquivalenceOpensLe_functor, CategoryTheory.ofGrothendieck_iff, TopCat.Presheaf.generateEquivalenceOpensLe_counitIso, overEquiv_symm_generate, TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom, arrows_generate_map_eq_functorPushforward, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, CategoryTheory.PreOneHypercover.sieve₀_cylinder, CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_apply_coe, generate_map_eq_functorPushforward, CategoryTheory.Pseudofunctor.IsPrestackFor_generate_iff, CategoryTheory.Presieve.restrict_extend, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left, pullbackArrows_comm, CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend, overEquiv_generate, TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map, generate_le_iff, CategoryTheory.Pretopology.mem_ofGrothendieck, generate_apply, TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map, CategoryTheory.GrothendieckTopology.mem_toCoverage_iff, CategoryTheory.Presieve.compatibleEquivGenerateSieveCompatible_symm_apply_coe, CategoryTheory.Presieve.isSeparatedFor_iff_generate, generate_of_contains_isSplitEpi, TopCat.Presheaf.generateEquivalenceOpensLe_inverse, CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
giGenerate 📖	CompOp	—
inf 📖	CompOp	—
instCoeFunPresieve 📖	CompOp	—
instCompleteLattice 📖	CompOp	75 math math: AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, generate_mono, mem_iff_pullback_eq_top, generate_functorPullback_le, CategoryTheory.Presheaf.imageSieve_app, functorPushforward_ofObjects_le, pullback_monotone, CategoryTheory.GrothendieckTopology.monotone_close, CategoryTheory.GrothendieckTopology.trivial_covering, CategoryTheory.GrothendieckTopology.arrow_intersect, CategoryTheory.GrothendieckTopology.intersection_covering_iff, top_apply, overEquiv_le_overEquiv_iff, functorPullback_bot, pullback_pushforward_le, generate_bot, sSup_apply, generate_top, equalizer_self, CategoryTheory.GrothendieckTopology.top_mem, CategoryTheory.GrothendieckTopology.closureOperator_isClosed, CategoryTheory.Presheaf.equalizerSieve_self_eq_top, CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁, overEquiv_top, CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem, arrows_eq_top_iff, arrows_top, functorPullback_inter, le_pullback_bind, generate_of_singleton_isSplitEpi, functorPullback_top, le_pushforward_pullback, functorPushforward_monotone, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, functorPullback_monotone, pullback_eq_top_of_mem, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, pullback_inter, ofObjects_mono, functorPushforward_pullback_le, CategoryTheory.GrothendieckTopology.bot_covering, CategoryTheory.GrothendieckTopology.intersection_covering, functorPushforward_union, le_functorPushforward_pullback, functorPushforward_bot, sInf_apply, CategoryTheory.GrothendieckTopology.le_close, galoisConnection, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, functor_galoisConnection, pushforward_union, functorInclusion_top_isIso, pushforward_le_bind_of_mem, overEquiv_symm_top, CategoryTheory.sieve₁'_toPreOneHypercover_eq_top, functorPushforward_top, functorPullback_pushforward_le, functorPushforward_le_iff_le_functorPullback, union_apply, CategoryTheory.GrothendieckTopology.top_mem', CategoryTheory.Presheaf.equalizerSieve_eq_top_iff, inter_apply, CategoryTheory.Functor.imageSieve_map, pullback_top, uliftFunctorInclusion_top_isIso, id_mem_iff_eq_top, pullback_ofObjects_eq_top, pushforward_monotone, generate_le_iff, CategoryTheory.PreOneHypercover.sieve₀_trivial, CategoryTheory.PreOneHypercover.sieve₁_trivial, generate_of_contains_isSplitEpi, ofArrows_le_ofObjects, CategoryTheory.PreZeroHypercover.Hom.sieve₀_le_sieve₀, functorPullback_union
inter 📖	CompOp	—
natTransOfLe 📖	CompOp	2 math math: natTransOfLe_comm, natTransOfLe_app_coe
ofArrows 📖	CompOp	15 math math: ofArrows_category', ofArrows_mk, ofArrows_category, CategoryTheory.regularTopology.equalizerConditionMap_iff_nonempty_isLimit, CategoryTheory.regularTopology.parallelPair_pullback_initial, AlgebraicGeometry.Scheme.Cover.overEquiv_generate_toPresieveOver_eq_ofArrows, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, pullback_ofArrows_of_iso, AlgebraicGeometry.Scheme.grothendieckTopology_cover, mem_ofArrows_iff, exists_eq_ofArrows, ofArrows_le_ofObjects, ofArrows_eq_ofObjects, ofArrows_eq_pullback_of_isPullback, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology
ofObjects 📖	CompOp	9 math math: functorPushforward_ofObjects_le, mem_ofObjects_iff, CategoryTheory.GrothendieckTopology.coversTop_iff_of_isTerminal, pullback_ofObjects, ofObjects_mono, CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible, pullback_ofObjects_eq_top, ofArrows_le_ofObjects, ofArrows_eq_ofObjects
ofTwoArrows 📖	CompOp	—
pullback 📖	CompOp	42 math math: CategoryTheory.Presieve.isSheafFor_pullback_iff, pullback_apply, overEquiv_pullback, mem_iff_pullback_eq_top, pullback_monotone, pullback_functorPushforward_equivalence_eq, CategoryTheory.GrothendieckTopology.isClosed_pullback, pullback_pushforward_le, CategoryTheory.GrothendieckTopology.pullback_stable', CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff, CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁', CategoryTheory.Coverage.Saturate.pullback, le_pullback_bind, CategoryTheory.GrothendieckTopology.pullback_stable, overEquiv_symm_pullback, functorPushforward_inverse, CategoryTheory.Presieve.FamilyOfElements.Compatible.pullback, le_pushforward_pullback, CategoryTheory.Coverage.eq_top_pullback, pullback_eq_top_of_mem, pullback_comp, pullback_ofObjects, pullback_inter, functorPullback_pullback, CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff, functorPushforward_pullback_le, CategoryTheory.PreOneHypercover.sieve₀_cylinder, functorPushforward_functor, galoisConnection, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, CategoryTheory.GrothendieckTopology.pullback_mem_iff_of_isIso, CategoryTheory.Functor.closedSieves_map_coe, CategoryTheory.PreOneHypercover.sieve₁'_cylinder, pullback_ofArrows_of_iso, pullbackArrows_comm, pullback_top, CategoryTheory.PreOneHypercover.sieve₁_inter, CategoryTheory.GrothendieckTopology.covers_iff, pullback_id, CategoryTheory.GrothendieckTopology.pullback_close, functorPushforward_equivalence_eq_pullback, ofArrows_eq_pullback_of_isPullback
pushforward 📖	CompOp	9 math math: pushforward_apply, pullback_pushforward_le, pushforward_comp, le_pushforward_pullback, galoisConnection, pushforward_union, pushforward_le_bind_of_mem, pushforward_monotone, pushforward_apply_comp
sieveInhabited 📖	CompOp	—
sieveOfSubfunctor 📖	CompOp	2 math math: sieveOfSubfunctor_functorInclusion, sieveOfSubfunctor_apply
sieveOfUliftSubfunctor 📖	CompOp	2 math math: sieveOfUliftSubfunctor_apply, sieveOfUliftSubfunctor_uliftFunctorInclusion
sup 📖	CompOp	—
toFunctor 📖	CompOp	1 math math: toFunctor_app_coe
toUliftFunctor 📖	CompOp	1 math math: toUliftFunctor_app_down_coe
uliftFunctor 📖	CompOp	7 math math: uliftNatTransOfLe_comm, uliftNatTransOfLe_app_down_coe, uliftFunctorInclusion_app, sieveOfUliftSubfunctor_uliftFunctorInclusion, uliftFunctorInclusion_is_mono, uliftFunctorInclusion_top_isIso, toUliftFunctor_app_down_coe
uliftFunctorInclusion 📖	CompOp	5 math math: uliftNatTransOfLe_comm, uliftFunctorInclusion_app, sieveOfUliftSubfunctor_uliftFunctorInclusion, uliftFunctorInclusion_is_mono, uliftFunctorInclusion_top_isIso
uliftNatTransOfLe 📖	CompOp	2 math math: uliftNatTransOfLe_comm, uliftNatTransOfLe_app_down_coe
union 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrows_eq_top_iff 📖	mathematical	—	arrows Top.top CategoryTheory.Presieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Sieve instCompleteLattice	—	arrows_ext arrows_top
arrows_ext 📖	—	arrows	—	—	—
arrows_generate_map_eq_functorPushforward 📖	mathematical	—	arrows CategoryTheory.Functor.obj generate CategoryTheory.Presieve.map CategoryTheory.Presieve.functorPushforward	—	Set.ext
arrows_top 📖	mathematical	—	arrows Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Presieve CategoryTheory.instCompleteLatticePresieve	—	—
bind_apply 📖	mathematical	—	arrows bind CategoryTheory.Presieve.bind	—	—
comp_mem_iff 📖	mathematical	—	arrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.IsIso.inv_hom_id_assoc downward_closed
downward_closed 📖	mathematical	arrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
exists_eq_ofArrows 📖	mathematical	—	ofArrows	—	ofArrows_category
ext 📖	—	arrows	—	—	arrows_ext
ext_iff 📖	mathematical	—	arrows	—	ext
functorInclusion_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types functor CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda functorInclusion Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop arrows	—	—
functorInclusion_is_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category functor CategoryTheory.Functor.obj CategoryTheory.yoneda functorInclusion	—	CategoryTheory.NatTrans.ext' CategoryTheory.types_ext CategoryTheory.NatTrans.congr_app
functorInclusion_top_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category functor Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor.obj CategoryTheory.yoneda functorInclusion	—	—
functorPullback_apply 📖	mathematical	—	arrows functorPullback CategoryTheory.Presieve.functorPullback CategoryTheory.Functor.obj	—	—
functorPullback_arrows 📖	mathematical	—	arrows functorPullback CategoryTheory.Presieve.functorPullback CategoryTheory.Functor.obj	—	—
functorPullback_bot 📖	mathematical	—	functorPullback Bot.bot CategoryTheory.Sieve CategoryTheory.Functor.obj OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
functorPullback_comp 📖	mathematical	—	functorPullback CategoryTheory.Functor.comp CategoryTheory.Functor.obj	—	ext
functorPullback_id 📖	mathematical	—	functorPullback CategoryTheory.Functor.id	—	ext
functorPullback_inter 📖	mathematical	—	functorPullback CategoryTheory.Sieve CategoryTheory.Functor.obj SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice instCompleteLattice	—	—
functorPullback_monotone 📖	mathematical	—	Monotone CategoryTheory.Sieve CategoryTheory.Functor.obj PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPullback	—	GaloisConnection.monotone_u functor_galoisConnection
functorPullback_pullback 📖	mathematical	—	functorPullback pullback CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	ext CategoryTheory.Functor.map_comp
functorPullback_pushforward_le 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Functor.obj Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPushforward functorPullback	—	GaloisConnection.l_u_le functor_galoisConnection
functorPullback_top 📖	mathematical	—	functorPullback Top.top CategoryTheory.Sieve CategoryTheory.Functor.obj OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
functorPullback_union 📖	mathematical	—	functorPullback CategoryTheory.Sieve CategoryTheory.Functor.obj SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice	—	—
functorPushforward_apply 📖	mathematical	—	arrows CategoryTheory.Functor.obj functorPushforward CategoryTheory.Presieve.functorPushforward	—	—
functorPushforward_bot 📖	mathematical	—	functorPushforward Bot.bot CategoryTheory.Sieve OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Functor.obj	—	GaloisConnection.l_bot functor_galoisConnection
functorPushforward_comp 📖	mathematical	—	functorPushforward CategoryTheory.Functor.comp CategoryTheory.Functor.obj	—	ext CategoryTheory.Presieve.functorPushforward_comp
functorPushforward_equivalence_eq_pullback 📖	mathematical	—	functorPushforward CategoryTheory.Equivalence.inverse CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor pullback CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitInv	—	ext CategoryTheory.Functor.map_comp CategoryTheory.Equivalence.inv_fun_map CategoryTheory.Category.assoc CategoryTheory.Equivalence.unit_inverse_comp CategoryTheory.Category.comp_id CategoryTheory.NatIso.inv_app_isIso
functorPushforward_extend_eq 📖	mathematical	—	CategoryTheory.Presieve.functorPushforward arrows generate	—	Set.ext CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc le_generate
functorPushforward_functor 📖	mathematical	—	functorPushforward CategoryTheory.Equivalence.functor functorPullback CategoryTheory.Equivalence.inverse CategoryTheory.Functor.obj pullback CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unitInv	—	ext CategoryTheory.Functor.map_comp CategoryTheory.Equivalence.inv_fun_map CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_app CategoryTheory.Category.comp_id downward_closed CategoryTheory.Equivalence.fun_inv_map CategoryTheory.Equivalence.counitInv_functor_comp CategoryTheory.Iso.inv_hom_id_app_assoc
functorPushforward_id 📖	mathematical	—	functorPushforward CategoryTheory.Functor.id	—	ext downward_closed CategoryTheory.Category.id_comp
functorPushforward_inverse 📖	mathematical	—	functorPushforward CategoryTheory.Equivalence.inverse functorPullback CategoryTheory.Equivalence.functor CategoryTheory.Functor.obj pullback CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Equivalence.counit	—	functorPushforward_functor
functorPushforward_le_iff_le_functorPullback 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Functor.obj Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPushforward functorPullback	—	GaloisConnection.le_iff_le functor_galoisConnection
functorPushforward_monotone 📖	mathematical	—	Monotone CategoryTheory.Sieve CategoryTheory.Functor.obj PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPushforward	—	GaloisConnection.monotone_l functor_galoisConnection
functorPushforward_ofObjects_le 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Functor.obj Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPushforward ofObjects	—	—
functorPushforward_pullback_le 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Functor.obj Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPushforward pullback CategoryTheory.Functor.map	—	functorPushforward_le_iff_le_functorPullback functorPullback_pullback pullback_monotone le_functorPushforward_pullback
functorPushforward_top 📖	mathematical	—	functorPushforward Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor.obj	—	generate_sieve generate_of_contains_isSplitEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.IsIso.id CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
functorPushforward_union 📖	mathematical	—	functorPushforward CategoryTheory.Sieve SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice CategoryTheory.Functor.obj	—	GaloisConnection.l_sup functor_galoisConnection
functor_galoisConnection 📖	mathematical	—	GaloisConnection CategoryTheory.Sieve CategoryTheory.Functor.obj PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPushforward functorPullback	—	CategoryTheory.Category.id_comp downward_closed
functor_map_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop arrows CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types functor CategoryTheory.CategoryStruct.comp Quiver.Hom.unop	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types functor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop arrows	—	—
galoisConnection 📖	mathematical	—	GaloisConnection CategoryTheory.Sieve PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice pushforward pullback	—	—
generate_apply 📖	mathematical	—	arrows generate Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	—	—
generate_bot 📖	mathematical	—	generate Bot.bot CategoryTheory.Presieve OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Sieve instCompleteLattice	—	—
generate_functorPullback_le 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice generate CategoryTheory.Presieve.functorPullback functorPullback CategoryTheory.Functor.obj	—	generate_le_iff le_generate
generate_le_iff 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice generate CategoryTheory.Presieve CategoryTheory.instCompleteLatticePresieve arrows	—	CategoryTheory.Category.id_comp downward_closed
generate_map_eq_functorPushforward 📖	mathematical	—	generate CategoryTheory.Functor.obj CategoryTheory.Presieve.map functorPushforward	—	ext arrows_generate_map_eq_functorPushforward functorPushforward_extend_eq
generate_mono 📖	mathematical	—	Monotone CategoryTheory.Presieve CategoryTheory.Sieve PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve instCompleteLattice generate	—	GaloisConnection.monotone_l GaloisInsertion.gc
generate_of_contains_isSplitEpi 📖	mathematical	—	generate Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	id_mem_iff_eq_top CategoryTheory.IsSplitEpi.id
generate_of_singleton_isSplitEpi 📖	mathematical	—	generate CategoryTheory.Presieve.singleton Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	generate_of_contains_isSplitEpi CategoryTheory.Presieve.singleton_self
generate_sieve 📖	mathematical	—	generate arrows	—	GaloisInsertion.l_u_eq
generate_top 📖	mathematical	—	generate Top.top CategoryTheory.Presieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticePresieve BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Sieve instCompleteLattice	—	generate_of_contains_isSplitEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.IsIso.id
id_mem_iff_eq_top 📖	mathematical	—	arrows CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique CategoryTheory.Category.comp_id downward_closed
image_mem_functorPushforward 📖	mathematical	arrows	CategoryTheory.Functor.obj functorPushforward CategoryTheory.Functor.map	—	CategoryTheory.Category.id_comp
inter_apply 📖	mathematical	—	arrows CategoryTheory.Sieve SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice instCompleteLattice	—	—
le_functorPushforward_pullback 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice functorPullback functorPushforward	—	GaloisConnection.le_u_l functor_galoisConnection
le_generate 📖	mathematical	—	CategoryTheory.Presieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CategoryTheory.instCompleteLatticePresieve arrows generate	—	GaloisConnection.le_u_l GaloisInsertion.gc
le_pullback_bind 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice pullback bind	—	galoisConnection pushforward_le_bind_of_mem
le_pushforward_pullback 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice pullback pushforward	—	GaloisConnection.le_u_l galoisConnection
mem_functorPushforward_functor 📖	mathematical	—	arrows CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor functorPushforward CategoryTheory.Equivalence.inverse CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Equivalence.unitInv	—	functorPushforward_functor
mem_functorPushforward_iff_of_full 📖	mathematical	—	CategoryTheory.Presieve.functorPushforward arrows CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Functor.map_surjective CategoryTheory.Functor.map_comp downward_closed CategoryTheory.Category.id_comp
mem_functorPushforward_iff_of_full_of_faithful 📖	mathematical	—	CategoryTheory.Presieve.functorPushforward arrows CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	mem_functorPushforward_iff_of_full CategoryTheory.Functor.map_injective
mem_functorPushforward_inverse 📖	mathematical	—	arrows CategoryTheory.Functor.obj CategoryTheory.Equivalence.inverse functorPushforward CategoryTheory.Equivalence.functor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Equivalence.counit	—	functorPushforward_inverse
mem_iff_pullback_eq_top 📖	mathematical	—	arrows pullback Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	id_mem_iff_eq_top pullback_apply CategoryTheory.Category.id_comp
mem_ofArrows_iff 📖	mathematical	—	arrows ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	downward_closed
mem_ofObjects_iff 📖	mathematical	—	arrows ofObjects Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
natTransOfLe_app_coe 📖	mathematical	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop arrows CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types functor natTransOfLe	—	—
natTransOfLe_comm 📖	mathematical	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category functor CategoryTheory.Functor.obj CategoryTheory.yoneda natTransOfLe functorInclusion	—	—
ofArrows_category 📖	mathematical	—	ofArrows CategoryTheory.Presieve.category arrows CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom	—	ofArrows_category' generate_sieve
ofArrows_category' 📖	mathematical	—	ofArrows CategoryTheory.Presieve.category CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom generate	—	le_antisymm generate_le_iff CategoryTheory.Category.id_comp
ofArrows_eq_ofObjects 📖	mathematical	—	ofArrows ofObjects	—	le_antisymm ofArrows_le_ofObjects mem_ofArrows_iff mem_ofObjects_iff CategoryTheory.Limits.IsTerminal.hom_ext
ofArrows_eq_pullback_of_isPullback 📖	mathematical	CategoryTheory.IsPullback	ofArrows pullback	—	le_antisymm ofArrows.eq_1 generate_le_iff CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.lift_fst
ofArrows_le_ofObjects 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice ofArrows ofObjects	—	mem_ofArrows_iff
ofArrows_mk 📖	mathematical	—	arrows ofArrows	—	CategoryTheory.Category.id_comp
ofObjects_mono 📖	mathematical	Set Set.instHasSubset Set.range	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice ofObjects	—	—
pullbackArrows_comm 📖	mathematical	—	generate CategoryTheory.Presieve.pullbackArrows pullback	—	ext CategoryTheory.Presieve.hasPullback pullback_apply CategoryTheory.Category.assoc CategoryTheory.Limits.pullback.condition downward_closed le_generate CategoryTheory.Limits.pullback.lift_snd
pullback_apply 📖	mathematical	—	arrows pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
pullback_comp 📖	mathematical	—	pullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc
pullback_eq_top_of_mem 📖	mathematical	arrows	pullback Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	mem_iff_pullback_eq_top
pullback_functorPushforward_equivalence_eq 📖	mathematical	—	pullback CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Equivalence.unit functorPushforward	—	ext CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Equivalence.functor_unit_comp CategoryTheory.Category.comp_id CategoryTheory.Equivalence.inv_fun_map CategoryTheory.Iso.hom_inv_id_app CategoryTheory.NatIso.inv_app_isIso
pullback_id 📖	mathematical	—	pullback CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id
pullback_inter 📖	mathematical	—	pullback CategoryTheory.Sieve SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice instCompleteLattice	—	—
pullback_monotone 📖	mathematical	—	Monotone CategoryTheory.Sieve PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice pullback	—	GaloisConnection.monotone_u galoisConnection
pullback_ofArrows_of_iso 📖	mathematical	—	pullback CategoryTheory.Iso.hom ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv	—	ext_iff CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id
pullback_ofObjects 📖	mathematical	—	pullback ofObjects	—	ext
pullback_ofObjects_eq_top 📖	mathematical	—	ofObjects Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	ext mem_ofObjects_iff
pullback_pushforward_le 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice pushforward pullback	—	GaloisConnection.l_u_le galoisConnection
pullback_top 📖	mathematical	—	pullback Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique
pushforward_apply 📖	mathematical	—	arrows pushforward Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	—	—
pushforward_apply_comp 📖	mathematical	arrows	pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
pushforward_comp 📖	mathematical	—	pushforward CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	ext CategoryTheory.Category.assoc
pushforward_le_bind_of_mem 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice pushforward bind	—	—
pushforward_monotone 📖	mathematical	—	Monotone CategoryTheory.Sieve PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice pushforward	—	GaloisConnection.monotone_l galoisConnection
pushforward_union 📖	mathematical	—	pushforward CategoryTheory.Sieve SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice	—	GaloisConnection.l_sup galoisConnection
sInf_apply 📖	mathematical	—	arrows InfSet.sInf CategoryTheory.Sieve CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf instCompleteLattice	—	—
sSup_apply 📖	mathematical	—	arrows SupSet.sSup CategoryTheory.Sieve CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instCompleteLattice	—	—
sieveOfSubfunctor_apply 📖	mathematical	—	arrows sieveOfSubfunctor CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.NatTrans.app	—	—
sieveOfSubfunctor_functorInclusion 📖	mathematical	—	sieveOfSubfunctor functor functorInclusion	—	ext
sieveOfUliftSubfunctor_apply 📖	mathematical	—	arrows sieveOfUliftSubfunctor CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftYoneda CategoryTheory.NatTrans.app CategoryTheory.yoneda	—	—
sieveOfUliftSubfunctor_uliftFunctorInclusion 📖	mathematical	—	sieveOfUliftSubfunctor uliftFunctor uliftFunctorInclusion	—	ext
toFunctor_app_coe 📖	mathematical	arrows	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda functor toFunctor CategoryTheory.CategoryStruct.comp	—	—
toUliftFunctor_app_down_coe 📖	mathematical	arrows	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types functor CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftYoneda uliftFunctor toUliftFunctor CategoryTheory.CategoryStruct.comp CategoryTheory.yoneda	—	—
top_apply 📖	mathematical	—	arrows Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
uliftFunctorInclusion_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types uliftFunctor CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftYoneda uliftFunctorInclusion Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop arrows	—	—
uliftFunctorInclusion_is_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category uliftFunctor CategoryTheory.Functor.obj CategoryTheory.uliftYoneda uliftFunctorInclusion	—	CategoryTheory.NatTrans.ext' CategoryTheory.types_ext ULift.ext CategoryTheory.NatTrans.congr_app
uliftFunctorInclusion_top_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category uliftFunctor Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Functor.obj CategoryTheory.uliftYoneda uliftFunctorInclusion	—	—
uliftNatTransOfLe_app_down_coe 📖	mathematical	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop arrows CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types functor CategoryTheory.NatTrans.app uliftFunctor uliftNatTransOfLe	—	—
uliftNatTransOfLe_comm 📖	mathematical	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instCompleteLattice	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category uliftFunctor CategoryTheory.Functor.obj CategoryTheory.uliftYoneda uliftNatTransOfLe uliftFunctorInclusion	—	—
union_apply 📖	mathematical	—	arrows CategoryTheory.Sieve SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice	—	—

CategoryTheory.Sieve.ofArrows

Definitions

Name	Category	Theorems
h 📖	CompOp	3 math math: fac, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, fac_assoc
i 📖	CompOp	3 math math: fac, CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows, fac_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists 📖	mathematical	CategoryTheory.Sieve.arrows CategoryTheory.Sieve.ofArrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
fac 📖	mathematical	CategoryTheory.Sieve.arrows CategoryTheory.Sieve.ofArrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i h	—	exists
fac_assoc 📖	mathematical	CategoryTheory.Sieve.arrows CategoryTheory.Sieve.ofArrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i h	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac

---

← Back to Index