Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-07 20:10 64fc7238

View on Github →

feat(algebraic_geometry/morphisms/finite_type): Morphisms locally of finite type. (#16124)

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

added def algebraic_geometry.Scheme.hom.app_le

Created src/algebraic_geometry/morphisms/finite_type.lean

added theorem algebraic_geometry.locally_of_finite_type.affine_open_cover_iff

added theorem algebraic_geometry.locally_of_finite_type.open_cover_iff

added theorem algebraic_geometry.locally_of_finite_type.source_open_cover_iff

added theorem algebraic_geometry.locally_of_finite_type_eq

added theorem algebraic_geometry.locally_of_finite_type_of_comp

added theorem algebraic_geometry.locally_of_finite_type_respects_iso

added theorem algebraic_geometry.locally_of_finite_type_stable_under_composition

Modified src/algebraic_geometry/morphisms/ring_hom_properties.lean

added theorem ring_hom.property_is_local.affine_locally_of_comp

Modified src/ring_theory/ring_hom/finite_type.lean

deleted theorem ring_hom.finite_is_local

added theorem ring_hom.finite_type_is_local

added theorem ring_hom.finite_type_respects_iso