Commit 2023-03-07 13:26 26763c5c

View on Github →

feat: port CategoryTheory.Sites.Sieves (#2691)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Sieves.lean

added structure CategoryTheory.Presieve.FunctorPushforwardStructure

added def CategoryTheory.Presieve.bind

added theorem CategoryTheory.Presieve.bind_comp

added def CategoryTheory.Presieve.functorPullback

added theorem CategoryTheory.Presieve.functorPullback_id

added theorem CategoryTheory.Presieve.functorPullback_mem

added def CategoryTheory.Presieve.functorPushforward

added theorem CategoryTheory.Presieve.functorPushforward_comp

added theorem CategoryTheory.Presieve.image_mem_functorPushforward

added inductive CategoryTheory.Presieve.ofArrows

added theorem CategoryTheory.Presieve.ofArrows_bind

added theorem CategoryTheory.Presieve.ofArrows_pUnit

added theorem CategoryTheory.Presieve.ofArrows_pullback

added inductive CategoryTheory.Presieve.pullbackArrows

added theorem CategoryTheory.Presieve.pullback_singleton

added inductive CategoryTheory.Presieve.singleton'

added theorem CategoryTheory.Presieve.singleton.mk

added def CategoryTheory.Presieve.singleton

added theorem CategoryTheory.Presieve.singleton_eq_iff_domain

added theorem CategoryTheory.Presieve.singleton_self

added def CategoryTheory.Presieve

added theorem CategoryTheory.Sieve.arrows_ext

added def CategoryTheory.Sieve.bind

added def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion

added def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion

added def CategoryTheory.Sieve.functor

added def CategoryTheory.Sieve.functorInclusion

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_id

added theorem CategoryTheory.Sieve.functorPullback_inter

added theorem CategoryTheory.Sieve.functorPullback_monotone

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_extend_eq

added theorem CategoryTheory.Sieve.functorPushforward_id

added theorem CategoryTheory.Sieve.functorPushforward_monotone

added theorem CategoryTheory.Sieve.functorPushforward_top

added theorem CategoryTheory.Sieve.functorPushforward_union

added theorem CategoryTheory.Sieve.functor_galoisConnection

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_of_contains_isSplitEpi

added theorem CategoryTheory.Sieve.generate_of_singleton_isSplitEpi

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.image_mem_functorPushforward

added theorem CategoryTheory.Sieve.infₛ_apply

added theorem CategoryTheory.Sieve.inter_apply

added theorem CategoryTheory.Sieve.le_functorPushforward_pullback

added theorem CategoryTheory.Sieve.le_generate

added theorem CategoryTheory.Sieve.le_pullback_bind

added theorem CategoryTheory.Sieve.le_pushforward_pullback

added def CategoryTheory.Sieve.natTransOfLe

added theorem CategoryTheory.Sieve.natTransOfLe_comm

added def CategoryTheory.Sieve.pullback

added theorem CategoryTheory.Sieve.pullbackArrows_comm

added theorem CategoryTheory.Sieve.pullback_comp

added theorem CategoryTheory.Sieve.pullback_eq_top_iff_mem

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_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_comp

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.sets_iff_generate

added def CategoryTheory.Sieve.sieveOfSubfunctor

added theorem CategoryTheory.Sieve.sieveOfSubfunctor_functorInclusion

added theorem CategoryTheory.Sieve.supₛ_apply

added theorem CategoryTheory.Sieve.top_apply

added theorem CategoryTheory.Sieve.union_apply

added structure CategoryTheory.Sieve