Commit 2020-10-21 01:39 3a860cc4View on Github →
fixup(category_theory/sites): add arrow sets that aren't sieves (#4703) Broken off from #4648.
- I realised that by creating a type
arrows_with_codomainI can avoid using
set (over X)entirely (the bit I was missing was that
derive complete_latticeworks on the new type even though it wasn't inferred on the pi-type), so I changed sieves to use that instead.
- I added constructors for special arrow sets. The definitions of
pullback_arrowslook a bit dubious because of the equality and
eq_to_homstuff; I don't love that either so if there's a suggestion on how to achieve the same things (in particular stating (1) and (3) from: https://stacks.math.columbia.edu/tag/00VH, as well as a complete lattice structure) I'd be happy to consider.
- I added a coercion so we can write
S finstead of
S.arrows ffor sieves.
modified theorem category_theory.grothendieck_topology.arrow_max
added theorem category_theory.grothendieck_topology.bind_covering
modified theorem category_theory.grothendieck_topology.dense_covering
added theorem category_theory.grothendieck_topology.ext
added theorem category_theory.arrows_with_codomain.bind_comp
added def category_theory.arrows_with_codomain
added def category_theory.sieve.bind
added theorem category_theory.sieve.downward_closed
modified def category_theory.sieve.generate
deleted inductive category_theory.sieve.generate_sets
modified def category_theory.sieve.gi_generate
modified theorem category_theory.sieve.id_mem_iff_eq_top
added theorem category_theory.sieve.le_pullback_bind
added theorem category_theory.sieve.mem_generate
modified theorem category_theory.sieve.mem_pushforward_of_comp
modified theorem category_theory.sieve.mem_top
modified theorem category_theory.sieve.pullback_eq_top_iff_mem
modified theorem category_theory.sieve.pullback_eq_top_of_mem
added theorem category_theory.sieve.pushforward_le_bind_of_mem
deleted def category_theory.sieve.set_over
modified theorem category_theory.sieve.sets_iff_generate