Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 11:47 8b80cafb

View on Github →

feat(topology/sheaves): Localization of a sheaf. (#15331)

Estimated changes

Modified src/algebra/category/Ring/instances.lean

added theorem is_localization.epi

Created src/topology/sheaves/operations.lean

added def Top.presheaf.submonoid_presheaf.localization_presheaf

added def Top.presheaf.submonoid_presheaf.to_localization_presheaf

added structure Top.presheaf.submonoid_presheaf

added def Top.presheaf.submonoid_presheaf_of_stalk

added def Top.presheaf.to_total_quotient_presheaf

added def Top.presheaf.total_quotient_presheaf