Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-05 12:41 7316286f

View on Github →

feat(algebraic_geometry/morphisms/basic): Morphism properties on the diagonal morphism. (#16111)

Estimated changes

Modified src/algebraic_geometry/morphisms/basic.lean

added def algebraic_geometry.affine_target_morphism_property.diagonal

added theorem algebraic_geometry.affine_target_morphism_property.diagonal_of_target_affine_locally

added theorem algebraic_geometry.affine_target_morphism_property.diagonal_respects_iso

added theorem algebraic_geometry.affine_target_morphism_property.is_local.diagonal

added theorem algebraic_geometry.affine_target_morphism_property.is_local.diagonal_affine_open_cover_tfae

added theorem algebraic_geometry.diagonal_target_affine_locally_eq_target_affine_locally

added theorem algebraic_geometry.diagonal_target_affine_locally_of_open_cover

Modified src/algebraic_geometry/pullbacks.lean

added def algebraic_geometry.Scheme.pullback.open_cover_of_left_right

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

added def category_theory.limits.pullback.map_desc

added theorem category_theory.limits.pullback.map_desc_comp

added def category_theory.limits.pushout.map_lift

added theorem category_theory.limits.pushout.map_lift_comp

Modified src/category_theory/morphism_property.lean

added def category_theory.morphism_property.diagonal

added theorem category_theory.morphism_property.diagonal_iff

added theorem category_theory.morphism_property.respects_iso.diagonal

added theorem category_theory.morphism_property.stable_under_base_change.diagonal

added theorem category_theory.morphism_property.stable_under_composition.diagonal