Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-17 17:25 621cf7f2

View on Github →

feat(algebraic_geometry): Intersection of affine open can be covered by common basic opens (#11649)

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

added theorem algebraic_geometry.basic_open_basic_open_is_basic_open

added def algebraic_geometry.basic_open_sections_to_affine

added theorem algebraic_geometry.exists_basic_open_subset_affine_inter

added theorem algebraic_geometry.is_affine_open.exists_basic_open_subset

added theorem algebraic_geometry.is_affine_open.opens_map_from_Spec_basic_open

added theorem algebraic_geometry.is_localization_basic_open

Modified src/algebraic_geometry/open_immersion.lean

modified theorem algebraic_geometry.PresheafedSpace.is_open_immersion.inv_app_app

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.is_iso_of_subset

added theorem algebraic_geometry.PresheafedSpace.is_open_immersion.of_restrict_inv_app

added theorem algebraic_geometry.is_open_immersion.image_basic_open