From 073c3ace482964f468c882180a6f9cbb97b4b7e2 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Thu, 14 Jul 2022 05:43:46 +0000 Subject: [PATCH] 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 | 115 +++++++++++++++++++-- src/ring_theory/localization/away.lean | 12 +++ src/ring_theory/ring_hom_properties.lean | 124 +++++++++++++++++++++++ 3 files changed, 241 insertions(+), 10 deletions(-) create mode 100644 src/ring_theory/ring_hom_properties.lean diff --git a/src/ring_theory/local_properties.lean b/src/ring_theory/local_properties.lean index 76555fefb3e9f..a76ad1b435a1e 100644 --- a/src/ring_theory/local_properties.lean +++ b/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 diff --git a/src/ring_theory/localization/away.lean b/src/ring_theory/localization/away.lean index 2c1f2359e9adb..94e5a33c55037 100644 --- a/src/ring_theory/localization/away.lean +++ b/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 diff --git a/src/ring_theory/ring_hom_properties.lean b/src/ring_theory/ring_hom_properties.lean new file mode 100644 index 0000000000000..37d9ac0cf1e34 --- /dev/null +++ b/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