Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-30 14:55 64fdfc74

View on Github →

feat(category_theory/sites): construct a presieve from an indexed family of arrows (#7413) For the LTE: alternate constructors for presieves which can be more convenient.

Estimated changes

Modified src/category_theory/sites/pretopology.lean

deleted inductive category_theory.pullback_arrows

deleted theorem category_theory.pullback_arrows_comm

deleted theorem category_theory.pullback_singleton

Modified src/category_theory/sites/sieves.lean

added inductive category_theory.presieve.of_arrows

added theorem category_theory.presieve.of_arrows_bind

added theorem category_theory.presieve.of_arrows_pullback

added theorem category_theory.presieve.of_arrows_punit

added inductive category_theory.presieve.pullback_arrows

added theorem category_theory.presieve.pullback_singleton

added theorem category_theory.sieve.pullback_arrows_comm

Modified src/category_theory/sites/spaces.lean