Commit 2020-09-26 06:09 7aef1505

View on Github →

feat(category_theory): sieves (#3909) Define sieves, from my topos project. Co-authored by @EdAyers. These definitions and lemmas have been battle-tested quite a bit so I'm reasonably confident they're workable.

Estimated changes

Created src/category_theory/sites/sieves.lean

added theorem category_theory.sieve.arrows_ext

added def category_theory.sieve.functor

added def category_theory.sieve.functor_inclusion

added def category_theory.sieve.galois_coinsertion_of_mono

added theorem category_theory.sieve.galois_connection

added def category_theory.sieve.galois_insertion_of_split_epi

added def category_theory.sieve.generate

added inductive category_theory.sieve.generate_sets

added def category_theory.sieve.gi_generate

added theorem category_theory.sieve.id_mem_iff_eq_top

added theorem category_theory.sieve.le_pushforward_pullback

added theorem category_theory.sieve.mem_Inf

added theorem category_theory.sieve.mem_Sup

added theorem category_theory.sieve.mem_inter

added theorem category_theory.sieve.mem_pullback

added theorem category_theory.sieve.mem_pushforward_of_comp

added theorem category_theory.sieve.mem_top

added theorem category_theory.sieve.mem_union

added def category_theory.sieve.nat_trans_of_le

added theorem category_theory.sieve.nat_trans_of_le_comm

added def category_theory.sieve.pullback

added theorem category_theory.sieve.pullback_comp

added theorem category_theory.sieve.pullback_eq_top_iff_mem

added theorem category_theory.sieve.pullback_inter

added theorem category_theory.sieve.pullback_monotone

added theorem category_theory.sieve.pullback_pushforward_le

added theorem category_theory.sieve.pullback_top

added def category_theory.sieve.pushforward

added theorem category_theory.sieve.pushforward_comp

added theorem category_theory.sieve.pushforward_monotone

added theorem category_theory.sieve.pushforward_union

added def category_theory.sieve.set_over

added theorem category_theory.sieve.sets_iff_generate

added structure category_theory.sieve