Commit 2020-10-29 14:18 7d7e850b

View on Github →

chore(category_theory/sites): nicer names (#4816) Changes the name arrows_with_codomain to presieve which is more suggestive and shorter, and changes singleton_arrow to singleton, since it's in the presieve namespace anyway.

Estimated changes

Modified src/category_theory/sites/pretopology.lean

modified def category_theory.pullback_arrows

Modified src/category_theory/sites/sieves.lean

deleted def category_theory.arrows_with_codomain.bind

deleted theorem category_theory.arrows_with_codomain.bind_comp

deleted def category_theory.arrows_with_codomain.singleton_arrow

deleted theorem category_theory.arrows_with_codomain.singleton_arrow_eq_iff_domain

deleted theorem category_theory.arrows_with_codomain.singleton_arrow_self

deleted def category_theory.arrows_with_codomain

added def category_theory.presieve.bind

added theorem category_theory.presieve.bind_comp

added def category_theory.presieve.singleton

added theorem category_theory.presieve.singleton_arrow_self

added theorem category_theory.presieve.singleton_eq_iff_domain

added def category_theory.presieve

modified def category_theory.sieve.bind

modified def category_theory.sieve.generate

modified def category_theory.sieve.gi_generate

modified theorem category_theory.sieve.le_pullback_bind

modified theorem category_theory.sieve.mem_generate

modified theorem category_theory.sieve.pushforward_le_bind_of_mem

modified theorem category_theory.sieve.sets_iff_generate