Commit 2021-10-11 07:59 1539ee18

View on Github →

refactor(topology/sheaves/*): Make sheaf condition a Prop (#9607) Make sheaf_condition into a Prop and redefine the type of sheaves on a topological space X as a subtype of (opens X)ᵒᵖ ⥤ C.

Estimated changes

Modified src/algebraic_geometry/Spec.lean

Modified src/algebraic_geometry/locally_ringed_space.lean

added def algebraic_geometry.LocallyRingedSpace.restrict

added def algebraic_geometry.LocallyRingedSpace.restrict_top_iso

Modified src/algebraic_geometry/sheafed_space.lean

modified def algebraic_geometry.SheafedSpace.sheaf

Modified src/algebraic_geometry/structure_sheaf.lean

modified def algebraic_geometry.structure_sheaf.basic_open_iso

modified theorem algebraic_geometry.structure_sheaf.exists_const

modified def algebraic_geometry.structure_sheaf.global_sections_iso

modified def algebraic_geometry.structure_sheaf.to_stalk

Modified src/topology/sheaves/forget.lean

added theorem Top.presheaf.is_sheaf_iff_is_sheaf_comp

deleted def Top.presheaf.sheaf_condition_equiv_sheaf_condition_comp

Modified src/topology/sheaves/local_predicate.lean

added theorem Top.subpresheaf_to_Types.is_sheaf

deleted def Top.subpresheaf_to_Types.sheaf_condition

Modified src/topology/sheaves/sheaf.lean

added def Top.presheaf.is_sheaf

added theorem Top.presheaf.is_sheaf_iso_iff

added theorem Top.presheaf.is_sheaf_of_iso

added theorem Top.presheaf.is_sheaf_punit

deleted def Top.presheaf.sheaf_condition

deleted def Top.presheaf.sheaf_condition_equiv_of_iso

deleted def Top.presheaf.sheaf_condition_punit

modified def Top.sheaf.forget

added def Top.sheaf

deleted structure Top.sheaf

Modified src/topology/sheaves/sheaf_condition/opens_le_cover.lean

added theorem Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover

added def Top.presheaf.is_sheaf_opens_le_cover

added theorem Top.presheaf.is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections

deleted def Top.presheaf.sheaf_condition_equiv_sheaf_condition_opens_le_cover

deleted def Top.presheaf.sheaf_condition_opens_le_cover

deleted def Top.presheaf.sheaf_condition_opens_le_cover_equiv_sheaf_condition_pairwise_intersections

Modified src/topology/sheaves/sheaf_condition/pairwise_intersections.lean

added theorem Top.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections

added theorem Top.presheaf.is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections

added def Top.presheaf.is_sheaf_pairwise_intersections

added def Top.presheaf.is_sheaf_preserves_limit_pairwise_intersections

deleted def Top.presheaf.sheaf_condition_equiv_sheaf_condition_pairwise_intersections

deleted def Top.presheaf.sheaf_condition_equiv_sheaf_condition_preserves_limit_pairwise_intersections

deleted def Top.presheaf.sheaf_condition_pairwise_intersections

deleted def Top.presheaf.sheaf_condition_preserves_limit_pairwise_intersections

Modified src/topology/sheaves/sheaf_condition/unique_gluing.lean

deleted def Top.presheaf.gluing

added theorem Top.presheaf.is_sheaf_iff_is_sheaf_unique_gluing

added theorem Top.presheaf.is_sheaf_iff_is_sheaf_unique_gluing_types

added theorem Top.presheaf.is_sheaf_of_is_sheaf_unique_gluing_types

added def Top.presheaf.is_sheaf_unique_gluing

added theorem Top.presheaf.is_sheaf_unique_gluing_of_is_sheaf_types

deleted def Top.presheaf.sheaf_condition_equiv_sheaf_condition_unique_gluing

deleted def Top.presheaf.sheaf_condition_equiv_sheaf_condition_unique_gluing_types

deleted def Top.presheaf.sheaf_condition_of_exists_unique_gluing

deleted def Top.presheaf.sheaf_condition_of_sheaf_condition_unique_gluing_types

deleted def Top.presheaf.sheaf_condition_unique_gluing

deleted def Top.presheaf.sheaf_condition_unique_gluing_of_sheaf_condition_types

modified theorem Top.sheaf.eq_of_locally_eq

modified theorem Top.sheaf.exists_unique_gluing

Modified src/topology/sheaves/sheaf_of_functions.lean

deleted def Top.presheaf.to_Type

added theorem Top.presheaf.to_Type_is_sheaf

deleted def Top.presheaf.to_Types

added theorem Top.presheaf.to_Types_is_sheaf

Modified src/topology/sheaves/sheafify.lean

modified def Top.presheaf.sheafify_stalk_iso

modified def Top.presheaf.stalk_to_fiber

modified def Top.presheaf.to_sheafify

Modified src/topology/sheaves/stalks.lean

modified theorem Top.presheaf.section_ext