Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-14 21:29 323e388c

View on Github →

feat(algebraic_geometry): More lemmas about affine schemes and basic open sets (#11449)

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

added theorem algebraic_geometry.Scheme.Spec_map_presheaf_map_eq_to_hom

added theorem algebraic_geometry.Scheme.map_prime_spectrum_basic_open_of_affine

added theorem algebraic_geometry.is_affine_open.Spec_Γ_identity_hom_app_from_Spec

added theorem algebraic_geometry.is_affine_open.basic_open_is_affine

added def algebraic_geometry.is_affine_open.from_Spec

added theorem algebraic_geometry.is_affine_open.from_Spec_app_eq

added theorem algebraic_geometry.is_affine_open.from_Spec_base_preimage

added theorem algebraic_geometry.is_affine_open.from_Spec_image_top

added theorem algebraic_geometry.is_affine_open.from_Spec_range

added theorem algebraic_geometry.is_affine_open.is_compact

added theorem algebraic_geometry.is_basis_basic_open

Modified src/algebraic_geometry/Scheme.lean

modified theorem algebraic_geometry.Scheme.basic_open_res

modified theorem algebraic_geometry.Scheme.basic_open_res_eq

added theorem algebraic_geometry.Scheme.basic_open_subset

added theorem algebraic_geometry.Scheme.comp_coe_base

added theorem algebraic_geometry.Scheme.comp_val

added theorem algebraic_geometry.Scheme.comp_val_base