Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 19:05 d8c87253

View on Github →

feat(ring_theory,algebraic_geometry): Miscellaneous lemmas/def/typo corrections (#10307) Split out from #9802 since I'm aiming at more general version.

Estimated changes

Modified src/algebraic_geometry/locally_ringed_space.lean

Modified src/algebraic_geometry/prime_spectrum/basic.lean

added def local_ring.closed_point

added theorem local_ring.local_hom_iff_comap_closed_point

added theorem prime_spectrum.is_basis_basic_opens

Modified src/algebraic_geometry/structure_sheaf.lean

Modified src/category_theory/sites/sheaf_of_types.lean

Modified src/category_theory/structured_arrow.lean

Modified src/ring_theory/ideal/local_ring.lean

added theorem local_ring.local_hom_tfae

Modified src/ring_theory/localization.lean

added theorem is_localization.iso_comp

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

added theorem Top.opens.cover_dense_iff_is_basis

added theorem Top.opens.cover_dense_induced_functor

added theorem Top.sheaf.extend_hom_app

added theorem Top.sheaf.hom_ext

added def Top.sheaf.restrict_hom_equiv_hom