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
• P_stable_under_composition: P is preserved under composition
• P_stable_under_base_change: P is preserved under base change
• 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)
• 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
  • localization_preserves_surjective
  • surjective_of_localization_span
  • surjective_of_localization_maximal
• bijective/isomorphism
  • localization_bijective
  • bijective_of_localization_maximal
• exact-ness
  • localization_exact
  • exact_of_localization_maximal
• finite
  • finite_of_surjective
  • finite_id ([Merged by Bors] - feat(ring_theory/finiteness): some finiteness notions in commutative algebra #4634)
  • finite.comp ([Merged by Bors] - feat(ring_theory/finiteness): some finiteness notions in commutative algebra #4634)
  • localization_finite
  • finite_of_localization_span
  • finite.base_change
• of finite type
  • finite_of_surjective
  • finite_type_id ([Merged by Bors] - feat(ring_theory/finiteness): some finiteness notions in commutative algebra #4634)
  • finite_type.comp ([Merged by Bors] - feat(ring_theory/finiteness): some finiteness notions in commutative algebra #4634)
  • localization_finite_type
  • finite_type_of_localization_span
  • finite_type_of_localization_span_target
  • finite_type_holds_for_localization_away
  • finite_type.base_change
• of finite presentation
  • finite_presentation_of_surjective
  • finite_presentation_id
  • 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
  • is_integral_of_surjective
  • integral.comp (is_integral_of_is_scalar_tower)
  • 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
  • formally_unramified_id
  • formally_unramified.comp
  • formally_unramified.base_change
  • localization_preserves_formally_unramified
  • formally_unramified_holds_for_localization_away
  • formally_unramified_of_localization_span_target
• formally etale
  • formally_etale_id
  • formally_etale.comp
  • formally_etale.base_change
  • formally_etale_holds_for_localization_away
• formally smooth
  • formally_smooth_id
  • formally_unramified.comp
  • formally_unramified.base_change
  • localization_preserves_formally_smooth
  • formally_unramified_holds_for_localization_away

We should also prove implications between these properties:

• isomorphism/bijective implies all the others
• finite = integral + finite type
• finite presentation -> finite type
• (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.