Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-13 13:20 6ea59e36

View on Github →

feat(category_theory/sites/sieves): Added functor pushforward (#9647) Defined sieve.functor_pushforward. Proved that sieve.functor_pushforward and sieve.functor_pullback forms a Galois connection. Provided some lemmas about sieve.functor_pushforward, sieve.functor_pullback regarding the lattice structure.

Estimated changes

Modified src/category_theory/sites/sieves.lean

modified def category_theory.presieve.functor_pullback

modified theorem category_theory.presieve.functor_pullback_id

modified theorem category_theory.presieve.functor_pullback_mem

added def category_theory.presieve.functor_pushforward

added theorem category_theory.presieve.functor_pushforward_comp

added theorem category_theory.presieve.image_mem_functor_pushforward

added def category_theory.sieve.ess_surj_full_functor_galois_insertion

added def category_theory.sieve.fully_faithful_functor_galois_coinsertion

added theorem category_theory.sieve.functor_galois_connection

modified def category_theory.sieve.functor_pullback

added theorem category_theory.sieve.functor_pullback_arrows

added theorem category_theory.sieve.functor_pullback_bot

added theorem category_theory.sieve.functor_pullback_comp

modified theorem category_theory.sieve.functor_pullback_id

added theorem category_theory.sieve.functor_pullback_inter

added theorem category_theory.sieve.functor_pullback_monotone

added theorem category_theory.sieve.functor_pullback_pushforward_le

added theorem category_theory.sieve.functor_pullback_top

added theorem category_theory.sieve.functor_pullback_union

added def category_theory.sieve.functor_pushforward

added theorem category_theory.sieve.functor_pushforward_bot

added theorem category_theory.sieve.functor_pushforward_comp

added theorem category_theory.sieve.functor_pushforward_extend_eq

added theorem category_theory.sieve.functor_pushforward_id

added theorem category_theory.sieve.functor_pushforward_monotone

added theorem category_theory.sieve.functor_pushforward_union

added theorem category_theory.sieve.image_mem_functor_pushforward

added theorem category_theory.sieve.le_functor_pushforward_pullback