Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-28 03:16 7e6393f8

View on Github →

feat(topology/sheaves): the sheaf condition for functions satisfying a local predicate (#3906) Functions satisfying a local predicate form a sheaf. This sheaf has a natural map from the stalk to the original fiber, and we give conditions for this map to be injective or surjective.

Estimated changes

Modified src/category_theory/limits/shapes/equalizers.lean

added def category_theory.limits.cofork.ext

added def category_theory.limits.fork.ext

Modified src/category_theory/limits/shapes/products.lean

added def category_theory.limits.pi.map_iso

added def category_theory.limits.sigma.map_iso

Modified src/data/set/basic.lean

added theorem set.inclusion_right

Modified src/topology/category/Top/open_nhds.lean

modified def topological_space.open_nhds.inclusion

modified theorem topological_space.open_nhds.inclusion_obj

modified def topological_space.open_nhds

Created src/topology/sheaves/local_predicate.lean

added def Top.continuous_local

added def Top.continuous_prelocal

added structure Top.local_predicate

added def Top.prelocal_predicate.sheafify

added structure Top.prelocal_predicate

added def Top.sheaf_to_Top

added def Top.stalk_to_fiber

added theorem Top.stalk_to_fiber_germ

added theorem Top.stalk_to_fiber_injective

added theorem Top.stalk_to_fiber_surjective

added def Top.subpresheaf_continuous_prelocal_iso_presheaf_to_Top

added def Top.subpresheaf_to_Types.diagram_subtype

added def Top.subpresheaf_to_Types.sheaf_condition

added def Top.subpresheaf_to_Types.subtype

added def Top.subpresheaf_to_Types

added def Top.subsheaf_to_Types

Modified src/topology/sheaves/presheaf_of_functions.lean

added theorem Top.presheaf_to_Top_obj

modified def Top.presheaf_to_Types

added theorem Top.presheaf_to_Types_map

added theorem Top.presheaf_to_Types_obj

Modified src/topology/sheaves/sheaf.lean

added def Top.sheaf_condition.diagram.iso_of_iso

added def Top.sheaf_condition.fork.iso_of_iso

added def Top.sheaf_condition.pi_inters.iso_of_iso

added def Top.sheaf_condition.pi_opens.iso_of_iso

added def Top.sheaf_condition_equiv_of_iso

Modified src/topology/sheaves/sheaf_of_functions.lean

deleted def Top.sheaf_condition.forget_continuity

deleted def Top.sheaf_condition.to_Top

added def Top.sheaf_to_Type

added def Top.sheaf_to_Types

Modified src/topology/sheaves/stalks.lean

added def Top.presheaf.germ

added theorem Top.presheaf.germ_res

added theorem Top.presheaf.germ_res_apply

modified theorem Top.presheaf.stalk_functor_obj