Commit 2020-09-07 05:46 94b96cff

View on Github →

feat(algebraic_geometry/structure_sheaf): stalk_iso (#4047) Given a ring R and a prime ideal p, construct an isomorphism of rings between the stalk of the structure sheaf of R at p and the localization of R at p.

Estimated changes

Modified src/algebraic_geometry/prime_spectrum.lean

modified def prime_spectrum.basic_open

deleted theorem prime_spectrum.basic_open_open

Modified src/algebraic_geometry/structure_sheaf.lean

added theorem algebraic_geometry.coe_open_to_localization

added def algebraic_geometry.const

added theorem algebraic_geometry.const_add

added theorem algebraic_geometry.const_apply'

added theorem algebraic_geometry.const_apply

added theorem algebraic_geometry.const_congr

added theorem algebraic_geometry.const_ext

added theorem algebraic_geometry.const_mul

added theorem algebraic_geometry.const_mul_cancel'

added theorem algebraic_geometry.const_mul_cancel

added theorem algebraic_geometry.const_mul_rev

added theorem algebraic_geometry.const_one

added theorem algebraic_geometry.const_self

added theorem algebraic_geometry.const_zero

added theorem algebraic_geometry.exists_const

added theorem algebraic_geometry.germ_comp_stalk_to_fiber_ring_hom

added theorem algebraic_geometry.germ_to_open

added theorem algebraic_geometry.germ_to_top

added theorem algebraic_geometry.is_unit_to_basic_open_self

added theorem algebraic_geometry.is_unit_to_stalk

added theorem algebraic_geometry.localization_to_basic_open

added def algebraic_geometry.localization_to_stalk

added theorem algebraic_geometry.localization_to_stalk_mk'

added theorem algebraic_geometry.localization_to_stalk_of

added def algebraic_geometry.open_to_localization

added theorem algebraic_geometry.open_to_localization_apply

added theorem algebraic_geometry.res_apply

added theorem algebraic_geometry.res_const'

added theorem algebraic_geometry.res_const

modified def algebraic_geometry.stalk_iso

modified def algebraic_geometry.stalk_to_fiber_ring_hom

added theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ'

added theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ

added theorem algebraic_geometry.stalk_to_fiber_ring_hom_to_stalk

added def algebraic_geometry.to_basic_open

added theorem algebraic_geometry.to_basic_open_mk'

added theorem algebraic_geometry.to_basic_open_to_map

added def algebraic_geometry.to_open

added theorem algebraic_geometry.to_open_apply

added theorem algebraic_geometry.to_open_eq_const

added theorem algebraic_geometry.to_open_germ

added theorem algebraic_geometry.to_open_res

added def algebraic_geometry.to_stalk

added theorem algebraic_geometry.to_stalk_comp_stalk_to_fiber_ring_hom

Modified src/topology/sheaves/stalks.lean

added theorem Top.presheaf.germ_ext

added theorem Top.presheaf.stalk_hom_ext