Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 16:28 9b3fec55

View on Github →

feat(algebraic_geometry): Gamma-Spec adjunction (#9802) Define the adjunction between the functors Gamma (global sections) and Spec (to LocallyRingedSpace). I'm currently working on a more general version in http://arxiv.org/pdf/1103.2139.pdf (Theorem 2), which may require refactoring structure_sheaf and Spec.

Estimated changes

Created src/algebraic_geometry/Gamma_Spec_adjunction.lean

added theorem algebraic_geometry.LocallyRingedSpace.comp_ring_hom_ext

added theorem algebraic_geometry.LocallyRingedSpace.is_unit_res_to_Γ_Spec_map_basic_open

added theorem algebraic_geometry.LocallyRingedSpace.not_mem_prime_iff_unit_in_stalk

added theorem algebraic_geometry.LocallyRingedSpace.to_stalk_stalk_map_to_Γ_Spec

added def algebraic_geometry.LocallyRingedSpace.to_to_Γ_Spec_map_basic_open

added def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec

added def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace

added theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace_app_eq

added theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_SheafedSpace_app_spec

added def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_base

added def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_c_app

added theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_c_app_iff

added theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_c_app_spec

added def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_c_basic_opens

added theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_continuous

added def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_fun

added def algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_map_basic_open

added theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_map_basic_open_eq

added theorem algebraic_geometry.LocallyRingedSpace.to_Γ_Spec_preim_basic_open_eq

added theorem algebraic_geometry.LocallyRingedSpace.Γ_Spec_left_triangle

added def algebraic_geometry.LocallyRingedSpace.Γ_to_stalk

added def algebraic_geometry.identity_to_Γ_Spec

added def algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction

added def algebraic_geometry.Γ_Spec.adjunction

added theorem algebraic_geometry.Γ_Spec.adjunction_counit_app

added theorem algebraic_geometry.Γ_Spec.adjunction_hom_equiv

added theorem algebraic_geometry.Γ_Spec.adjunction_hom_equiv_apply

added theorem algebraic_geometry.Γ_Spec.adjunction_hom_equiv_symm_apply

added theorem algebraic_geometry.Γ_Spec.adjunction_unit_app

added theorem algebraic_geometry.Γ_Spec.left_triangle

added theorem algebraic_geometry.Γ_Spec.right_triangle

Modified src/algebraic_geometry/Spec.lean

Modified src/algebraic_geometry/structure_sheaf.lean

deleted theorem algebraic_geometry.structure_sheaf.is_localization.to_basic_open

deleted theorem algebraic_geometry.structure_sheaf.is_localization.to_stalk

added theorem algebraic_geometry.structure_sheaf.open_algebra_map

added theorem algebraic_geometry.structure_sheaf.stalk_algebra_map