Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 05:50 af80234d

View on Github →

feat(algebraic_geometry/morphisms/basic): Basic framework for local properties of morphisms. (#15709)

Estimated changes

Modified src/algebraic_geometry/morphisms/basic.lean

added theorem algebraic_geometry.affine_cancel_left_is_iso

added theorem algebraic_geometry.affine_cancel_right_is_iso

added theorem algebraic_geometry.affine_target_morphism_property.is_local.affine_open_cover_iff

added theorem algebraic_geometry.affine_target_morphism_property.is_local.affine_open_cover_tfae

added theorem algebraic_geometry.affine_target_morphism_property.is_local.affine_target_iff

added theorem algebraic_geometry.affine_target_morphism_property.is_local.open_cover_iff

added theorem algebraic_geometry.affine_target_morphism_property.is_local.target_affine_locally_is_local

added structure algebraic_geometry.affine_target_morphism_property.is_local

added theorem algebraic_geometry.affine_target_morphism_property.is_local_of_open_cover_imply

added theorem algebraic_geometry.is_affine_open.map_is_iso

added theorem algebraic_geometry.property_is_local_at_target.open_cover_tfae

added structure algebraic_geometry.property_is_local_at_target

added def algebraic_geometry.target_affine_locally

added theorem algebraic_geometry.target_affine_locally_of_open_cover

added theorem algebraic_geometry.target_affine_locally_respects_iso