Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-04 16:20 13361559

View on Github →

chore(topology/sheaves/*): universe generalizations (#19153) Necessary but sadly insufficient for the request at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2319146.20sheaves.20on.20manifolds

Estimated changes

Modified src/algebraic_geometry/morphisms/quasi_compact.lean

modified theorem algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact

Modified src/algebraic_geometry/morphisms/quasi_separated.lean

modified theorem algebraic_geometry.exists_eq_pow_mul_of_is_compact_of_is_quasi_separated

Modified src/algebraic_geometry/ringed_space.lean

Modified src/algebraic_geometry/structure_sheaf.lean

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

added theorem category_theory.limits.types.pi_lift_π_apply'

added theorem category_theory.limits.types.pi_map_π_apply'

modified theorem category_theory.limits.types.pi_map_π_apply

Modified src/topology/sheaves/forget.lean

modified def Top.presheaf.sheaf_condition.map_cone_fork

Modified src/topology/sheaves/local_predicate.lean

modified def Top.continuous_prelocal

modified def Top.stalk_to_fiber

modified theorem Top.stalk_to_fiber_germ

modified theorem Top.stalk_to_fiber_injective

modified theorem Top.stalk_to_fiber_surjective

modified def Top.subpresheaf_to_Types

modified def Top.subsheaf_to_Types

Modified src/topology/sheaves/presheaf.lean

modified def Top.presheaf.pullback

modified def Top.presheaf.pullback_hom_iso_pushforward_inv

modified def Top.presheaf.pullback_inv_iso_pushforward_hom

modified def Top.presheaf.pullback_map

modified def Top.presheaf.pullback_obj

modified def Top.presheaf.pullback_obj_obj_of_image_open

modified def Top.presheaf.pushforward_pullback_adjunction

Modified src/topology/sheaves/presheaf_of_functions.lean

modified def Top.presheaf_to_Type

modified def Top.presheaf_to_Types

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

Modified src/topology/sheaves/sheaf_of_functions.lean

modified def Top.sheaf_to_Type

modified def Top.sheaf_to_Types

Modified src/topology/sheaves/stalks.lean