Commit 2021-06-02 04:57 21641075

View on Github →

refactor(algebraic_geometry/structure_sheaf): Rename Spec.Top to prime_spectrum.Top (#7786) Renames Spec.Top to prime_specturm.Top to free up the namespace for the Spec functor.

Estimated changes

Modified src/algebraic_geometry/structure_sheaf.lean

deleted def algebraic_geometry.Spec.Top

modified theorem algebraic_geometry.coe_open_to_localization

modified def algebraic_geometry.const

modified theorem algebraic_geometry.const_apply'

modified theorem algebraic_geometry.const_apply

modified theorem algebraic_geometry.exists_const

modified theorem algebraic_geometry.germ_comp_stalk_to_fiber_ring_hom

modified theorem algebraic_geometry.germ_to_open

modified theorem algebraic_geometry.germ_to_top

modified theorem algebraic_geometry.is_unit_to_stalk

modified def algebraic_geometry.localization_to_stalk

modified theorem algebraic_geometry.localization_to_stalk_mk'

modified theorem algebraic_geometry.localization_to_stalk_of

modified theorem algebraic_geometry.locally_const_basic_open

modified theorem algebraic_geometry.normalize_finite_fraction_representation

modified def algebraic_geometry.open_to_localization

modified theorem algebraic_geometry.open_to_localization_apply

added def algebraic_geometry.prime_spectrum.Top

modified theorem algebraic_geometry.res_apply

modified def algebraic_geometry.stalk_iso

modified def algebraic_geometry.stalk_to_fiber_ring_hom

modified theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ'

modified theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ

modified theorem algebraic_geometry.stalk_to_fiber_ring_hom_to_stalk

modified def algebraic_geometry.structure_presheaf_in_CommRing

modified def algebraic_geometry.structure_sheaf.is_fraction

modified def algebraic_geometry.structure_sheaf.localizations

modified def algebraic_geometry.structure_sheaf.sections_subring

modified def algebraic_geometry.structure_sheaf

modified def algebraic_geometry.structure_sheaf_in_Type

modified def algebraic_geometry.to_basic_open

modified def algebraic_geometry.to_open

modified theorem algebraic_geometry.to_open_apply

modified theorem algebraic_geometry.to_open_eq_const

modified theorem algebraic_geometry.to_open_germ

modified theorem algebraic_geometry.to_open_res

modified def algebraic_geometry.to_stalk

modified theorem algebraic_geometry.to_stalk_comp_stalk_to_fiber_ring_hom