feat(ring_theory): Basic framework for classes of ring homomorphisms (#…

…14966)




Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/ring_theory/local_properties.lean

@@ -11,6 +11,7 @@ import ring_theory.localization.away
 import ring_theory.localization.integer
 import ring_theory.localization.submodule
 import ring_theory.nilpotent
+import ring_theory.ring_hom_properties
 
 /-!
 # Local properties of commutative rings
@@ -20,9 +21,10 @@ In this file, we provide the proofs of various local properties.
 ## Naming Conventions
 
 * `localization_P` : `P` holds for `S⁻¹R` if `P` holds for `R`.
-* `P_of_localization_maximal` : `P` holds for `R` if `P` holds for `Aₘ` for all maximal `m`.
+* `P_of_localization_maximal` : `P` holds for `R` if `P` holds for `Rₘ` for all maximal `m`.
+* `P_of_localization_prime` : `P` holds for `R` if `P` holds for `Rₘ` for all prime `m`.
 * `P_of_localization_span` : `P` holds for `R` if given a spanning set `{fᵢ}`, `P` holds for all
-  `A_{fᵢ}`.
+  `R_{fᵢ}`.
 
 ## Main results
 
@@ -75,7 +77,7 @@ include P
 /-- A property `P` of ring homs is said to be preserved by localization
  if `P` holds for `M⁻¹R →+* M⁻¹S` whenever `P` holds for `R →+* S`. -/
 def ring_hom.localization_preserves :=
-  ∀ {R S : Type u} [comm_ring R] [comm_ring S] (f : by exactI R →+* S) (M : by exactI submonoid R)
+  ∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S) (M : by exactI submonoid R)
     (R' S' : Type u) [comm_ring R'] [comm_ring S'] [by exactI algebra R R']
     [by exactI algebra S S'] [by exactI is_localization M R']
     [by exactI is_localization (M.map f) S'],
@@ -88,7 +90,7 @@ if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spa
 Note that this is equivalent to `ring_hom.of_localization_span` via
 `ring_hom.of_localization_span_iff_finite`, but this is easier to prove. -/
 def ring_hom.of_localization_finite_span :=
-  ∀ {R S : Type u} [comm_ring R] [comm_ring S] (f : by exactI R →+* S)
+  ∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S)
     (s : finset R) (hs : by exactI ideal.span (s : set R) = ⊤)
     (H : by exactI (∀ (r : s), P (localization.away_map f r))), by exactI P f
 
@@ -99,10 +101,40 @@ if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `R`
 Note that this is equivalent to `ring_hom.of_localization_finite_span` via
 `ring_hom.of_localization_span_iff_finite`, but this has less restrictions when applying. -/
 def ring_hom.of_localization_span :=
-  ∀ {R S : Type u} [comm_ring R] [comm_ring S] (f : by exactI R →+* S)
+  ∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S)
     (s : set R) (hs : by exactI ideal.span s = ⊤)
     (H : by exactI (∀ (r : s), P (localization.away_map f r))), by exactI P f
 
+/-- A property `P` of ring homs satisfies `ring_hom.holds_for_localization_away`
+ if `P` holds for each localization map `R →+* Rᵣ`. -/
+def ring_hom.holds_for_localization_away : Prop :=
+∀ ⦃R : Type u⦄ (S : Type u) [comm_ring R] [comm_ring S] [by exactI algebra R S] (r : R)
+  [by exactI is_localization.away r S], by exactI P (algebra_map R S)
+
+/-- A property `P` of ring homs satisfies `ring_hom.of_localization_span_target`
+if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `S` such that
+`P` holds for `R →+* Sᵣ`. -/
+def ring_hom.of_localization_span_target : Prop :=
+∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S)
+  (s : set S) (hs : by exactI ideal.span s = ⊤)
+  (H : by exactI (∀ (r : s), P ((algebra_map S (localization.away (r : S))).comp f))),
+  by exactI P f
+
+/-- A property `P` of ring homs satisfies `of_localization_prime` if
+  if `P` holds for `R` whenever `P` holds for `Rₘ` for all prime ideals `p`. -/
+def ring_hom.of_localization_prime : Prop :=
+∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S),
+  by exactI (∀ (J : ideal S) (hJ : J.is_prime),
+    by exactI P (localization.local_ring_hom _ J f rfl)) → P f
+
+/-- A property of ring homs is local if it is preserved by localizations and compositions, and for
+each `{ r }` that spans `S`, we have `P (R →+* S) ↔ ∀ r, P (R →+* Sᵣ)`. -/
+structure ring_hom.property_is_local : Prop :=
+(localization_preserves : ring_hom.localization_preserves @P)
+(of_localization_span_target : ring_hom.of_localization_span_target @P)
+(stable_under_composition : ring_hom.stable_under_composition @P)
+(holds_for_localization_away : ring_hom.holds_for_localization_away @P)
+
 lemma ring_hom.of_localization_span_iff_finite :
   ring_hom.of_localization_span @P ↔ ring_hom.of_localization_finite_span @P :=
 begin
