Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-04 09:44 03872fdd

View on Github →

feat(*): Prerequisites for the Spec gamma adjunction (#11209)

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

added theorem algebraic_geometry.Scheme.forget_to_LocallyRingedSpace_preimage

Modified src/algebraic_geometry/Spec.lean

added theorem algebraic_geometry.Spec.basic_open_hom_ext

Modified src/algebraic_geometry/locally_ringed_space.lean

added theorem algebraic_geometry.LocallyRingedSpace.comp_val_c

added theorem algebraic_geometry.LocallyRingedSpace.comp_val_c_app

Modified src/algebraic_geometry/prime_spectrum/basic.lean

added theorem local_ring.comap_closed_point

added theorem local_ring.is_local_ring_hom_iff_comap_closed_point

deleted theorem local_ring.local_hom_iff_comap_closed_point

added theorem prime_spectrum.comap_comp_apply

Modified src/algebraic_geometry/ringed_space.lean

added theorem algebraic_geometry.RingedSpace.mem_top_basic_open

Modified src/algebraic_geometry/stalks.lean

modified def algebraic_geometry.PresheafedSpace.stalk

Modified src/algebraic_geometry/structure_sheaf.lean

added theorem algebraic_geometry.structure_sheaf.is_localization.to_basic_open

added theorem algebraic_geometry.structure_sheaf.is_localization.to_stalk

Modified src/category_theory/adjunction/basic.lean

added theorem category_theory.adjunction.hom_equiv_id

added theorem category_theory.adjunction.hom_equiv_symm_id

Modified src/topology/sheaves/presheaf.lean

added theorem Top.presheaf.pushforward_eq'_hom_app

added theorem Top.presheaf.pushforward_map_app'