Mathlib Changelog
Changelog
About
Github
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