Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-16 19:33 af5c45db

View on Github →

feat(algebraic_geometry): Restriction of morphisms onto open sets of the target (#14972)

Estimated changes

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.Scheme.open_cover.add

added def algebraic_geometry.Scheme.open_cover.inter

added def algebraic_geometry.Scheme.restrict_functor

added def algebraic_geometry.Scheme.restrict_map_iso

added theorem algebraic_geometry.image_morphism_restrict_preimage

added theorem algebraic_geometry.is_open_immersion.range_pullback_fst_of_right

added theorem algebraic_geometry.is_open_immersion.range_pullback_snd_of_left

added theorem algebraic_geometry.is_open_immersion.range_pullback_to_base_of_left

added theorem algebraic_geometry.is_open_immersion.range_pullback_to_base_of_right

added def algebraic_geometry.morphism_restrict

added theorem algebraic_geometry.morphism_restrict_base_coe

added theorem algebraic_geometry.morphism_restrict_c_app

added theorem algebraic_geometry.morphism_restrict_comp

added theorem algebraic_geometry.morphism_restrict_ι

added def algebraic_geometry.pullback_restrict_iso_restrict

added theorem algebraic_geometry.pullback_restrict_iso_restrict_hom_morphism_restrict

added theorem algebraic_geometry.pullback_restrict_iso_restrict_hom_restrict

added theorem algebraic_geometry.pullback_restrict_iso_restrict_inv_fst

added theorem algebraic_geometry.Γ_map_morphism_restrict