@@ -118,9 +150,21 @@ end
 
 variables {P f R' S'}
 
+lemma _root_.ring_hom.property_is_local.respects_iso (hP : ring_hom.property_is_local @P) :
+  ring_hom.respects_iso @P :=
+begin
+  apply hP.stable_under_composition.respects_iso,
+  introv,
+  resetI,
+  letI := e.to_ring_hom.to_algebra,
+  apply_with hP.holds_for_localization_away { instances := ff },
+  apply is_localization.away_of_is_unit_of_bijective _ is_unit_one,
+  exact e.bijective
+end
+
 -- Almost all arguments are implicit since this is not intended to use mid-proof.
-lemma ring_hom.localization_away_of_localization_preserves
-  (H : ring_hom.localization_preserves @P) {r : R} [is_localization.away r R']
+lemma ring_hom.localization_preserves.away
+  (H : ring_hom.localization_preserves @P) (r : R) [is_localization.away r R']
   [is_localization.away (f r) S'] (hf : P f) :
     P (by exactI is_localization.away.map R' S' f r) :=
 begin
@@ -130,6 +174,21 @@ begin
   exact H f (submonoid.powers r) R' S' hf,
 end
 
+lemma ring_hom.property_is_local.of_localization_span (hP : ring_hom.property_is_local @P) :
+  ring_hom.of_localization_span @P :=
+begin
+  introv R hs hs',
+  resetI,
+  apply_fun (ideal.map f) at hs,
+  rw [ideal.map_span, ideal.map_top] at hs,
+  apply hP.of_localization_span_target _ _ hs,
+  rintro ⟨_, r, hr, rfl⟩,
+  have := hs' ⟨r, hr⟩,
+  convert hP.stable_under_composition _ _ (hP.holds_for_localization_away (localization.away r) r)
+    (hs' ⟨r, hr⟩) using 1,
+  exact (is_localization.map_comp _).symm
+end
+
 end ring_hom
 
 end properties
@@ -224,6 +283,41 @@ end
 
 end reduced
 
+section surjective
+
+lemma localization_preserves_surjective :
+  ring_hom.localization_preserves (λ R S _ _ f, function.surjective f) :=
+begin
+  introv R H x,
+  resetI,
+  obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := is_localization.mk'_surjective (M.map f) x,
+  obtain ⟨y, rfl⟩ := H x,
+  use is_localization.mk' R' y ⟨s, hs⟩,
+  rw is_localization.map_mk',
+  refl,
+end
+
+lemma surjective_of_localization_span :
+  ring_hom.of_localization_span (λ R S _ _ f, function.surjective f) :=
+begin
+  introv R e H,
+  rw [← set.range_iff_surjective, set.eq_univ_iff_forall],
+  resetI,
+  letI := f.to_algebra,
+  intro x,
+  apply submodule.mem_of_span_eq_top_of_smul_pow_mem (algebra.of_id R S).to_linear_map.range s e,
+  intro r,
+  obtain ⟨a, e'⟩ := H r (algebra_map _ _ x),
+  obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := is_localization.mk'_surjective (submonoid.powers (r : R)) a,
+  erw is_localization.map_mk' at e',
+  rw [eq_comm, is_localization.eq_mk'_iff_mul_eq, subtype.coe_mk, subtype.coe_mk, ← map_mul] at e',
+  obtain ⟨⟨_, n', rfl⟩, e''⟩ := (is_localization.eq_iff_exists (submonoid.powers (f r)) _).mp e',
+  rw [subtype.coe_mk, mul_assoc, ← map_pow, ← map_mul, ← map_mul, ← pow_add, mul_comm] at e'',
+  exact ⟨n + n', _, e''.symm⟩
+end
+
+end surjective
+
 section finite
 
 /-- If `S` is a finite `R`-algebra, then `S' = M⁻¹S` is a finite `R' = M⁻¹R`-algebra. -/
@@ -271,7 +365,7 @@ end
 lemma localization_away_map_finite (r : R) [is_localization.away r R']
   [is_localization.away (f r) S'] (hf : f.finite) :
     (is_localization.away.map R' S' f r).finite :=
-ring_hom.localization_away_of_localization_preserves @localization_finite hf
+localization_finite.away r hf
 
 /--
 Let `S` be an `R`-algebra, `M` an submonoid of `R`, and `S' = M⁻¹S`.
@@ -323,6 +417,7 @@ lemma multiple_mem_span_of_mem_localization_span [algebra R' S] [algebra R S]
   (s : set S) (x : S) (hx : x ∈ submodule.span R' s) :
     ∃ t : M, t • x ∈ submodule.span R s :=
 begin
+  classical,
   obtain ⟨s', hss', hs'⟩ := submodule.mem_span_finite_of_mem_span hx,
   suffices : ∃ t : M, t • x ∈ submodule.span R (s' : set S),
   { obtain ⟨t, ht⟩ := this,
@@ -446,7 +541,7 @@ end
 lemma localization_away_map_finite_type (r : R) [is_localization.away r R']
   [is_localization.away (f r) S'] (hf : f.finite_type) :
     (is_localization.away.map R' S' f r).finite_type :=
-ring_hom.localization_away_of_localization_preserves @localization_finite_type hf
+localization_finite_type.away r hf
 
 /--
 Let `S` be an `R`-algebra, `M` an submonoid of `R`, and `S' = M⁻¹S`.
@@ -483,7 +578,7 @@ begin
     (submonoid.map (algebra_map R S : R →* S) M) s : set S)).smul_mem hx' a using 1,
   convert ha₂.symm,
   { rw [mul_comm (y' ^ n • x), subtype.coe_mk, submonoid.smul_def, submonoid.coe_mul, ← smul_smul,
-        algebra.smul_def, submonoid_class.coe_pow], refl },
+      algebra.smul_def, submonoid_class.coe_pow], refl },
   { rw mul_comm, exact algebra.smul_def _ _ }
 end
 

src/ring_theory/localization/away.lean

@@ -125,6 +125,18 @@ noncomputable
 def at_one [is_localization.away (1 : R) S] : R ≃ₐ[R] S :=
 @at_unit R _ S _ _ (1 : R) is_unit_one _
 
+lemma away_of_is_unit_of_bijective {R : Type*} (S : Type*) [comm_ring R] [comm_ring S]
+  [algebra R S] {r : R} (hr : is_unit r) (H : function.bijective (algebra_map R S)) :
+  is_localization.away r S :=
+{ map_units := by { rintros ⟨_, n, rfl⟩, exact (algebra_map R S).is_unit_map (hr.pow _) },
+  surj := λ z, by { obtain ⟨z', rfl⟩ := H.2 z, exact ⟨⟨z', 1⟩, by simp⟩ },
+  eq_iff_exists := λ x y, begin
+    erw H.1.eq_iff,
+    split,
+    { rintro rfl, exact ⟨1, rfl⟩ },
+    { rintro ⟨⟨_, n, rfl⟩, e⟩, exact (hr.pow _).mul_left_inj.mp e }
+  end }
+
 end at_units
 
 end is_localization

src/ring_theory/ring_hom_properties.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2022 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import algebra.category.Ring.constructions
+import category_theory.isomorphism
+import ring_theory.localization.away
+
+/-!
+# Properties of ring homomorphisms
+
+We provide the basic framework for talking about properties of ring homomorphisms.
+The following meta-properties of predicates on ring homomorphisms are defined
+
+* `ring_hom.respects_iso`: `P` respects isomorphisms if `P f → P (e ≫ f)` and
+  `P f → P (f ≫ e)`, where `e` is an isomorphism.
+* `ring_hom.stable_under_composition`: `P` is stable under composition if `P f → P g → P (f ≫ g)`.
+* `ring_hom.stable_under_base_change`: `P` is stable under base change if `P (S ⟶ Y)`
+  implies `P (X ⟶ X ⊗[S] Y)`.
+
+-/
+
+universe u
+
+open category_theory opposite category_theory.limits
+
+namespace ring_hom
+
+variable (P : ∀ {R S : Type u} [comm_ring R] [comm_ring S] (f : by exactI R →+* S), Prop)
+
+include P
+
+section respects_iso
+
+/-- A property `respects_iso` if it still holds when composed with an isomorphism -/
+def respects_iso : Prop :=
+(∀ {R S T : Type u} [comm_ring R] [comm_ring S] [comm_ring T], by exactI
+    ∀ (f : R →+* S) (e : S ≃+* T) (hf : P f), P (e.to_ring_hom.comp f)) ∧
+  (∀ {R S T : Type u} [comm_ring R] [comm_ring S] [comm_ring T], by exactI
+    ∀ (f : S →+* T) (e : R ≃+* S) (hf : P f), P (f.comp e.to_ring_hom))
+
+variable {P}
+
+lemma respects_iso.cancel_left_is_iso (hP : respects_iso @P) {R S T : CommRing}
+  (f : R ⟶ S) (g : S ⟶ T)
+  [is_iso f] : P (f ≫ g) ↔ P g :=
+⟨λ H, by { convert hP.2 (f ≫ g) (as_iso f).symm.CommRing_iso_to_ring_equiv H,
+  exact (is_iso.inv_hom_id_assoc _ _).symm }, hP.2 g (as_iso f).CommRing_iso_to_ring_equiv⟩
+
+lemma respects_iso.cancel_right_is_iso (hP : respects_iso @P) {R S T : CommRing}
+  (f : R ⟶ S) (g : S ⟶ T)
+  [is_iso g] : P (f ≫ g) ↔ P f :=
+⟨λ H, by { convert hP.1 (f ≫ g) (as_iso g).symm.CommRing_iso_to_ring_equiv H,
+  change f = f ≫ g ≫ (inv g), simp }, hP.1 f (as_iso g).CommRing_iso_to_ring_equiv⟩
+
+lemma respects_iso.is_localization_away_iff (hP : ring_hom.respects_iso @P) {R S : Type*}
+  (R' S' : Type*) [comm_ring R] [comm_ring S] [comm_ring R'] [comm_ring S'] [algebra R R']
+  [algebra S S'] (f : R →+* S) (r : R) [is_localization.away r R'] [is_localization.away (f r) S'] :
+  P (localization.away_map f r) ↔ P (is_localization.away.map R' S' f r) :=
+begin
+  let e₁ : R' ≃+* localization.away r :=
+    (is_localization.alg_equiv (submonoid.powers r) _ _).to_ring_equiv,
+  let e₂ : localization.away (f r) ≃+* S' :=
+    (is_localization.alg_equiv (submonoid.powers (f r)) _ _).to_ring_equiv,
+  refine (hP.cancel_left_is_iso e₁.to_CommRing_iso.hom (CommRing.of_hom _)).symm.trans _,
+  refine (hP.cancel_right_is_iso (CommRing.of_hom _) e₂.to_CommRing_iso.hom).symm.trans _,
+  rw ← eq_iff_iff,
+  congr' 1,
+  dsimp [CommRing.of_hom, CommRing.of, bundled.of],
+  refine is_localization.ring_hom_ext (submonoid.powers r) _,
+  ext1,
+  revert e₁ e₂,
+  dsimp [ring_equiv.to_ring_hom, is_localization.away.map],
+  simp only [category_theory.comp_apply, ring_equiv.refl_apply, is_localization.alg_equiv_apply,
+    is_localization.ring_equiv_of_ring_equiv_apply, ring_hom.coe_mk, ring_equiv.to_fun_eq_coe,
+    is_localization.ring_equiv_of_ring_equiv_eq, is_localization.map_eq],
+end
+
+end respects_iso
+
+section stable_under_composition
+
+/-- A property is `stable_under_composition` if the composition of two such morphisms
+still falls in the class. -/
+def stable_under_composition : Prop :=
+  ∀ ⦃R S T⦄ [comm_ring R] [comm_ring S] [comm_ring T],
+    by exactI ∀ (f : R →+* S) (g : S →+* T) (hf : P f) (hg : P g), P (g.comp f)
+
+variable {P}
+
+lemma stable_under_composition.respects_iso (hP : ring_hom.stable_under_composition @P)
+  (hP' : ∀ {R S : Type*} [comm_ring R] [comm_ring S] (e : by exactI R ≃+* S),
+    by exactI P e.to_ring_hom) : ring_hom.respects_iso @P :=
+begin
+  split,
+  { introv H, resetI, apply hP, exacts [H, hP' e] },
+  { introv H, resetI, apply hP, exacts [hP' e, H] }
+end
+
+end stable_under_composition
+
+section stable_under_base_change
+
+/-- A morphism property `P` is `stable_under_base_change` if `P(S →+* A)` implies
+`P(B →+* A ⊗[S] B)`. -/
+def stable_under_base_change : Prop :=
+  ∀ ⦃R S T⦄ [comm_ring R] [comm_ring S] [comm_ring T], by exactI ∀ [algebra R S] [algebra R T],
+    by exactI (P (algebra_map R T) →
+      P (algebra.tensor_product.include_left.to_ring_hom : S →+* tensor_product R S T))
+
+lemma stable_under_base_change.pushout_inl
+  (hP : ring_hom.stable_under_base_change @P) (hP' : ring_hom.respects_iso @P) {R S T : CommRing}
+  (f : R ⟶ S) (g : R ⟶ T) (H : P g) : P (pushout.inl : S ⟶ pushout f g) :=
+begin
+  rw [← (show _ = pushout.inl, from colimit.iso_colimit_cocone_ι_inv
+    ⟨_, CommRing.pushout_cocone_is_colimit f g⟩ walking_span.left), hP'.cancel_right_is_iso],
+  apply hP,
+  exact H,
+end
+
+end stable_under_base_change
+
+end ring_hom