properties of ring homomorphisms

[jcommelin]

We should define a boatload of predicates on R ->+* S

There should be predicates on variable (P : ∀ {R S : Type u} [comm_ring R] [comm_ring S] (f : by exactI R →+* S), Prop) characterizing the following properties :

• [ ] P_of_surjective: surjective implies P
• [ ] P_of_bijective: bijective implies P
• [x] P_stable_under_composition: P is preserved under composition
• [x] P_stable_under_base_change: P is preserved under base change
• [x] localization_P: P holds for A →+* B if P holds for A →+* B_f for a generating family { f }. (in ring_theory/local_properties.lean)
• [x] P_of_localization_span: P holds for S⁻¹A →+* S⁻¹B if P holds for A →+* B. (in ring_theory/local_properties.lean)
• [ ] P_of_localization_maximal: P holds for A →+* B if P holds for A_m →+* B_m for all maximal ideal m of B.
• [ ] P_of_localization_prime: P holds for A →+* B if P holds for A_m →+* B_m for all prime ideal m of B.

Also some implications between these properties of properties

• [ ] localization_P + P_of_localization_prime -> P_of_localization_span
• [ ] P_of_localization_maximal -> P_of_localization_prime

The following ring properties should be covered :

• [ ] injective
  • [ ] localization_injective
  • [ ] injective_of_localization_maximal
• [ ] surjective
  • [x] localization_preserves_surjective
  • [x] surjective_of_localization_span
  • [ ] surjective_of_localization_maximal
• [ ] bijective/isomorphism
  • [ ] localization_bijective
  • [ ] bijective_of_localization_maximal
• [ ] exact-ness
  • [ ] localization_exact
  • [ ] exact_of_localization_maximal
• [x] finite
  • [x] finite_of_surjective
  • [x] finite_id (#4634)
  • [x] finite.comp (#4634)
  • [x] localization_finite
  • [x] finite_of_localization_span
  • [x] finite.base_change
• [x] of finite type
  • [x] finite_of_surjective
  • [x] finite_type_id (#4634)
  • [x] finite_type.comp (#4634)
  • [x] localization_finite_type
  • [x] finite_type_of_localization_span
  • [x] finite_type_of_localization_span_target
  • [x] finite_type_holds_for_localization_away
  • [x] finite_type.base_change
• [ ] of finite presentation
  • [x] finite_presentation_of_surjective
  • [x] finite_presentation_id
  • [x] finite_presentation.comp
  • [ ] localization_finite_presentation
  • [ ] finite_presentation_holds_for_localization_away
  • [ ] finite_presentation_of_localization_span
  • [ ] finite_presentation_of_localization_span_target
  • [ ] finite_presentation.base_change
• [ ] flat
  • [ ] flat_of_bijective
  • [ ] flat.comp
  • [ ] flat.base_change
  • [ ] localization_flat
  • [ ] flat_of_localization_maximal
• [ ] integral
  • [x] is_integral_of_surjective
  • [x] integral.comp (is_integral_of_is_scalar_tower)
  • [x] integral.base_change
  • [ ] localization_integral
  • [ ] integral_of_localization_maximal
• [ ] unramified
  • [ ] unramified_id
  • [ ] unramified.comp
  • [ ] unramified.base_change
• [ ] etale
  • [ ] etale_id
  • [ ] etale.comp
  • [ ] etale.base_change
• [ ] smooth
  • [ ] smooth_of_localization_span_target
• [ ] formally unramified
  • [x] formally_unramified_id
  • [x] formally_unramified.comp
  • [x] formally_unramified.base_change
  • [x] localization_preserves_formally_unramified
  • [x] formally_unramified_holds_for_localization_away
  • [ ] formally_unramified_of_localization_span_target
• [x] formally etale
  • [x] formally_etale_id
  • [x] formally_etale.comp
  • [x] formally_etale.base_change
  • [x] formally_etale_holds_for_localization_away
• [x] formally smooth
  • [x] formally_smooth_id
  • [x] formally_unramified.comp
  • [x] formally_unramified.base_change
  • [x] localization_preserves_formally_smooth
  • [x] formally_unramified_holds_for_localization_away

We should also prove implications between these properties:

• [ ] isomorphism/bijective implies all the others
• [x] finite = integral + finite type
• [x] finite presentation -> finite type
• [x] (if base is noetherian) finite type -> finite presentations
• [ ] etale -> flat
• [ ] etale -> unramified
• [ ] smooth -> etale
• [ ] ...

A good source for more implications is https://github.com/stacks/stacks-table/blob/master/database/morphism-properties-relation/relations.json

See also #4033.