Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 08:37 feaf6f5e

View on Github →

feat(algebraic_geometry): lemmas about basic opens in schemes (#11393)

Estimated changes

Modified src/algebraic_geometry/Gamma_Spec_adjunction.lean

added theorem algebraic_geometry.Γ_Spec.adjunction_unit_app_app_top

Modified src/algebraic_geometry/Scheme.lean

added def algebraic_geometry.Scheme.basic_open

added theorem algebraic_geometry.Scheme.basic_open_mul

added theorem algebraic_geometry.Scheme.basic_open_of_is_unit

added theorem algebraic_geometry.Scheme.basic_open_res

added theorem algebraic_geometry.Scheme.basic_open_res_eq

added theorem algebraic_geometry.Scheme.basic_open_zero

added theorem algebraic_geometry.Scheme.comp_val_c_app

added theorem algebraic_geometry.Scheme.congr_app

added theorem algebraic_geometry.Scheme.mem_basic_open

added theorem algebraic_geometry.Scheme.mem_basic_open_top

added theorem algebraic_geometry.Scheme.preimage_basic_open'

added theorem algebraic_geometry.Scheme.preimage_basic_open

added theorem algebraic_geometry.basic_open_eq_of_affine'

added theorem algebraic_geometry.basic_open_eq_of_affine

Modified src/algebraic_geometry/Spec.lean

modified def algebraic_geometry.Spec_Γ_identity

Modified src/algebraic_geometry/locally_ringed_space.lean

Modified src/algebraic_geometry/properties.lean

deleted theorem algebraic_geometry.basic_open_eq_of_affine'

deleted theorem algebraic_geometry.basic_open_eq_of_affine

Modified src/algebraic_geometry/ringed_space.lean

added theorem algebraic_geometry.RingedSpace.basic_open_mul

added theorem algebraic_geometry.RingedSpace.basic_open_of_is_unit

modified theorem algebraic_geometry.RingedSpace.basic_open_res

added theorem algebraic_geometry.RingedSpace.basic_open_res_eq

Modified src/algebraic_geometry/sheafed_space.lean

Modified src/topology/category/Top/opens.lean

added theorem topological_space.opens.inclusion_map_eq_top

added theorem topological_space.opens.open_embedding_obj_top