Mathlib Changelog
Changelog
About
Github
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