Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-25 05:10 b351ad53

View on Github →

feat(algebraic_geometry/morphisms): Basic framework for classes of morphisms between schemes (#14944)

Estimated changes

Created src/algebraic_geometry/morphisms/basic.lean

added def algebraic_geometry.affine_target_morphism_property.to_property

added theorem algebraic_geometry.affine_target_morphism_property.to_property_apply

added def algebraic_geometry.affine_target_morphism_property

Modified src/category_theory/limits/shapes/pullbacks.lean

added def category_theory.limits.base_change

Created src/category_theory/morphism_property.lean

added theorem category_theory.morphism_property.respects_iso.cancel_left_is_iso

added theorem category_theory.morphism_property.respects_iso.cancel_right_is_iso

added def category_theory.morphism_property.respects_iso

added theorem category_theory.morphism_property.stable_under_base_change.base_change_map

added theorem category_theory.morphism_property.stable_under_base_change.base_change_obj

added theorem category_theory.morphism_property.stable_under_base_change.fst

added theorem category_theory.morphism_property.stable_under_base_change.pullback_map

added theorem category_theory.morphism_property.stable_under_base_change.snd

added def category_theory.morphism_property.stable_under_base_change

added theorem category_theory.morphism_property.stable_under_composition.respects_iso

added def category_theory.morphism_property.stable_under_composition

added def category_theory.morphism_property