Commit 2026-08-23 14:46 f2916a54

View on Github →

refactor(CategoryTheory/Sites): split long file Sieves.lean (#43014) Split this file into the following pieces:

Presieve.lean — 434 lines — Presieves, arrow families, binding, pullback and pushforward along morphisms, pullback existence, and uncurrying.
Basic.lean — 526 lines — Core sieve theory: generation, lattice structure, arrow families, pullbacks, and pushforwards.
Functoriality.lean — 438 lines — Pullback, pushforward, and mapping of both presieves and sieves along functors and equivalences.
Presheaf.lean — 153 lines — The presheaf associated to a sieve and its inclusion into the Yoneda presheaf.
Shrink.lean — 83 lines — Universe-shrunk sieve presheaves and their comparison isomorphisms.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Sites/Precoverage.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

deleted theorem CategoryTheory.Presieve.BindStruct.bind

deleted structure CategoryTheory.Presieve.BindStruct

deleted structure CategoryTheory.Presieve.FunctorPushforwardStructure

deleted def CategoryTheory.Presieve.bind

deleted inductive CategoryTheory.Presieve.bindOfArrows

deleted theorem CategoryTheory.Presieve.bindOfArrows_ofArrows

deleted theorem CategoryTheory.Presieve.bind_comp

deleted theorem CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows

deleted theorem CategoryTheory.Presieve.exists_eq_ofArrows

deleted def CategoryTheory.Presieve.functorPullback

deleted theorem CategoryTheory.Presieve.functorPullback_arrows

deleted theorem CategoryTheory.Presieve.functorPullback_id

deleted theorem CategoryTheory.Presieve.functorPullback_map_functorPullback

deleted theorem CategoryTheory.Presieve.functorPullback_mem

deleted theorem CategoryTheory.Presieve.functorPullback_monotone

deleted def CategoryTheory.Presieve.functorPushforward

deleted theorem CategoryTheory.Presieve.functorPushforward_comp

deleted theorem CategoryTheory.Presieve.functorPushforward_monotone

deleted theorem CategoryTheory.Presieve.functorPushforward_overForget

deleted theorem CategoryTheory.Presieve.galoisConnection_map_functorPullback

deleted theorem CategoryTheory.Presieve.galoisConnection_pushforward_pullback

deleted theorem CategoryTheory.Presieve.image_mem_functorPushforward

deleted theorem CategoryTheory.Presieve.le_functorPullback_map

deleted theorem CategoryTheory.Presieve.le_pullback_pushforward

deleted inductive CategoryTheory.Presieve.map

deleted theorem CategoryTheory.Presieve.map_bot

deleted theorem CategoryTheory.Presieve.map_functorPullback

deleted theorem CategoryTheory.Presieve.map_functorPullback_map

deleted theorem CategoryTheory.Presieve.map_id

deleted theorem CategoryTheory.Presieve.map_iff

deleted theorem CategoryTheory.Presieve.map_le_functorPushforward

deleted theorem CategoryTheory.Presieve.map_le_iff_le_functorPullback

deleted theorem CategoryTheory.Presieve.map_map

deleted theorem CategoryTheory.Presieve.map_monotone

deleted theorem CategoryTheory.Presieve.map_ofArrows

deleted theorem CategoryTheory.Presieve.map_singleton

deleted theorem CategoryTheory.Presieve.monotone_pullback

deleted theorem CategoryTheory.Presieve.monotone_pushforward

deleted theorem CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx

deleted theorem CategoryTheory.Presieve.ofArrows.hom_idx

deleted def CategoryTheory.Presieve.ofArrows.idx

deleted theorem CategoryTheory.Presieve.ofArrows.mk'

deleted theorem CategoryTheory.Presieve.ofArrows.obj_idx

deleted inductive CategoryTheory.Presieve.ofArrows

deleted theorem CategoryTheory.Presieve.ofArrows_bind

deleted theorem CategoryTheory.Presieve.ofArrows_category

deleted theorem CategoryTheory.Presieve.ofArrows_comp_eq_of_surjective

deleted theorem CategoryTheory.Presieve.ofArrows_comp_le

deleted theorem CategoryTheory.Presieve.ofArrows_eq_ofArrows_uncurry

deleted theorem CategoryTheory.Presieve.ofArrows_le_iff

deleted theorem CategoryTheory.Presieve.ofArrows_of_isEmpty

deleted theorem CategoryTheory.Presieve.ofArrows_of_unique

deleted theorem CategoryTheory.Presieve.ofArrows_pUnit

deleted theorem CategoryTheory.Presieve.ofArrows_pullback

deleted theorem CategoryTheory.Presieve.ofArrows_surj

deleted def CategoryTheory.Presieve.pullback

deleted inductive CategoryTheory.Presieve.pullbackArrows

deleted theorem CategoryTheory.Presieve.pullback_comp

deleted theorem CategoryTheory.Presieve.pullback_id

deleted theorem CategoryTheory.Presieve.pullback_iff

deleted theorem CategoryTheory.Presieve.pullback_singleton

deleted def CategoryTheory.Presieve.pushforward

deleted theorem CategoryTheory.Presieve.pushforward_apply_comp

deleted theorem CategoryTheory.Presieve.pushforward_comp

deleted theorem CategoryTheory.Presieve.pushforward_id

deleted theorem CategoryTheory.Presieve.pushforward_le_iff_le_pullback

deleted theorem CategoryTheory.Presieve.pushforward_ofArrows

deleted theorem CategoryTheory.Presieve.pushforward_pullback_le

deleted theorem CategoryTheory.Presieve.pushforward_singleton

deleted inductive CategoryTheory.Presieve.singleton

deleted theorem CategoryTheory.Presieve.singleton_eq_iff_domain

deleted theorem CategoryTheory.Presieve.singleton_le_iff

deleted theorem CategoryTheory.Presieve.singleton_self

deleted def CategoryTheory.Presieve.uncurry

deleted theorem CategoryTheory.Presieve.uncurry_bind

deleted theorem CategoryTheory.Presieve.uncurry_ofArrows

deleted theorem CategoryTheory.Presieve.uncurry_pullbackArrows

deleted theorem CategoryTheory.Presieve.uncurry_singleton

deleted def CategoryTheory.Presieve

deleted theorem CategoryTheory.Sieve.arrows_bot

deleted theorem CategoryTheory.Sieve.arrows_eq_bot_iff

deleted theorem CategoryTheory.Sieve.arrows_eq_top_iff

deleted theorem CategoryTheory.Sieve.arrows_ext

deleted theorem CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward

deleted theorem CategoryTheory.Sieve.arrows_mono

deleted theorem CategoryTheory.Sieve.arrows_top

deleted def CategoryTheory.Sieve.bind

deleted theorem CategoryTheory.Sieve.bot_apply

deleted theorem CategoryTheory.Sieve.comp_mem_iff

deleted def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion

deleted theorem CategoryTheory.Sieve.exists_eq_ofArrows

deleted def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion

deleted def CategoryTheory.Sieve.functor

deleted def CategoryTheory.Sieve.functorInclusion

deleted def CategoryTheory.Sieve.functorPullback

deleted theorem CategoryTheory.Sieve.functorPullback_arrows

deleted theorem CategoryTheory.Sieve.functorPullback_bot

deleted theorem CategoryTheory.Sieve.functorPullback_comp

deleted theorem CategoryTheory.Sieve.functorPullback_functorPushforward_eq

deleted theorem CategoryTheory.Sieve.functorPullback_id

deleted theorem CategoryTheory.Sieve.functorPullback_inter

deleted theorem CategoryTheory.Sieve.functorPullback_monotone

deleted theorem CategoryTheory.Sieve.functorPullback_pullback

deleted theorem CategoryTheory.Sieve.functorPullback_pushforward_le

deleted theorem CategoryTheory.Sieve.functorPullback_top

deleted theorem CategoryTheory.Sieve.functorPullback_union

deleted def CategoryTheory.Sieve.functorPushforward

deleted theorem CategoryTheory.Sieve.functorPushforward_bot

deleted theorem CategoryTheory.Sieve.functorPushforward_comp

deleted theorem CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback

deleted theorem CategoryTheory.Sieve.functorPushforward_extend_eq

deleted theorem CategoryTheory.Sieve.functorPushforward_functor

deleted theorem CategoryTheory.Sieve.functorPushforward_id

deleted theorem CategoryTheory.Sieve.functorPushforward_inverse

deleted theorem CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback

deleted theorem CategoryTheory.Sieve.functorPushforward_monotone

deleted theorem CategoryTheory.Sieve.functorPushforward_ofArrows

deleted theorem CategoryTheory.Sieve.functorPushforward_ofObjects_le

deleted theorem CategoryTheory.Sieve.functorPushforward_pullback_le

deleted theorem CategoryTheory.Sieve.functorPushforward_top

deleted theorem CategoryTheory.Sieve.functorPushforward_union

deleted theorem CategoryTheory.Sieve.functor_galoisConnection

deleted def CategoryTheory.Sieve.galoisCoinsertionOfMono

deleted theorem CategoryTheory.Sieve.galoisConnection

deleted def CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi

deleted def CategoryTheory.Sieve.generate

deleted theorem CategoryTheory.Sieve.generate_bot

deleted theorem CategoryTheory.Sieve.generate_eq_bot_iff

deleted theorem CategoryTheory.Sieve.generate_functorPullback_le

deleted theorem CategoryTheory.Sieve.generate_le_iff

deleted theorem CategoryTheory.Sieve.generate_map_eq_functorPushforward

deleted theorem CategoryTheory.Sieve.generate_mono

deleted theorem CategoryTheory.Sieve.generate_of_contains_isSplitEpi

deleted theorem CategoryTheory.Sieve.generate_of_singleton_isSplitEpi

deleted theorem CategoryTheory.Sieve.generate_pushforward

deleted theorem CategoryTheory.Sieve.generate_sieve

deleted theorem CategoryTheory.Sieve.generate_top

deleted def CategoryTheory.Sieve.giGenerate

deleted theorem CategoryTheory.Sieve.id_mem_iff_eq_top

deleted theorem CategoryTheory.Sieve.image_mem_functorPushforward

deleted theorem CategoryTheory.Sieve.inter_apply

deleted theorem CategoryTheory.Sieve.le_functorPushforward_pullback

deleted theorem CategoryTheory.Sieve.le_generate

deleted theorem CategoryTheory.Sieve.le_pullback_bind

deleted theorem CategoryTheory.Sieve.le_pushforward_pullback

deleted theorem CategoryTheory.Sieve.mem_functorPushforward_functor

deleted theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full

deleted theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful

deleted theorem CategoryTheory.Sieve.mem_functorPushforward_inverse

deleted theorem CategoryTheory.Sieve.mem_iff_pullback_eq_top

deleted theorem CategoryTheory.Sieve.mem_ofArrows_iff

deleted theorem CategoryTheory.Sieve.mem_ofObjects_iff

deleted def CategoryTheory.Sieve.natTransOfLe

deleted theorem CategoryTheory.Sieve.natTransOfLe_comm

deleted theorem CategoryTheory.Sieve.ofArrows.exists

deleted theorem CategoryTheory.Sieve.ofArrows.fac

deleted theorem CategoryTheory.Sieve.ofArrows_category'

deleted theorem CategoryTheory.Sieve.ofArrows_category

deleted theorem CategoryTheory.Sieve.ofArrows_eq_ofObjects

deleted theorem CategoryTheory.Sieve.ofArrows_eq_pullback_of_isPullback

deleted theorem CategoryTheory.Sieve.ofArrows_le_ofObjects

deleted theorem CategoryTheory.Sieve.ofArrows_mk

deleted def CategoryTheory.Sieve.ofObjects

deleted theorem CategoryTheory.Sieve.ofObjects_id

deleted theorem CategoryTheory.Sieve.ofObjects_mono

deleted def CategoryTheory.Sieve.pullback

deleted theorem CategoryTheory.Sieve.pullbackArrows_comm

deleted theorem CategoryTheory.Sieve.pullback_arrows

deleted theorem CategoryTheory.Sieve.pullback_bot

deleted theorem CategoryTheory.Sieve.pullback_comp

deleted theorem CategoryTheory.Sieve.pullback_eq_top_of_mem

deleted theorem CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq

deleted theorem CategoryTheory.Sieve.pullback_id

deleted theorem CategoryTheory.Sieve.pullback_inter

deleted theorem CategoryTheory.Sieve.pullback_monotone

deleted theorem CategoryTheory.Sieve.pullback_ofArrows_of_iso

deleted theorem CategoryTheory.Sieve.pullback_ofObjects

deleted theorem CategoryTheory.Sieve.pullback_ofObjects_eq_top

deleted theorem CategoryTheory.Sieve.pullback_pushforward_le

deleted theorem CategoryTheory.Sieve.pullback_top

deleted def CategoryTheory.Sieve.pushforward

deleted theorem CategoryTheory.Sieve.pushforward_apply_comp

deleted theorem CategoryTheory.Sieve.pushforward_arrows

deleted theorem CategoryTheory.Sieve.pushforward_bot

deleted theorem CategoryTheory.Sieve.pushforward_comp

deleted theorem CategoryTheory.Sieve.pushforward_eq_bot_iff

deleted theorem CategoryTheory.Sieve.pushforward_le_bind_of_mem

deleted theorem CategoryTheory.Sieve.pushforward_monotone

deleted theorem CategoryTheory.Sieve.pushforward_union

deleted theorem CategoryTheory.Sieve.sInf_apply

deleted theorem CategoryTheory.Sieve.sSup_apply

deleted def CategoryTheory.Sieve.shrinkFunctor

deleted def CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso

deleted theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι

deleted def CategoryTheory.Sieve.sieveOfSubfunctor

deleted theorem CategoryTheory.Sieve.sieveOfSubfunctor_functorInclusion

deleted def CategoryTheory.Sieve.sieveOfUliftSubfunctor

deleted theorem CategoryTheory.Sieve.sieveOfUliftSubfunctor_uliftFunctorInclusion

deleted def CategoryTheory.Sieve.toFunctor

deleted def CategoryTheory.Sieve.toUliftFunctor

deleted theorem CategoryTheory.Sieve.top_apply

deleted def CategoryTheory.Sieve.uliftFunctorInclusion

deleted def CategoryTheory.Sieve.uliftNatTransOfLe

deleted theorem CategoryTheory.Sieve.uliftNatTransOfLe_comm

deleted theorem CategoryTheory.Sieve.union_apply

deleted structure CategoryTheory.Sieve

deleted theorem CategoryTheory.bot_apply

deleted theorem CategoryTheory.top_apply

Created Mathlib/CategoryTheory/Sites/Sieves/Basic.lean

added theorem CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows

added theorem CategoryTheory.Sieve.arrows_bot

added theorem CategoryTheory.Sieve.arrows_eq_bot_iff

added theorem CategoryTheory.Sieve.arrows_eq_top_iff

added theorem CategoryTheory.Sieve.arrows_ext

added theorem CategoryTheory.Sieve.arrows_mono

added theorem CategoryTheory.Sieve.arrows_top

added def CategoryTheory.Sieve.bind

added theorem CategoryTheory.Sieve.bot_apply

added theorem CategoryTheory.Sieve.comp_mem_iff

added theorem CategoryTheory.Sieve.exists_eq_ofArrows

added def CategoryTheory.Sieve.galoisCoinsertionOfMono

added theorem CategoryTheory.Sieve.galoisConnection

added def CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi

added def CategoryTheory.Sieve.generate

added theorem CategoryTheory.Sieve.generate_bot

added theorem CategoryTheory.Sieve.generate_eq_bot_iff

added theorem CategoryTheory.Sieve.generate_le_iff

added theorem CategoryTheory.Sieve.generate_mono

added theorem CategoryTheory.Sieve.generate_of_contains_isSplitEpi

added theorem CategoryTheory.Sieve.generate_of_singleton_isSplitEpi

added theorem CategoryTheory.Sieve.generate_pushforward

added theorem CategoryTheory.Sieve.generate_sieve

added theorem CategoryTheory.Sieve.generate_top

added def CategoryTheory.Sieve.giGenerate

added theorem CategoryTheory.Sieve.id_mem_iff_eq_top

added theorem CategoryTheory.Sieve.inter_apply

added theorem CategoryTheory.Sieve.le_generate

added theorem CategoryTheory.Sieve.le_pullback_bind

added theorem CategoryTheory.Sieve.le_pushforward_pullback

added theorem CategoryTheory.Sieve.mem_iff_pullback_eq_top

added theorem CategoryTheory.Sieve.mem_ofArrows_iff

added theorem CategoryTheory.Sieve.mem_ofObjects_iff

added theorem CategoryTheory.Sieve.ofArrows.exists

added theorem CategoryTheory.Sieve.ofArrows.fac

added theorem CategoryTheory.Sieve.ofArrows_category'

added theorem CategoryTheory.Sieve.ofArrows_category

added theorem CategoryTheory.Sieve.ofArrows_eq_ofObjects

added theorem CategoryTheory.Sieve.ofArrows_eq_pullback_of_isPullback

added theorem CategoryTheory.Sieve.ofArrows_le_ofObjects

added theorem CategoryTheory.Sieve.ofArrows_mk

added def CategoryTheory.Sieve.ofObjects

added theorem CategoryTheory.Sieve.ofObjects_id

added theorem CategoryTheory.Sieve.ofObjects_mono

added def CategoryTheory.Sieve.pullback

added theorem CategoryTheory.Sieve.pullbackArrows_comm

added theorem CategoryTheory.Sieve.pullback_arrows

added theorem CategoryTheory.Sieve.pullback_bot

added theorem CategoryTheory.Sieve.pullback_comp

added theorem CategoryTheory.Sieve.pullback_eq_top_of_mem

added theorem CategoryTheory.Sieve.pullback_id

added theorem CategoryTheory.Sieve.pullback_inter

added theorem CategoryTheory.Sieve.pullback_monotone

added theorem CategoryTheory.Sieve.pullback_ofArrows_of_iso

added theorem CategoryTheory.Sieve.pullback_ofObjects

added theorem CategoryTheory.Sieve.pullback_ofObjects_eq_top

added theorem CategoryTheory.Sieve.pullback_pushforward_le

added theorem CategoryTheory.Sieve.pullback_top

added def CategoryTheory.Sieve.pushforward

added theorem CategoryTheory.Sieve.pushforward_apply_comp

added theorem CategoryTheory.Sieve.pushforward_arrows

added theorem CategoryTheory.Sieve.pushforward_bot

added theorem CategoryTheory.Sieve.pushforward_comp

added theorem CategoryTheory.Sieve.pushforward_eq_bot_iff

added theorem CategoryTheory.Sieve.pushforward_le_bind_of_mem

added theorem CategoryTheory.Sieve.pushforward_monotone

added theorem CategoryTheory.Sieve.pushforward_union

added theorem CategoryTheory.Sieve.sInf_apply

added theorem CategoryTheory.Sieve.sSup_apply

added theorem CategoryTheory.Sieve.top_apply

added theorem CategoryTheory.Sieve.union_apply

added structure CategoryTheory.Sieve

Created Mathlib/CategoryTheory/Sites/Sieves/Functoriality.lean

added structure CategoryTheory.Presieve.FunctorPushforwardStructure

added def CategoryTheory.Presieve.functorPullback

added theorem CategoryTheory.Presieve.functorPullback_arrows

added theorem CategoryTheory.Presieve.functorPullback_id

added theorem CategoryTheory.Presieve.functorPullback_map_functorPullback

added theorem CategoryTheory.Presieve.functorPullback_mem

added theorem CategoryTheory.Presieve.functorPullback_monotone

added def CategoryTheory.Presieve.functorPushforward

added theorem CategoryTheory.Presieve.functorPushforward_comp

added theorem CategoryTheory.Presieve.functorPushforward_monotone

added theorem CategoryTheory.Presieve.functorPushforward_overForget

added theorem CategoryTheory.Presieve.galoisConnection_map_functorPullback

added theorem CategoryTheory.Presieve.image_mem_functorPushforward

added theorem CategoryTheory.Presieve.le_functorPullback_map

added inductive CategoryTheory.Presieve.map

added theorem CategoryTheory.Presieve.map_bot

added theorem CategoryTheory.Presieve.map_functorPullback

added theorem CategoryTheory.Presieve.map_functorPullback_map

added theorem CategoryTheory.Presieve.map_id

added theorem CategoryTheory.Presieve.map_iff

added theorem CategoryTheory.Presieve.map_le_functorPushforward

added theorem CategoryTheory.Presieve.map_le_iff_le_functorPullback

added theorem CategoryTheory.Presieve.map_map

added theorem CategoryTheory.Presieve.map_monotone

added theorem CategoryTheory.Presieve.map_ofArrows

added theorem CategoryTheory.Presieve.map_singleton

added theorem CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward

added def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion

added def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion

added def CategoryTheory.Sieve.functorPullback

added theorem CategoryTheory.Sieve.functorPullback_arrows

added theorem CategoryTheory.Sieve.functorPullback_bot

added theorem CategoryTheory.Sieve.functorPullback_comp

added theorem CategoryTheory.Sieve.functorPullback_functorPushforward_eq

added theorem CategoryTheory.Sieve.functorPullback_id

added theorem CategoryTheory.Sieve.functorPullback_inter

added theorem CategoryTheory.Sieve.functorPullback_monotone

added theorem CategoryTheory.Sieve.functorPullback_pullback

added theorem CategoryTheory.Sieve.functorPullback_pushforward_le

added theorem CategoryTheory.Sieve.functorPullback_top

added theorem CategoryTheory.Sieve.functorPullback_union

added def CategoryTheory.Sieve.functorPushforward

added theorem CategoryTheory.Sieve.functorPushforward_bot

added theorem CategoryTheory.Sieve.functorPushforward_comp

added theorem CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback

added theorem CategoryTheory.Sieve.functorPushforward_extend_eq

added theorem CategoryTheory.Sieve.functorPushforward_functor

added theorem CategoryTheory.Sieve.functorPushforward_id

added theorem CategoryTheory.Sieve.functorPushforward_inverse

added theorem CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback

added theorem CategoryTheory.Sieve.functorPushforward_monotone

added theorem CategoryTheory.Sieve.functorPushforward_ofArrows

added theorem CategoryTheory.Sieve.functorPushforward_ofObjects_le

added theorem CategoryTheory.Sieve.functorPushforward_pullback_le

added theorem CategoryTheory.Sieve.functorPushforward_top

added theorem CategoryTheory.Sieve.functorPushforward_union

added theorem CategoryTheory.Sieve.functor_galoisConnection

added theorem CategoryTheory.Sieve.generate_functorPullback_le

added theorem CategoryTheory.Sieve.generate_map_eq_functorPushforward

added theorem CategoryTheory.Sieve.image_mem_functorPushforward

added theorem CategoryTheory.Sieve.le_functorPushforward_pullback

added theorem CategoryTheory.Sieve.mem_functorPushforward_functor

added theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full

added theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful

added theorem CategoryTheory.Sieve.mem_functorPushforward_inverse

added theorem CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq

Created Mathlib/CategoryTheory/Sites/Sieves/Presheaf.lean

added def CategoryTheory.Sieve.functor

added def CategoryTheory.Sieve.functorInclusion

added def CategoryTheory.Sieve.natTransOfLe

added theorem CategoryTheory.Sieve.natTransOfLe_comm

added def CategoryTheory.Sieve.sieveOfSubfunctor

added theorem CategoryTheory.Sieve.sieveOfSubfunctor_functorInclusion

added def CategoryTheory.Sieve.sieveOfUliftSubfunctor

added theorem CategoryTheory.Sieve.sieveOfUliftSubfunctor_uliftFunctorInclusion

added def CategoryTheory.Sieve.toFunctor

added def CategoryTheory.Sieve.toUliftFunctor

added def CategoryTheory.Sieve.uliftFunctorInclusion

added def CategoryTheory.Sieve.uliftNatTransOfLe

added theorem CategoryTheory.Sieve.uliftNatTransOfLe_comm

Created Mathlib/CategoryTheory/Sites/Sieves/Presieve.lean

added theorem CategoryTheory.Presieve.BindStruct.bind

added structure CategoryTheory.Presieve.BindStruct

added def CategoryTheory.Presieve.bind

added inductive CategoryTheory.Presieve.bindOfArrows

added theorem CategoryTheory.Presieve.bindOfArrows_ofArrows

added theorem CategoryTheory.Presieve.bind_comp

added theorem CategoryTheory.Presieve.exists_eq_ofArrows

added theorem CategoryTheory.Presieve.galoisConnection_pushforward_pullback

added theorem CategoryTheory.Presieve.le_pullback_pushforward

added theorem CategoryTheory.Presieve.monotone_pullback

added theorem CategoryTheory.Presieve.monotone_pushforward

added theorem CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx

added theorem CategoryTheory.Presieve.ofArrows.hom_idx

added def CategoryTheory.Presieve.ofArrows.idx

added theorem CategoryTheory.Presieve.ofArrows.mk'

added theorem CategoryTheory.Presieve.ofArrows.obj_idx

added inductive CategoryTheory.Presieve.ofArrows

added theorem CategoryTheory.Presieve.ofArrows_bind

added theorem CategoryTheory.Presieve.ofArrows_category

added theorem CategoryTheory.Presieve.ofArrows_comp_eq_of_surjective

added theorem CategoryTheory.Presieve.ofArrows_comp_le

added theorem CategoryTheory.Presieve.ofArrows_eq_ofArrows_uncurry

added theorem CategoryTheory.Presieve.ofArrows_le_iff

added theorem CategoryTheory.Presieve.ofArrows_of_isEmpty

added theorem CategoryTheory.Presieve.ofArrows_of_unique

added theorem CategoryTheory.Presieve.ofArrows_pUnit

added theorem CategoryTheory.Presieve.ofArrows_pullback

added theorem CategoryTheory.Presieve.ofArrows_surj

added def CategoryTheory.Presieve.pullback

added inductive CategoryTheory.Presieve.pullbackArrows

added theorem CategoryTheory.Presieve.pullback_comp

added theorem CategoryTheory.Presieve.pullback_id

added theorem CategoryTheory.Presieve.pullback_iff

added theorem CategoryTheory.Presieve.pullback_singleton

added def CategoryTheory.Presieve.pushforward

added theorem CategoryTheory.Presieve.pushforward_apply_comp

added theorem CategoryTheory.Presieve.pushforward_comp

added theorem CategoryTheory.Presieve.pushforward_id

added theorem CategoryTheory.Presieve.pushforward_le_iff_le_pullback

added theorem CategoryTheory.Presieve.pushforward_ofArrows

added theorem CategoryTheory.Presieve.pushforward_pullback_le

added theorem CategoryTheory.Presieve.pushforward_singleton

added inductive CategoryTheory.Presieve.singleton

added theorem CategoryTheory.Presieve.singleton_eq_iff_domain

added theorem CategoryTheory.Presieve.singleton_le_iff

added theorem CategoryTheory.Presieve.singleton_self

added def CategoryTheory.Presieve.uncurry

added theorem CategoryTheory.Presieve.uncurry_bind

added theorem CategoryTheory.Presieve.uncurry_ofArrows

added theorem CategoryTheory.Presieve.uncurry_pullbackArrows

added theorem CategoryTheory.Presieve.uncurry_singleton

added def CategoryTheory.Presieve

added theorem CategoryTheory.bot_apply

added theorem CategoryTheory.top_apply

Created Mathlib/CategoryTheory/Sites/Sieves/Shrink.lean

added def CategoryTheory.Sieve.shrinkFunctor

added def CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso

added theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι