Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-17 19:34 ce566b31

View on Github →

feat(algebraic_geometry/morphisms): Construct morphism properties from ring homomorphism properties (#16059)

Estimated changes

Modified src/algebraic_geometry/morphisms/ring_hom_properties.lean

added theorem algebraic_geometry.Scheme_restrict_basic_open_of_localization_preserves

added def algebraic_geometry.affine_locally

added theorem algebraic_geometry.affine_locally_iff_affine_opens_le

added theorem algebraic_geometry.affine_locally_respects_iso

added theorem algebraic_geometry.is_open_immersion_comp_of_source_affine_locally

added def algebraic_geometry.source_affine_locally

added theorem algebraic_geometry.source_affine_locally_is_local

added theorem algebraic_geometry.source_affine_locally_of_source_open_cover_aux

added theorem algebraic_geometry.source_affine_locally_respects_iso

added theorem ring_hom.property_is_local.affine_locally_of_is_open_immersion

added theorem ring_hom.property_is_local.affine_locally_stable_under_composition

added theorem ring_hom.property_is_local.affine_open_cover_iff

added theorem ring_hom.property_is_local.affine_open_cover_tfae

added theorem ring_hom.property_is_local.is_local_affine_locally

added theorem ring_hom.property_is_local.is_local_source_affine_locally

added theorem ring_hom.property_is_local.open_cover_tfae

added theorem ring_hom.property_is_local.source_affine_locally_comp_of_is_open_immersion

added theorem ring_hom.property_is_local.source_affine_locally_of_source_open_cover

added theorem ring_hom.property_is_local.source_affine_open_cover_iff

added theorem ring_hom.property_is_local.source_open_cover_iff