From b479ce63ba159bc287f99242ed9fb313ea7668da Mon Sep 17 00:00:00 2001 From: Yongle Hu Date: Tue, 24 Sep 2024 15:04:44 +0000 Subject: [PATCH] chore(Mathlib/RingTheory/LocalProperties): split LocalProperties.lean (#16879) Split the section on local properties in general and the properties that satisfy local properties in `LocalProperties.lean` into separate files. See the discussions [here](https://github.com/leanprover-community/mathlib4/pull/16558#discussion_r1761381528). Co-authored-by: Hu Yongle <2065545849@qq.com> Co-authored-by: Yongle Hu <2065545849@qq.com> --- Mathlib.lean | 4 +- .../Morphisms/ClosedImmersion.lean | 4 +- .../Morphisms/Preimmersion.lean | 4 +- .../Morphisms/RingHomProperties.lean | 2 +- Mathlib/AlgebraicGeometry/Properties.lean | 5 +- Mathlib/RingTheory/Ideal/Norm.lean | 2 +- .../IntegralClosure/IntegralRestrict.lean | 8 +- .../IntegralClosure/IntegrallyClosed.lean | 40 +- Mathlib/RingTheory/LocalProperties.lean | 709 ------------------ Mathlib/RingTheory/LocalProperties/Basic.lean | 332 ++++++++ .../LocalProperties/IntegrallyClosed.lean | 68 ++ .../RingTheory/LocalProperties/Reduced.lean | 53 ++ .../RingTheory/Localization/Finiteness.lean | 2 +- Mathlib/RingTheory/RingHom/Finite.lean | 195 ++++- Mathlib/RingTheory/RingHom/FiniteType.lean | 136 +++- Mathlib/RingTheory/RingHom/Surjective.lean | 69 +- 16 files changed, 842 insertions(+), 791 deletions(-) delete mode 100644 Mathlib/RingTheory/LocalProperties.lean create mode 100644 Mathlib/RingTheory/LocalProperties/Basic.lean create mode 100644 Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean create mode 100644 Mathlib/RingTheory/LocalProperties/Reduced.lean diff --git a/Mathlib.lean b/Mathlib.lean index 4de0c7bf38993..cc970198038fa 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3920,7 +3920,9 @@ import Mathlib.RingTheory.Kaehler.CotangentComplex import Mathlib.RingTheory.Kaehler.Polynomial import Mathlib.RingTheory.LaurentSeries import Mathlib.RingTheory.LittleWedderburn -import Mathlib.RingTheory.LocalProperties +import Mathlib.RingTheory.LocalProperties.Basic +import Mathlib.RingTheory.LocalProperties.IntegrallyClosed +import Mathlib.RingTheory.LocalProperties.Reduced import Mathlib.RingTheory.LocalRing.Basic import Mathlib.RingTheory.LocalRing.Defs import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic diff --git a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean index 4affb2c6194ba..4eedb17248903 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean @@ -95,11 +95,11 @@ theorem spec_of_surjective {R S : CommRingCat} (f : R ⟶ S) (h : Function.Surje surj_on_stalks x := by haveI : (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso := by rw [← RingHom.toMorphismProperty_respectsIso_iff] - exact surjective_respectsIso + exact RingHom.surjective_respectsIso apply (MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)) (Scheme.arrowStalkMapSpecIso f x)).mpr - exact surjective_localRingHom_of_surjective f h x.asIdeal + exact RingHom.surjective_localRingHom_of_surjective f h x.asIdeal /-- For any ideal `I` in a commutative ring `R`, the quotient map `specObj R ⟶ specObj (R ⧸ I)` is a closed immersion. -/ diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean index 25d3e57f11b98..b9472fc3ea550 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap -import Mathlib.RingTheory.LocalProperties +import Mathlib.RingTheory.RingHom.Surjective /-! @@ -52,7 +52,7 @@ lemma isPreimmersion_eq_inf : /-- Being surjective on stalks is local at the target. -/ instance isSurjectiveOnStalks_isLocalAtTarget : IsLocalAtTarget (stalkwise (Function.Surjective ·)) := - stalkwiseIsLocalAtTarget_of_respectsIso surjective_respectsIso + stalkwiseIsLocalAtTarget_of_respectsIso RingHom.surjective_respectsIso namespace IsPreimmersion diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean index fe7b94f0420b3..1a867be2b4d2a 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ import Mathlib.AlgebraicGeometry.Morphisms.Basic -import Mathlib.RingTheory.LocalProperties +import Mathlib.RingTheory.LocalProperties.Basic /-! diff --git a/Mathlib/AlgebraicGeometry/Properties.lean b/Mathlib/AlgebraicGeometry/Properties.lean index d4cb9d574a2c2..70e632782f02a 100644 --- a/Mathlib/AlgebraicGeometry/Properties.lean +++ b/Mathlib/AlgebraicGeometry/Properties.lean @@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ import Mathlib.AlgebraicGeometry.AffineScheme -import Mathlib.RingTheory.Nilpotent.Lemmas -import Mathlib.Topology.Sheaves.SheafCondition.Sites -import Mathlib.Algebra.Category.Ring.Constructions -import Mathlib.RingTheory.LocalProperties +import Mathlib.RingTheory.LocalProperties.Reduced /-! # Basic properties of schemes diff --git a/Mathlib/RingTheory/Ideal/Norm.lean b/Mathlib/RingTheory/Ideal/Norm.lean index b30d0820ffb94..6e1a0aa1de64f 100644 --- a/Mathlib/RingTheory/Ideal/Norm.lean +++ b/Mathlib/RingTheory/Ideal/Norm.lean @@ -12,7 +12,7 @@ import Mathlib.LinearAlgebra.FreeModule.Determinant import Mathlib.LinearAlgebra.FreeModule.IdealQuotient import Mathlib.RingTheory.DedekindDomain.PID import Mathlib.RingTheory.Ideal.Basis -import Mathlib.RingTheory.LocalProperties +import Mathlib.RingTheory.LocalProperties.Basic import Mathlib.RingTheory.Localization.NormTrace /-! diff --git a/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean b/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean index f0f556d8c02f6..5253fd9dff111 100644 --- a/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean +++ b/Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean @@ -3,11 +3,11 @@ Copyright (c) 2023 Andrew Yang, Patrick Lutz. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ -import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed -import Mathlib.RingTheory.LocalProperties -import Mathlib.RingTheory.Localization.NormTrace -import Mathlib.RingTheory.Localization.LocalizationLocalization import Mathlib.RingTheory.DedekindDomain.IntegralClosure +import Mathlib.RingTheory.RingHom.Finite +import Mathlib.RingTheory.Localization.LocalizationLocalization +import Mathlib.RingTheory.Localization.NormTrace + /-! # Restriction of various maps between fields to integrally closed subrings. diff --git a/Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean b/Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean index bca52f16d811e..c987ccc2c77c5 100644 --- a/Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean +++ b/Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Anne Baanen -/ import Mathlib.RingTheory.Localization.Integral -import Mathlib.RingTheory.Localization.LocalizationLocalization /-! # Integrally closed rings @@ -278,44 +277,7 @@ end integralClosure /-- Any field is integral closed. -/ /- Although `infer_instance` can find this if you import Mathlib, in this file they have not been - proven yet. However, the next theorem is a fundamental property of `IsIntegrallyClosed`, + proven yet. However, it is used to prove a fundamental property of `IsIntegrallyClosed`, and it is not desirable to involve more content from other files. -/ instance Field.instIsIntegrallyClosed (K : Type*) [Field K] : IsIntegrallyClosed K := (isIntegrallyClosed_iff K).mpr fun {x} _ ↦ ⟨x, rfl⟩ - -open Localization Ideal IsLocalization in -/-- An integral domain `R` is integral closed if `Rₘ` is integral closed -for any maximal ideal `m` of `R`. -/ -theorem IsIntegrallyClosed.of_localization_maximal {R : Type*} [CommRing R] [IsDomain R] - (h : ∀ p : Ideal R, p ≠ ⊥ → [p.IsMaximal] → IsIntegrallyClosed (Localization.AtPrime p)) : - IsIntegrallyClosed R := by - by_cases hf : IsField R - · exact hf.toField.instIsIntegrallyClosed - apply (isIntegrallyClosed_iff (FractionRing R)).mpr - rintro ⟨x⟩ hx - let I : Ideal R := span {x.2.1} / span {x.1} - have h1 : 1 ∈ I := by - apply I.eq_top_iff_one.mp - by_contra hn - rcases I.exists_le_maximal hn with ⟨p, hpm, hpi⟩ - have hic := h p (Ring.ne_bot_of_isMaximal_of_not_isField hpm hf) - have hxp : IsIntegral (Localization.AtPrime p) (mk x.1 x.2) := hx.tower_top - /- `x.1 / x.2.1 ∈ Rₚ` since it is integral over `Rₚ` and `Rₚ` is integrally closed. - More precisely, `x.1 / x.2.1 = y.1 / y.2.1` where `y.1, y.2.1 ∈ R` and `y.2.1 ∉ p`. -/ - rcases (isIntegrallyClosed_iff (FractionRing R)).mp hic hxp with ⟨⟨y⟩, hy⟩ - /- `y.2.1 ∈ I` since for all `a ∈ Ideal.span {x.1}`, say `a = b * x.1`, - we have `y.2 * a = b * x.1 * y.2 = b * y.1 * x.2.1 ∈ Ideal.span {x.2.1}`. -/ - have hyi : y.2.1 ∈ I := by - intro a ha - rcases mem_span_singleton'.mp ha with ⟨b, hb⟩ - apply mem_span_singleton'.mpr ⟨b * y.1, _⟩ - rw [← hb, ← mul_assoc, mul_comm y.2.1 b, mul_assoc, mul_assoc] - exact congrArg (HMul.hMul b) <| (mul_comm y.1 x.2.1).trans <| - NoZeroSMulDivisors.algebraMap_injective R (Localization R⁰) <| mk'_eq_iff_eq.mp <| - (mk'_eq_algebraMap_mk'_of_submonoid_le _ _ p.primeCompl_le_nonZeroDivisors y.1 y.2).trans - <| show algebraMap (Localization.AtPrime p) _ (mk' _ y.1 y.2) = mk' _ x.1 x.2 - by simpa only [← mk_eq_mk', ← hy] using by rfl - -- `y.2.1 ∈ I` implies `y.2.1 ∈ p` since `I ⊆ p`, which contradicts to the choice of `y`. - exact y.2.2 (hpi hyi) - rcases mem_span_singleton'.mp (h1 x.1 (mem_span_singleton_self x.1)) with ⟨y, hy⟩ - exact ⟨y, (eq_mk'_of_mul_eq (hy.trans (one_mul x.1))).trans (mk_eq_mk'_apply x.1 x.2).symm⟩ diff --git a/Mathlib/RingTheory/LocalProperties.lean b/Mathlib/RingTheory/LocalProperties.lean deleted file mode 100644 index 8add67ec8ef96..0000000000000 --- a/Mathlib/RingTheory/LocalProperties.lean +++ /dev/null @@ -1,709 +0,0 @@ -/- -Copyright (c) 2021 Andrew Yang. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Andrew Yang --/ -import Mathlib.RingTheory.Localization.Submodule -import Mathlib.RingTheory.RingHomProperties -import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed - -/-! -# Local properties of commutative rings - -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 `Rₘ` for all maximal `m`. -* `P_of_localization_prime` : `P` holds for `R` if `P` holds for `Rₘ` for all prime `m`. -* `P_ofLocalizationSpan` : `P` holds for `R` if given a spanning set `{fᵢ}`, `P` holds for all - `R_{fᵢ}`. - -## Main results - -The following properties are covered: - -* The triviality of an ideal or an element: - `ideal_eq_bot_of_localization`, `eq_zero_of_localization` -* `IsReduced` : `localization_isReduced`, `isReduced_of_localization_maximal`. -* `RingHom.finite`: `localization_finite`, `finite_ofLocalizationSpan` -* `RingHom.finiteType`: `localization_finiteType`, `finiteType_ofLocalizationSpan` - --/ - -open scoped Pointwise Classical - -universe u - -variable {R S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) -variable (N : Submonoid S) (R' S' : Type u) [CommRing R'] [CommRing S'] (f : R →+* S) -variable [Algebra R R'] [Algebra S S'] - -section Properties - -section CommRing - -variable (P : ∀ (R : Type u) [CommRing R], Prop) - -/-- A property `P` of comm rings is said to be preserved by localization - if `P` holds for `M⁻¹R` whenever `P` holds for `R`. -/ -def LocalizationPreserves : Prop := - ∀ {R : Type u} [hR : CommRing R] (M : Submonoid R) (S : Type u) [hS : CommRing S] [Algebra R S] - [IsLocalization M S], @P R hR → @P S hS - -/-- A property `P` of comm rings satisfies `OfLocalizationMaximal` - if `P` holds for `R` whenever `P` holds for `Rₘ` for all maximal ideal `m`. -/ -def OfLocalizationMaximal : Prop := - ∀ (R : Type u) [CommRing R], - (∀ (J : Ideal R) (_ : J.IsMaximal), P (Localization.AtPrime J)) → P R - -end CommRing - -section RingHom - -variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop) - -/-- A property `P` of ring homs is said to contain identities if `P` holds -for the identity homomorphism of every ring. -/ -def RingHom.ContainsIdentities := ∀ (R : Type u) [CommRing R], P (RingHom.id R) - -/-- 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 RingHom.LocalizationPreserves := - ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (M : Submonoid R) (R' S' : Type u) - [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] [IsLocalization M R'] - [IsLocalization (M.map f) S'], - P f → P (IsLocalization.map S' f (Submonoid.le_comap_map M) : R' →+* S') - -/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan` -if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `R` such that -`P` holds for `Rᵣ →+* Sᵣ`. - -Note that this is equivalent to `RingHom.OfLocalizationSpan` via -`RingHom.ofLocalizationSpan_iff_finite`, but this is easier to prove. -/ -def RingHom.OfLocalizationFiniteSpan := - ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Finset R) - (_ : Ideal.span (s : Set R) = ⊤) (_ : ∀ r : s, P (Localization.awayMap f r)), P f - -/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan` -if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `R` such that -`P` holds for `Rᵣ →+* Sᵣ`. - -Note that this is equivalent to `RingHom.OfLocalizationFiniteSpan` via -`RingHom.ofLocalizationSpan_iff_finite`, but this has less restrictions when applying. -/ -def RingHom.OfLocalizationSpan := - ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (_ : Ideal.span s = ⊤) - (_ : ∀ r : s, P (Localization.awayMap f r)), P f - -/-- A property `P` of ring homs satisfies `RingHom.HoldsForLocalizationAway` - if `P` holds for each localization map `R →+* Rᵣ`. -/ -def RingHom.HoldsForLocalizationAway : Prop := - ∀ ⦃R : Type u⦄ (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (r : R) - [IsLocalization.Away r S], P (algebraMap R S) - -/-- A property `P` of ring homs satisfies `RingHom.StableUnderCompositionWithLocalizationAway` -if whenever `P` holds for `f` it also holds for the composition with -localization maps on the left and on the right. -/ -def RingHom.StableUnderCompositionWithLocalizationAway : Prop := - (∀ ⦃R S : Type u⦄ (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra S T] (s : S) - [IsLocalization.Away s T] (f : R →+* S), P f → P ((algebraMap S T).comp f)) ∧ - ∀ ⦃R : Type u⦄ (S : Type u) ⦃T : Type u⦄ [CommRing R] [CommRing S] [CommRing T] [Algebra R S] - (r : R) [IsLocalization.Away r S] (f : S →+* T), P f → P (f.comp (algebraMap R S)) - -/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpanTarget` -if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `S` such that -`P` holds for `R →+* Sᵣ`. - -Note that this is equivalent to `RingHom.OfLocalizationSpanTarget` via -`RingHom.ofLocalizationSpanTarget_iff_finite`, but this is easier to prove. -/ -def RingHom.OfLocalizationFiniteSpanTarget : Prop := - ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Finset S) - (_ : Ideal.span (s : Set S) = ⊤) - (_ : ∀ r : s, P ((algebraMap S (Localization.Away (r : S))).comp f)), P f - -/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationSpanTarget` -if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `S` such that -`P` holds for `R →+* Sᵣ`. - -Note that this is equivalent to `RingHom.OfLocalizationFiniteSpanTarget` via -`RingHom.ofLocalizationSpanTarget_iff_finite`, but this has less restrictions when applying. -/ -def RingHom.OfLocalizationSpanTarget : Prop := - ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (_ : Ideal.span s = ⊤) - (_ : ∀ r : s, P ((algebraMap S (Localization.Away (r : S))).comp f)), P f - -/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationPrime` -if `P` holds for `R` whenever `P` holds for `Rₘ` for all prime ideals `p`. -/ -def RingHom.OfLocalizationPrime : Prop := - ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S), - (∀ (J : Ideal S) (_ : J.IsPrime), P (Localization.localRingHom _ 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 RingHom.PropertyIsLocal : Prop where - LocalizationPreserves : RingHom.LocalizationPreserves @P - OfLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget @P - StableUnderCompositionWithLocalizationAway : RingHom.StableUnderCompositionWithLocalizationAway @P - -theorem RingHom.ofLocalizationSpan_iff_finite : - RingHom.OfLocalizationSpan @P ↔ RingHom.OfLocalizationFiniteSpan @P := by - delta RingHom.OfLocalizationSpan RingHom.OfLocalizationFiniteSpan - apply forall₅_congr - -- TODO: Using `refine` here breaks `resetI`. - intros - constructor - · intro h s; exact h s - · intro h s hs hs' - obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs - exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩ - -theorem RingHom.ofLocalizationSpanTarget_iff_finite : - RingHom.OfLocalizationSpanTarget @P ↔ RingHom.OfLocalizationFiniteSpanTarget @P := by - delta RingHom.OfLocalizationSpanTarget RingHom.OfLocalizationFiniteSpanTarget - apply forall₅_congr - -- TODO: Using `refine` here breaks `resetI`. - intros - constructor - · intro h s; exact h s - · intro h s hs hs' - obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs - exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩ - -theorem RingHom.HoldsForLocalizationAway.of_bijective - (H : RingHom.HoldsForLocalizationAway P) (hf : Function.Bijective f) : - P f := by - letI := f.toAlgebra - have := IsLocalization.at_units (.powers (1 : R)) (by simp) - have := IsLocalization.isLocalization_of_algEquiv (.powers (1 : R)) - (AlgEquiv.ofBijective (Algebra.ofId R S) hf) - exact H _ 1 - -variable {P f R' S'} - -lemma RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway - (hPc : RingHom.StableUnderComposition P) (hPl : HoldsForLocalizationAway P) : - StableUnderCompositionWithLocalizationAway P := by - constructor - · introv _ hf - exact hPc _ _ hf (hPl T s) - · introv _ hf - exact hPc _ _ (hPl S r) hf - -lemma RingHom.HoldsForLocalizationAway.containsIdentities (hPl : HoldsForLocalizationAway P) : - ContainsIdentities P := by - introv R - exact hPl.of_bijective _ _ Function.bijective_id - -theorem RingHom.PropertyIsLocal.respectsIso (hP : RingHom.PropertyIsLocal @P) : - RingHom.RespectsIso @P := by - constructor - · intro R S T _ _ _ f e hf - letI := e.toRingHom.toAlgebra - have : IsLocalization.Away (1 : S) T := - IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective - exact hP.StableUnderCompositionWithLocalizationAway.left T (1 : S) f hf - · intro R S T _ _ _ f e hf - letI := e.toRingHom.toAlgebra - have : IsLocalization.Away (1 : R) S := - IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective - exact hP.StableUnderCompositionWithLocalizationAway.right S (1 : R) f hf - --- Almost all arguments are implicit since this is not intended to use mid-proof. -theorem RingHom.LocalizationPreserves.away (H : RingHom.LocalizationPreserves @P) (r : R) - [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : P f) : - P (IsLocalization.Away.map R' S' f r) := by - have : IsLocalization ((Submonoid.powers r).map f) S' := by rw [Submonoid.map_powers]; assumption - exact H f (Submonoid.powers r) R' S' hf - -lemma RingHom.PropertyIsLocal.HoldsForLocalizationAway (hP : RingHom.PropertyIsLocal @P) - (hPi : ContainsIdentities P) : - RingHom.HoldsForLocalizationAway @P := by - introv R _ - have : algebraMap R S = (algebraMap R S).comp (RingHom.id R) := by simp - rw [this] - apply (hP.StableUnderCompositionWithLocalizationAway).left S r - apply hPi - -theorem RingHom.PropertyIsLocal.ofLocalizationSpan (hP : RingHom.PropertyIsLocal @P) : - RingHom.OfLocalizationSpan @P := by - introv R hs hs' - apply_fun Ideal.map f at hs - rw [Ideal.map_span, Ideal.map_top] at hs - apply hP.OfLocalizationSpanTarget _ _ hs - rintro ⟨_, r, hr, rfl⟩ - rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r) - (T := Submonoid.powers (f r))] - apply hP.StableUnderCompositionWithLocalizationAway.right _ r - exact hs' ⟨r, hr⟩ - -lemma RingHom.OfLocalizationSpanTarget.ofIsLocalization - (hP : RingHom.OfLocalizationSpanTarget P) (hP' : RingHom.RespectsIso P) - {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (hs : Ideal.span s = ⊤) - (hT : ∀ r : s, ∃ (T : Type u) (_ : CommRing T) (_ : Algebra S T) - (_ : IsLocalization.Away (r : S) T), P ((algebraMap S T).comp f)) : P f := by - apply hP _ s hs - intros r - obtain ⟨T, _, _, _, hT⟩ := hT r - convert hP'.1 _ - (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT - rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_eq_coe, - AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp, - RingHom.comp_id] - -end RingHom - -end Properties - -section Ideal - -open scoped nonZeroDivisors - -/-- Let `I J : Ideal R`. If the localization of `I` at each maximal ideal `P` is included in -the localization of `J` at `P`, then `I ≤ J`. -/ -theorem Ideal.le_of_localization_maximal {I J : Ideal R} - (h : ∀ (P : Ideal R) (hP : P.IsMaximal), - Ideal.map (algebraMap R (Localization.AtPrime P)) I ≤ - Ideal.map (algebraMap R (Localization.AtPrime P)) J) : - I ≤ J := by - intro x hx - suffices J.colon (Ideal.span {x}) = ⊤ by - simpa using Submodule.mem_colon.mp - (show (1 : R) ∈ J.colon (Ideal.span {x}) from this.symm ▸ Submodule.mem_top) x - (Ideal.mem_span_singleton_self x) - refine Not.imp_symm (J.colon (Ideal.span {x})).exists_le_maximal ?_ - push_neg - intro P hP le - obtain ⟨⟨⟨a, ha⟩, ⟨s, hs⟩⟩, eq⟩ := - (IsLocalization.mem_map_algebraMap_iff P.primeCompl _).mp (h P hP (Ideal.mem_map_of_mem _ hx)) - rw [← _root_.map_mul, ← sub_eq_zero, ← map_sub] at eq - obtain ⟨⟨m, hm⟩, eq⟩ := (IsLocalization.map_eq_zero_iff P.primeCompl _ _).mp eq - refine hs ((hP.isPrime.mem_or_mem (le (Ideal.mem_colon_singleton.mpr ?_))).resolve_right hm) - simp only [Subtype.coe_mk, mul_sub, sub_eq_zero, mul_comm x s, mul_left_comm] at eq - simpa only [mul_assoc, eq] using J.mul_mem_left m ha - -/-- Let `I J : Ideal R`. If the localization of `I` at each maximal ideal `P` is equal to -the localization of `J` at `P`, then `I = J`. -/ -theorem Ideal.eq_of_localization_maximal {I J : Ideal R} - (h : ∀ (P : Ideal R) (_ : P.IsMaximal), - Ideal.map (algebraMap R (Localization.AtPrime P)) I = - Ideal.map (algebraMap R (Localization.AtPrime P)) J) : - I = J := - le_antisymm (Ideal.le_of_localization_maximal fun P hP => (h P hP).le) - (Ideal.le_of_localization_maximal fun P hP => (h P hP).ge) - -/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/ -theorem ideal_eq_bot_of_localization' (I : Ideal R) - (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), - Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) : - I = ⊥ := - Ideal.eq_of_localization_maximal fun P hP => by simpa using h P hP - --- TODO: This proof should work for all modules, once we have enough material on submodules of --- localized modules. -/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/ -theorem ideal_eq_bot_of_localization (I : Ideal R) - (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), - IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥) : - I = ⊥ := - ideal_eq_bot_of_localization' _ fun P hP => - (Ideal.map_eq_bot_iff_le_ker _).mpr fun x hx => by - rw [RingHom.mem_ker, ← Submodule.mem_bot R, ← h P hP, IsLocalization.mem_coeSubmodule] - exact ⟨x, hx, rfl⟩ - -theorem eq_zero_of_localization (r : R) - (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), algebraMap R (Localization.AtPrime J) r = 0) : - r = 0 := by - rw [← Ideal.span_singleton_eq_bot] - apply ideal_eq_bot_of_localization - intro J hJ - delta IsLocalization.coeSubmodule - erw [Submodule.map_span, Submodule.span_eq_bot] - rintro _ ⟨_, h', rfl⟩ - cases Set.mem_singleton_iff.mpr h' - exact h J hJ - -end Ideal - -section Reduced - -theorem localization_isReduced : LocalizationPreserves fun R hR => IsReduced R := by - introv R _ _ - constructor - rintro x ⟨_ | n, e⟩ - · simpa using congr_arg (· * x) e - obtain ⟨⟨y, m⟩, hx⟩ := IsLocalization.surj M x - dsimp only at hx - let hx' := congr_arg (· ^ n.succ) hx - simp only [mul_pow, e, zero_mul, ← RingHom.map_pow] at hx' - rw [← (algebraMap R S).map_zero] at hx' - obtain ⟨m', hm'⟩ := (IsLocalization.eq_iff_exists M S).mp hx' - apply_fun (· * (m' : R) ^ n) at hm' - simp only [mul_assoc, zero_mul, mul_zero] at hm' - rw [← mul_left_comm, ← pow_succ', ← mul_pow] at hm' - replace hm' := IsNilpotent.eq_zero ⟨_, hm'.symm⟩ - rw [← (IsLocalization.map_units S m).mul_left_inj, hx, zero_mul, - IsLocalization.map_eq_zero_iff M] - exact ⟨m', by rw [← hm', mul_comm]⟩ - -instance [IsReduced R] : IsReduced (Localization M) := - localization_isReduced M _ inferInstance - -theorem isReduced_ofLocalizationMaximal : OfLocalizationMaximal fun R hR => IsReduced R := by - introv R h - constructor - intro x hx - apply eq_zero_of_localization - intro J hJ - specialize h J hJ - exact (hx.map <| algebraMap R <| Localization.AtPrime J).eq_zero - -end Reduced - -section Surjective - -theorem localizationPreserves_surjective : - RingHom.LocalizationPreserves fun {R S} _ _ f => Function.Surjective f := by - introv R H x - obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (M.map f) x - obtain ⟨y, rfl⟩ := H x - use IsLocalization.mk' R' y ⟨s, hs⟩ - rw [IsLocalization.map_mk'] - -theorem surjective_ofLocalizationSpan : - RingHom.OfLocalizationSpan fun {R S} _ _ f => Function.Surjective f := by - introv R e H - rw [← Set.range_iff_surjective, Set.eq_univ_iff_forall] - letI := f.toAlgebra - intro x - apply Submodule.mem_of_span_eq_top_of_smul_pow_mem - (LinearMap.range (Algebra.linearMap R S)) s e - intro r - obtain ⟨a, e'⟩ := H r (algebraMap _ _ x) - obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (r : R)) a - erw [IsLocalization.map_mk'] at e' - rw [eq_comm, IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, Subtype.coe_mk, ← map_mul] at e' - obtain ⟨⟨_, n', rfl⟩, e''⟩ := (IsLocalization.eq_iff_exists (Submonoid.powers (f r)) _).mp e' - dsimp only at e'' - rw [mul_comm x, ← mul_assoc, ← map_pow, ← map_mul, ← map_mul, ← pow_add] at e'' - exact ⟨n' + n, _, e''.symm⟩ - -/-- A surjective ring homomorphism `R →+* S` induces a surjective homomorphism `R_{f⁻¹(P)} →+* S_P` -for every prime ideal `P` of `S`. -/ -theorem surjective_localRingHom_of_surjective (h : Function.Surjective f) (P : Ideal S) - [P.IsPrime] : Function.Surjective (Localization.localRingHom (P.comap f) P f rfl) := - have : IsLocalization (Submonoid.map f (Ideal.comap f P).primeCompl) (Localization.AtPrime P) := - (Submonoid.map_comap_eq_of_surjective h P.primeCompl).symm ▸ Localization.isLocalization - localizationPreserves_surjective _ _ _ _ h - -lemma surjective_respectsIso : RingHom.RespectsIso (fun f ↦ Function.Surjective f) := by - apply RingHom.StableUnderComposition.respectsIso - · intro R S T _ _ _ f g hf hg - simp only [RingHom.coe_comp] - exact Function.Surjective.comp hg hf - · intro R S _ _ e - exact EquivLike.surjective e - -end Surjective - -section Finite - -lemma Module.Finite_of_isLocalization (R S Rₚ Sₚ) [CommSemiring R] [CommRing S] [CommRing Rₚ] - [CommRing Sₚ] [Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] - [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ] - [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] : - Module.Finite Rₚ Sₚ := by - classical - have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ - (algebraMap R S) (Submonoid.le_comap_map M) := by - apply IsLocalization.ringHom_ext M - simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq] - -- We claim that if `S` is generated by `T` as an `R`-module, - -- then `S'` is generated by `T` as an `R'`-module. - obtain ⟨T, hT⟩ := hRS - use T.image (algebraMap S Sₚ) - rw [eq_top_iff] - rintro x - - -- By the hypotheses, for each `x : S'`, we have `x = y / (f r)` for some `y : S` and `r : M`. - -- Since `S` is generated by `T`, the image of `y` should fall in the span of the image of `T`. - obtain ⟨y, ⟨_, ⟨r, hr, rfl⟩⟩, rfl⟩ := - IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x - rw [IsLocalization.mk'_eq_mul_mk'_one, mul_comm, Finset.coe_image] - have hy : y ∈ Submodule.span R ↑T := by rw [hT]; trivial - replace hy : algebraMap S Sₚ y ∈ Submodule.map (IsScalarTower.toAlgHom R S Sₚ).toLinearMap - (Submodule.span R (T : Set S)) := Submodule.mem_map_of_mem --- -- Note: #8386 had to specify the value of `f` below - (f := (IsScalarTower.toAlgHom R S Sₚ).toLinearMap) hy - rw [Submodule.map_span (IsScalarTower.toAlgHom R S Sₚ).toLinearMap T] at hy - have H : Submodule.span R (algebraMap S Sₚ '' T) ≤ - (Submodule.span Rₚ (algebraMap S Sₚ '' T)).restrictScalars R := by - rw [Submodule.span_le]; exact Submodule.subset_span - -- Now, since `y ∈ span T`, and `(f r)⁻¹ ∈ R'`, `x / (f r)` is in `span T` as well. - convert (Submodule.span Rₚ (algebraMap S Sₚ '' T)).smul_mem - (IsLocalization.mk' Rₚ (1 : R) ⟨r, hr⟩) (H hy) using 1 - rw [Algebra.smul_def, this, IsLocalization.map_mk', map_one] - -/-- If `S` is a finite `R`-algebra, then `S' = M⁻¹S` is a finite `R' = M⁻¹R`-algebra. -/ -theorem localization_finite : RingHom.LocalizationPreserves @RingHom.Finite := by - introv R hf - letI := f.toAlgebra - letI := ((algebraMap S S').comp f).toAlgebra - let f' : R' →+* S' := IsLocalization.map S' f (Submonoid.le_comap_map M) - letI := f'.toAlgebra - have : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq' - (IsLocalization.map_comp M.le_comap_map).symm - have : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' rfl - have : IsLocalization (Algebra.algebraMapSubmonoid S M) S' := by - rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra] - have : Module.Finite R S := hf - apply Module.Finite_of_isLocalization R S R' S' M - -theorem localization_away_map_finite (r : R) [IsLocalization.Away r R'] - [IsLocalization.Away (f r) S'] (hf : f.Finite) : (IsLocalization.Away.map R' S' f r).Finite := - localization_finite.away r hf - -/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`. -If the image of some `x : S` falls in the span of some finite `s ⊆ S'` over `R`, -then there exists some `m : M` such that `m • x` falls in the -span of `IsLocalization.finsetIntegerMultiple _ s` over `R`. --/ -theorem IsLocalization.smul_mem_finsetIntegerMultiple_span [Algebra R S] [Algebra R S'] - [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S') - (hx : algebraMap S S' x ∈ Submodule.span R (s : Set S')) : - ∃ m : M, m • x ∈ - Submodule.span R - (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) := by - let g : S →ₐ[R] S' := - AlgHom.mk' (algebraMap S S') fun c x => by simp [Algebra.algebraMap_eq_smul_one] - -- We first obtain the `y' ∈ M` such that `s' = y' • s` is falls in the image of `S` in `S'`. - let y := IsLocalization.commonDenomOfFinset (M.map (algebraMap R S)) s - have hx₁ : (y : S) • (s : Set S') = g '' _ := - (IsLocalization.finsetIntegerMultiple_image _ s).symm - obtain ⟨y', hy', e : algebraMap R S y' = y⟩ := y.prop - have : algebraMap R S y' • (s : Set S') = y' • (s : Set S') := by - simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul] - rw [← e, this] at hx₁ - replace hx₁ := congr_arg (Submodule.span R) hx₁ - rw [Submodule.span_smul] at hx₁ - replace hx : _ ∈ y' • Submodule.span R (s : Set S') := Set.smul_mem_smul_set hx - rw [hx₁] at hx - erw [← _root_.map_smul g, ← Submodule.map_span (g : S →ₗ[R] S')] at hx - -- Since `x` falls in the span of `s` in `S'`, `y' • x : S` falls in the span of `s'` in `S'`. - -- That is, there exists some `x' : S` in the span of `s'` in `S` and `x' = y' • x` in `S'`. - -- Thus `a • (y' • x) = a • x' ∈ span s'` in `S` for some `a ∈ M`. - obtain ⟨x', hx', hx'' : algebraMap _ _ _ = _⟩ := hx - obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ := - (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx'' - use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M) - convert (Submodule.span R - (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s : Set S)).smul_mem - a hx' using 1 - convert ha₂.symm using 1 - · rw [Subtype.coe_mk, Submonoid.smul_def, Submonoid.coe_mul, ← smul_smul] - exact Algebra.smul_def _ _ - · exact Algebra.smul_def _ _ - -/-- If `M` is an `R' = S⁻¹R` module, and `x ∈ span R' s`, -then `t • x ∈ span R s` for some `t : S`. -/ -theorem multiple_mem_span_of_mem_localization_span - {N : Type*} [AddCommMonoid N] [Module R N] [Module R' N] - [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N) - (hx : x ∈ Submodule.span R' s) : ∃ (t : M), t • x ∈ Submodule.span R s := by - classical - obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx - rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N) - · exact ⟨t, Submodule.span_mono hss' ht⟩ - clear hx hss' s - induction s' using Finset.induction_on generalizing x - · use 1; simpa using hs' - rename_i a s _ hs - simp only [Finset.coe_insert, Finset.image_insert, Finset.coe_image, Subtype.coe_mk, - Submodule.mem_span_insert] at hs' ⊢ - rcases hs' with ⟨y, z, hz, rfl⟩ - rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩ - apply congrArg (fun x ↦ x • a) at e - simp only [algebraMap_smul] at e - rcases hs _ hz with ⟨t, ht⟩ - refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩ - rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def] - simp - rfl - -/-- If `S` is an `R' = M⁻¹R` algebra, and `x ∈ adjoin R' s`, -then `t • x ∈ adjoin R s` for some `t : M`. -/ -theorem multiple_mem_adjoin_of_mem_localization_adjoin [Algebra R' S] [Algebra R S] - [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S) (x : S) - (hx : x ∈ Algebra.adjoin R' s) : ∃ t : M, t • x ∈ Algebra.adjoin R s := by - change ∃ t : M, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s) - change x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s) at hx - simp_rw [Algebra.adjoin_eq_span] at hx ⊢ - exact multiple_mem_span_of_mem_localization_span M R' _ _ hx - -theorem finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.Finite := by - rw [RingHom.ofLocalizationSpan_iff_finite] - introv R hs H - -- We first setup the instances - letI := f.toAlgebra - letI := fun r : s => (Localization.awayMap f r).toAlgebra - have : ∀ r : s, - IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S)) (Localization.Away (f r)) := - by intro r; rw [Submonoid.map_powers]; exact Localization.isLocalization - haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) := - fun r => IsScalarTower.of_algebraMap_eq' - (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm - -- By the hypothesis, we may find a finite generating set for each `Sᵣ`. This set can then be - -- lifted into `R` by multiplying a sufficiently large power of `r`. I claim that the union of - -- these generates `S`. - constructor - replace H := fun r => (H r).1 - choose s₁ s₂ using H - let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x) - use s.attach.biUnion sf - rw [Submodule.span_attach_biUnion, eq_top_iff] - -- It suffices to show that `r ^ n • x ∈ span T` for each `r : s`, since `{ r ^ n }` spans `R`. - -- This then follows from the fact that each `x : R` is a linear combination of the generating set - -- of `Sᵣ`. By multiplying a sufficiently large power of `r`, we can cancel out the `r`s in the - -- denominators of both the generating set and the coefficients. - rintro x - - apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _ - intro r - obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := - multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R)) - (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x) - (by rw [s₂ r]; trivial) - dsimp only at hn₁ - rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁ - obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := - IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R)) - (Localization.Away (f r)) _ (s₁ r) hn₁ - rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂ - simp_rw [Submonoid.map_powers] at hn₂ - use n₂ + n₁ - exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂ - -end Finite - -section FiniteType - -theorem localization_finiteType : RingHom.LocalizationPreserves @RingHom.FiniteType := by - introv R hf - -- mirrors the proof of `localization_map_finite` - letI := f.toAlgebra - letI := ((algebraMap S S').comp f).toAlgebra - let f' : R' →+* S' := IsLocalization.map S' f (Submonoid.le_comap_map M) - letI := f'.toAlgebra - haveI : IsScalarTower R R' S' := - IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp M.le_comap_map).symm - let fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') fun c x => RingHom.map_mul _ _ _ - obtain ⟨T, hT⟩ := id hf - use T.image (algebraMap S S') - rw [eq_top_iff] - rintro x - - obtain ⟨y, ⟨_, ⟨r, hr, rfl⟩⟩, rfl⟩ := IsLocalization.mk'_surjective (M.map f) x - rw [IsLocalization.mk'_eq_mul_mk'_one, mul_comm, Finset.coe_image] - have hy : y ∈ Algebra.adjoin R (T : Set S) := by rw [hT]; trivial - replace hy : algebraMap S S' y ∈ (Algebra.adjoin R (T : Set S)).map fₐ := - Subalgebra.mem_map.mpr ⟨_, hy, rfl⟩ - rw [fₐ.map_adjoin T] at hy - have H : Algebra.adjoin R (algebraMap S S' '' T) ≤ - (Algebra.adjoin R' (algebraMap S S' '' T)).restrictScalars R := by - rw [Algebra.adjoin_le_iff]; exact Algebra.subset_adjoin - convert (Algebra.adjoin R' (algebraMap S S' '' T)).smul_mem (H hy) - (IsLocalization.mk' R' (1 : R) ⟨r, hr⟩) using 1 - rw [Algebra.smul_def] - erw [IsLocalization.map_mk' M.le_comap_map] - rw [map_one] - -theorem localization_away_map_finiteType (r : R) [IsLocalization.Away r R'] - [IsLocalization.Away (f r) S'] (hf : f.FiniteType) : - (IsLocalization.Away.map R' S' f r).FiniteType := - localization_finiteType.away r hf - -variable {S'} - -/-- Let `S` be an `R`-algebra, `M` a submonoid of `S`, `S' = M⁻¹S`. -Suppose the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`, -and `A` is an `R`-subalgebra of `S` containing both `M` and the numerators of `s`. -Then, there exists some `m : M` such that `m • x` falls in `A`. --/ -theorem IsLocalization.exists_smul_mem_of_mem_adjoin [Algebra R S] [Algebra R S'] - [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S'] (x : S) (s : Finset S') - (A : Subalgebra R S) (hA₁ : (IsLocalization.finsetIntegerMultiple M s : Set S) ⊆ A) - (hA₂ : M ≤ A.toSubmonoid) (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) : - ∃ m : M, m • x ∈ A := by - let g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S' - let y := IsLocalization.commonDenomOfFinset M s - have hx₁ : (y : S) • (s : Set S') = g '' _ := - (IsLocalization.finsetIntegerMultiple_image _ s).symm - obtain ⟨n, hn⟩ := - Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin (y : S) (s : Set S') (A.map g) - (by rw [hx₁]; exact Set.image_subset _ hA₁) hx (Set.mem_image_of_mem _ (hA₂ y.2)) - obtain ⟨x', hx', hx''⟩ := hn n (le_of_eq rfl) - rw [Algebra.smul_def, ← _root_.map_mul] at hx'' - obtain ⟨a, ha₂⟩ := (IsLocalization.eq_iff_exists M S').mp hx'' - use a * y ^ n - convert A.mul_mem hx' (hA₂ a.prop) using 1 - rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂, - mul_comm] - -/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`. -If the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`, -then there exists some `m : M` such that `m • x` falls in the -adjoin of `IsLocalization.finsetIntegerMultiple _ s` over `R`. --/ -theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple [Algebra R S] [Algebra R S'] - [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S') - (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) : - ∃ m : M, m • x ∈ - Algebra.adjoin R - (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) := by - obtain ⟨⟨_, a, ha, rfl⟩, e⟩ := - IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _) - Algebra.subset_adjoin (by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx - refine ⟨⟨a, ha⟩, ?_⟩ - simpa only [Submonoid.smul_def, algebraMap_smul] using e - -theorem finiteType_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.FiniteType := by - rw [RingHom.ofLocalizationSpan_iff_finite] - introv R hs H - -- mirrors the proof of `finite_ofLocalizationSpan` - letI := f.toAlgebra - letI := fun r : s => (Localization.awayMap f r).toAlgebra - have : ∀ r : s, - IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S)) (Localization.Away (f r)) := - by intro r; rw [Submonoid.map_powers]; exact Localization.isLocalization - haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) := - fun r => IsScalarTower.of_algebraMap_eq' - (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm - constructor - replace H := fun r => (H r).1 - choose s₁ s₂ using H - let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x) - use s.attach.biUnion sf - convert (Algebra.adjoin_attach_biUnion (R := R) sf).trans _ - rw [eq_top_iff] - rintro x - - apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem - _ hs _ _ - intro r - obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := - multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R)) - (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) - (algebraMap S (Localization.Away (f r)) x) (by rw [s₂ r]; trivial) - rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁ - obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := - IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁ - rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂ - simp_rw [Submonoid.map_powers] at hn₂ - use n₂ + n₁ - exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂ - -end FiniteType - -section IsIntegallyClosed - -/-- `IsIntegrallyClosed` is a local property. -/ -theorem isIntegrallyClosed_ofLocalizationMaximal : - OfLocalizationMaximal fun R _ ↦ ([IsDomain R] → IsIntegrallyClosed R) := - fun _ _ h _ ↦ IsIntegrallyClosed.of_localization_maximal fun p _ hpm ↦ h p hpm - -end IsIntegallyClosed diff --git a/Mathlib/RingTheory/LocalProperties/Basic.lean b/Mathlib/RingTheory/LocalProperties/Basic.lean new file mode 100644 index 0000000000000..0141196dfed77 --- /dev/null +++ b/Mathlib/RingTheory/LocalProperties/Basic.lean @@ -0,0 +1,332 @@ +/- +Copyright (c) 2021 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.RingTheory.Localization.Submodule +import Mathlib.RingTheory.RingHomProperties + +/-! +# Local properties of commutative rings + +In this file, we define local properties in general. + +## 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 `Rₘ` for all maximal `m`. +* `P_of_localization_prime` : `P` holds for `R` if `P` holds for `Rₘ` for all prime `m`. +* `P_ofLocalizationSpan` : `P` holds for `R` if given a spanning set `{fᵢ}`, `P` holds for all + `R_{fᵢ}`. + +## Main definitions + +* `LocalizationPreserves` : A property `P` of comm rings is said to be preserved by localization + if `P` holds for `M⁻¹R` whenever `P` holds for `R`. +* `OfLocalizationMaximal` : A property `P` of comm rings satisfies `OfLocalizationMaximal` + if `P` holds for `R` whenever `P` holds for `Rₘ` for all maximal ideal `m`. +* `RingHom.LocalizationPreserves` : 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`. +* `RingHom.OfLocalizationSpan` : A property `P` of ring homs satisfies + `RingHom.OfLocalizationSpan` if `P` holds for `R →+* S` whenever there exists a + set `{ r }` that spans `R` such that `P` holds for `Rᵣ →+* Sᵣ`. + +## Main results + +* The triviality of an ideal or an element: + `ideal_eq_bot_of_localization`, `eq_zero_of_localization` + +-/ + +open scoped Pointwise Classical + +universe u + +variable {R S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (f : R →+* S) +variable (N : Submonoid S) (R' S' : Type u) [CommRing R'] [CommRing S'] +variable [Algebra R R'] [Algebra S S'] + +section Properties + +section CommRing + +variable (P : ∀ (R : Type u) [CommRing R], Prop) + +/-- A property `P` of comm rings is said to be preserved by localization + if `P` holds for `M⁻¹R` whenever `P` holds for `R`. -/ +def LocalizationPreserves : Prop := + ∀ {R : Type u} [hR : CommRing R] (M : Submonoid R) (S : Type u) [hS : CommRing S] [Algebra R S] + [IsLocalization M S], @P R hR → @P S hS + +/-- A property `P` of comm rings satisfies `OfLocalizationMaximal` + if `P` holds for `R` whenever `P` holds for `Rₘ` for all maximal ideal `m`. -/ +def OfLocalizationMaximal : Prop := + ∀ (R : Type u) [CommRing R], + (∀ (J : Ideal R) (_ : J.IsMaximal), P (Localization.AtPrime J)) → P R + +end CommRing + +section RingHom + +variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S] (_ : R →+* S), Prop) + +/-- A property `P` of ring homs is said to contain identities if `P` holds +for the identity homomorphism of every ring. -/ +def RingHom.ContainsIdentities := ∀ (R : Type u) [CommRing R], P (RingHom.id R) + +/-- 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 RingHom.LocalizationPreserves := + ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (M : Submonoid R) (R' S' : Type u) + [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] [IsLocalization M R'] + [IsLocalization (M.map f) S'], + P f → P (IsLocalization.map S' f (Submonoid.le_comap_map M) : R' →+* S') + +/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan` +if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `R` such that +`P` holds for `Rᵣ →+* Sᵣ`. + +Note that this is equivalent to `RingHom.OfLocalizationSpan` via +`RingHom.ofLocalizationSpan_iff_finite`, but this is easier to prove. -/ +def RingHom.OfLocalizationFiniteSpan := + ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Finset R) + (_ : Ideal.span (s : Set R) = ⊤) (_ : ∀ r : s, P (Localization.awayMap f r)), P f + +/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan` +if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `R` such that +`P` holds for `Rᵣ →+* Sᵣ`. + +Note that this is equivalent to `RingHom.OfLocalizationFiniteSpan` via +`RingHom.ofLocalizationSpan_iff_finite`, but this has less restrictions when applying. -/ +def RingHom.OfLocalizationSpan := + ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (_ : Ideal.span s = ⊤) + (_ : ∀ r : s, P (Localization.awayMap f r)), P f + +/-- A property `P` of ring homs satisfies `RingHom.HoldsForLocalizationAway` + if `P` holds for each localization map `R →+* Rᵣ`. -/ +def RingHom.HoldsForLocalizationAway : Prop := + ∀ ⦃R : Type u⦄ (S : Type u) [CommRing R] [CommRing S] [Algebra R S] (r : R) + [IsLocalization.Away r S], P (algebraMap R S) + +/-- A property `P` of ring homs satisfies `RingHom.StableUnderCompositionWithLocalizationAway` +if whenever `P` holds for `f` it also holds for the composition with +localization maps on the left and on the right. -/ +def RingHom.StableUnderCompositionWithLocalizationAway : Prop := + (∀ ⦃R S : Type u⦄ (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra S T] (s : S) + [IsLocalization.Away s T] (f : R →+* S), P f → P ((algebraMap S T).comp f)) ∧ + ∀ ⦃R : Type u⦄ (S : Type u) ⦃T : Type u⦄ [CommRing R] [CommRing S] [CommRing T] [Algebra R S] + (r : R) [IsLocalization.Away r S] (f : S →+* T), P f → P (f.comp (algebraMap R S)) + +/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpanTarget` +if `P` holds for `R →+* S` whenever there exists a finite set `{ r }` that spans `S` such that +`P` holds for `R →+* Sᵣ`. + +Note that this is equivalent to `RingHom.OfLocalizationSpanTarget` via +`RingHom.ofLocalizationSpanTarget_iff_finite`, but this is easier to prove. -/ +def RingHom.OfLocalizationFiniteSpanTarget : Prop := + ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Finset S) + (_ : Ideal.span (s : Set S) = ⊤) + (_ : ∀ r : s, P ((algebraMap S (Localization.Away (r : S))).comp f)), P f + +/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationSpanTarget` +if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `S` such that +`P` holds for `R →+* Sᵣ`. + +Note that this is equivalent to `RingHom.OfLocalizationFiniteSpanTarget` via +`RingHom.ofLocalizationSpanTarget_iff_finite`, but this has less restrictions when applying. -/ +def RingHom.OfLocalizationSpanTarget : Prop := + ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (_ : Ideal.span s = ⊤) + (_ : ∀ r : s, P ((algebraMap S (Localization.Away (r : S))).comp f)), P f + +/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationPrime` +if `P` holds for `R` whenever `P` holds for `Rₘ` for all prime ideals `p`. -/ +def RingHom.OfLocalizationPrime : Prop := + ∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S), + (∀ (J : Ideal S) (_ : J.IsPrime), P (Localization.localRingHom _ 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 RingHom.PropertyIsLocal : Prop where + LocalizationPreserves : RingHom.LocalizationPreserves @P + OfLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget @P + StableUnderCompositionWithLocalizationAway : RingHom.StableUnderCompositionWithLocalizationAway @P + +theorem RingHom.ofLocalizationSpan_iff_finite : + RingHom.OfLocalizationSpan @P ↔ RingHom.OfLocalizationFiniteSpan @P := by + delta RingHom.OfLocalizationSpan RingHom.OfLocalizationFiniteSpan + apply forall₅_congr + -- TODO: Using `refine` here breaks `resetI`. + intros + constructor + · intro h s; exact h s + · intro h s hs hs' + obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs + exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩ + +theorem RingHom.ofLocalizationSpanTarget_iff_finite : + RingHom.OfLocalizationSpanTarget @P ↔ RingHom.OfLocalizationFiniteSpanTarget @P := by + delta RingHom.OfLocalizationSpanTarget RingHom.OfLocalizationFiniteSpanTarget + apply forall₅_congr + -- TODO: Using `refine` here breaks `resetI`. + intros + constructor + · intro h s; exact h s + · intro h s hs hs' + obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs + exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩ + +theorem RingHom.HoldsForLocalizationAway.of_bijective + (H : RingHom.HoldsForLocalizationAway P) (hf : Function.Bijective f) : + P f := by + letI := f.toAlgebra + have := IsLocalization.at_units (.powers (1 : R)) (by simp) + have := IsLocalization.isLocalization_of_algEquiv (.powers (1 : R)) + (AlgEquiv.ofBijective (Algebra.ofId R S) hf) + exact H _ 1 + +variable {P f R' S'} + +lemma RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway + (hPc : RingHom.StableUnderComposition P) (hPl : HoldsForLocalizationAway P) : + StableUnderCompositionWithLocalizationAway P := by + constructor + · introv _ hf + exact hPc _ _ hf (hPl T s) + · introv _ hf + exact hPc _ _ (hPl S r) hf + +lemma RingHom.HoldsForLocalizationAway.containsIdentities (hPl : HoldsForLocalizationAway P) : + ContainsIdentities P := by + introv R + exact hPl.of_bijective _ _ Function.bijective_id + +theorem RingHom.PropertyIsLocal.respectsIso (hP : RingHom.PropertyIsLocal @P) : + RingHom.RespectsIso @P := by + constructor + · intro R S T _ _ _ f e hf + letI := e.toRingHom.toAlgebra + have : IsLocalization.Away (1 : S) T := + IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective + exact hP.StableUnderCompositionWithLocalizationAway.left T (1 : S) f hf + · intro R S T _ _ _ f e hf + letI := e.toRingHom.toAlgebra + have : IsLocalization.Away (1 : R) S := + IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective + exact hP.StableUnderCompositionWithLocalizationAway.right S (1 : R) f hf + +-- Almost all arguments are implicit since this is not intended to use mid-proof. +theorem RingHom.LocalizationPreserves.away (H : RingHom.LocalizationPreserves @P) (r : R) + [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] (hf : P f) : + P (IsLocalization.Away.map R' S' f r) := by + have : IsLocalization ((Submonoid.powers r).map f) S' := by rw [Submonoid.map_powers]; assumption + exact H f (Submonoid.powers r) R' S' hf + +lemma RingHom.PropertyIsLocal.HoldsForLocalizationAway (hP : RingHom.PropertyIsLocal @P) + (hPi : ContainsIdentities P) : + RingHom.HoldsForLocalizationAway @P := by + introv R _ + have : algebraMap R S = (algebraMap R S).comp (RingHom.id R) := by simp + rw [this] + apply (hP.StableUnderCompositionWithLocalizationAway).left S r + apply hPi + +theorem RingHom.PropertyIsLocal.ofLocalizationSpan (hP : RingHom.PropertyIsLocal @P) : + RingHom.OfLocalizationSpan @P := by + introv R hs hs' + apply_fun Ideal.map f at hs + rw [Ideal.map_span, Ideal.map_top] at hs + apply hP.OfLocalizationSpanTarget _ _ hs + rintro ⟨_, r, hr, rfl⟩ + rw [← IsLocalization.map_comp (M := Submonoid.powers r) (S := Localization.Away r) + (T := Submonoid.powers (f r))] + apply hP.StableUnderCompositionWithLocalizationAway.right _ r + exact hs' ⟨r, hr⟩ + +lemma RingHom.OfLocalizationSpanTarget.ofIsLocalization + (hP : RingHom.OfLocalizationSpanTarget P) (hP' : RingHom.RespectsIso P) + {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (hs : Ideal.span s = ⊤) + (hT : ∀ r : s, ∃ (T : Type u) (_ : CommRing T) (_ : Algebra S T) + (_ : IsLocalization.Away (r : S) T), P ((algebraMap S T).comp f)) : P f := by + apply hP _ s hs + intros r + obtain ⟨T, _, _, _, hT⟩ := hT r + convert hP'.1 _ + (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT + rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_eq_coe, + AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp, + RingHom.comp_id] + +end RingHom + +end Properties + +section Ideal + +open scoped nonZeroDivisors + +/-- Let `I J : Ideal R`. If the localization of `I` at each maximal ideal `P` is included in +the localization of `J` at `P`, then `I ≤ J`. -/ +theorem Ideal.le_of_localization_maximal {I J : Ideal R} + (h : ∀ (P : Ideal R) (hP : P.IsMaximal), + Ideal.map (algebraMap R (Localization.AtPrime P)) I ≤ + Ideal.map (algebraMap R (Localization.AtPrime P)) J) : + I ≤ J := by + intro x hx + suffices J.colon (Ideal.span {x}) = ⊤ by + simpa using Submodule.mem_colon.mp + (show (1 : R) ∈ J.colon (Ideal.span {x}) from this.symm ▸ Submodule.mem_top) x + (Ideal.mem_span_singleton_self x) + refine Not.imp_symm (J.colon (Ideal.span {x})).exists_le_maximal ?_ + push_neg + intro P hP le + obtain ⟨⟨⟨a, ha⟩, ⟨s, hs⟩⟩, eq⟩ := + (IsLocalization.mem_map_algebraMap_iff P.primeCompl _).mp (h P hP (Ideal.mem_map_of_mem _ hx)) + rw [← _root_.map_mul, ← sub_eq_zero, ← map_sub] at eq + obtain ⟨⟨m, hm⟩, eq⟩ := (IsLocalization.map_eq_zero_iff P.primeCompl _ _).mp eq + refine hs ((hP.isPrime.mem_or_mem (le (Ideal.mem_colon_singleton.mpr ?_))).resolve_right hm) + simp only [Subtype.coe_mk, mul_sub, sub_eq_zero, mul_comm x s, mul_left_comm] at eq + simpa only [mul_assoc, eq] using J.mul_mem_left m ha + +/-- Let `I J : Ideal R`. If the localization of `I` at each maximal ideal `P` is equal to +the localization of `J` at `P`, then `I = J`. -/ +theorem Ideal.eq_of_localization_maximal {I J : Ideal R} + (h : ∀ (P : Ideal R) (_ : P.IsMaximal), + Ideal.map (algebraMap R (Localization.AtPrime P)) I = + Ideal.map (algebraMap R (Localization.AtPrime P)) J) : + I = J := + le_antisymm (Ideal.le_of_localization_maximal fun P hP => (h P hP).le) + (Ideal.le_of_localization_maximal fun P hP => (h P hP).ge) + +/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/ +theorem ideal_eq_bot_of_localization' (I : Ideal R) + (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), + Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) : + I = ⊥ := + Ideal.eq_of_localization_maximal fun P hP => by simpa using h P hP + +-- TODO: This proof should work for all modules, once we have enough material on submodules of +-- localized modules. +/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/ +theorem ideal_eq_bot_of_localization (I : Ideal R) + (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), + IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥) : + I = ⊥ := + ideal_eq_bot_of_localization' _ fun P hP => + (Ideal.map_eq_bot_iff_le_ker _).mpr fun x hx => by + rw [RingHom.mem_ker, ← Submodule.mem_bot R, ← h P hP, IsLocalization.mem_coeSubmodule] + exact ⟨x, hx, rfl⟩ + +theorem eq_zero_of_localization (r : R) + (h : ∀ (J : Ideal R) (hJ : J.IsMaximal), algebraMap R (Localization.AtPrime J) r = 0) : + r = 0 := by + rw [← Ideal.span_singleton_eq_bot] + apply ideal_eq_bot_of_localization + intro J hJ + delta IsLocalization.coeSubmodule + erw [Submodule.map_span, Submodule.span_eq_bot] + rintro _ ⟨_, h', rfl⟩ + cases Set.mem_singleton_iff.mpr h' + exact h J hJ + +end Ideal diff --git a/Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean b/Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean new file mode 100644 index 0000000000000..3753f3c70b5be --- /dev/null +++ b/Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2024 Yongle Hu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yongle Hu +-/ +import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed +import Mathlib.RingTheory.LocalProperties.Basic +import Mathlib.RingTheory.Localization.LocalizationLocalization + +/-! +# `IsIntegrallyClosed` is a local property + +In this file, we prove that `IsIntegrallyClosed` is a local property. + +## Main results + +* `IsIntegrallyClosed.of_localization_maximal` : An integral domain `R` is integral closed + if `Rₘ` is integral closed for any maximal ideal `m` of `R`. + +## TODO + +Prove that `IsIntegrallyClosed` is preserved by localization + +-/ + +open scoped nonZeroDivisors + +open Localization Ideal IsLocalization + +/-- An integral domain `R` is integral closed if `Rₘ` is integral closed + for any maximal ideal `m` of `R`. -/ +theorem IsIntegrallyClosed.of_localization_maximal {R : Type*} [CommRing R] [IsDomain R] + (h : ∀ p : Ideal R, p ≠ ⊥ → [p.IsMaximal] → IsIntegrallyClosed (Localization.AtPrime p)) : + IsIntegrallyClosed R := by + by_cases hf : IsField R + · exact hf.toField.instIsIntegrallyClosed + apply (isIntegrallyClosed_iff (FractionRing R)).mpr + rintro ⟨x⟩ hx + let I : Ideal R := span {x.2.1} / span {x.1} + have h1 : 1 ∈ I := by + apply I.eq_top_iff_one.mp + by_contra hn + rcases I.exists_le_maximal hn with ⟨p, hpm, hpi⟩ + have hic := h p (Ring.ne_bot_of_isMaximal_of_not_isField hpm hf) + have hxp : IsIntegral (Localization.AtPrime p) (mk x.1 x.2) := hx.tower_top + /- `x.1 / x.2.1 ∈ Rₚ` since it is integral over `Rₚ` and `Rₚ` is integrally closed. + More precisely, `x.1 / x.2.1 = y.1 / y.2.1` where `y.1, y.2.1 ∈ R` and `y.2.1 ∉ p`. -/ + rcases (isIntegrallyClosed_iff (FractionRing R)).mp hic hxp with ⟨⟨y⟩, hy⟩ + /- `y.2.1 ∈ I` since for all `a ∈ Ideal.span {x.1}`, say `a = b * x.1`, + we have `y.2 * a = b * x.1 * y.2 = b * y.1 * x.2.1 ∈ Ideal.span {x.2.1}`. -/ + have hyi : y.2.1 ∈ I := by + intro a ha + rcases mem_span_singleton'.mp ha with ⟨b, hb⟩ + apply mem_span_singleton'.mpr ⟨b * y.1, _⟩ + rw [← hb, ← mul_assoc, mul_comm y.2.1 b, mul_assoc, mul_assoc] + exact congrArg (HMul.hMul b) <| (mul_comm y.1 x.2.1).trans <| + NoZeroSMulDivisors.algebraMap_injective R (Localization R⁰) <| mk'_eq_iff_eq.mp <| + (mk'_eq_algebraMap_mk'_of_submonoid_le _ _ p.primeCompl_le_nonZeroDivisors y.1 y.2).trans + <| show algebraMap (Localization.AtPrime p) _ (mk' _ y.1 y.2) = mk' _ x.1 x.2 + by simpa only [← mk_eq_mk', ← hy] using by rfl + -- `y.2.1 ∈ I` implies `y.2.1 ∈ p` since `I ⊆ p`, which contradicts to the choice of `y`. + exact y.2.2 (hpi hyi) + rcases mem_span_singleton'.mp (h1 x.1 (mem_span_singleton_self x.1)) with ⟨y, hy⟩ + exact ⟨y, (eq_mk'_of_mul_eq (hy.trans (one_mul x.1))).trans (mk_eq_mk'_apply x.1 x.2).symm⟩ + +theorem isIntegrallyClosed_ofLocalizationMaximal : + OfLocalizationMaximal fun R _ => ([IsDomain R] → IsIntegrallyClosed R) := + fun _ _ h _ ↦ IsIntegrallyClosed.of_localization_maximal fun p _ hpm ↦ h p hpm diff --git a/Mathlib/RingTheory/LocalProperties/Reduced.lean b/Mathlib/RingTheory/LocalProperties/Reduced.lean new file mode 100644 index 0000000000000..65df178848887 --- /dev/null +++ b/Mathlib/RingTheory/LocalProperties/Reduced.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2021 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import Mathlib.RingTheory.LocalProperties.Basic + +/-! +# `IsReduced` is a local property + +In this file, we prove that `IsReduced` is a local property. + +## Main results + +Let `R` be a commutative ring, `M` be a submonoid of `R`. + +* `isReduced_localizationPreserves` : `M⁻¹R` is reduced if `R` is reduced. +* `isReduced_ofLocalizationMaximal` : `R` is reduced if `Rₘ` is reduced for all maximal ideal `m`. + +-/ + +/-- `M⁻¹R` is reduced if `R` is reduced. -/ +theorem isReduced_localizationPreserves : LocalizationPreserves fun R hR => IsReduced R := by + introv R _ _ + constructor + rintro x ⟨_ | n, e⟩ + · simpa using congr_arg (· * x) e + obtain ⟨⟨y, m⟩, hx⟩ := IsLocalization.surj M x + dsimp only at hx + let hx' := congr_arg (· ^ n.succ) hx + simp only [mul_pow, e, zero_mul, ← RingHom.map_pow] at hx' + rw [← (algebraMap R S).map_zero] at hx' + obtain ⟨m', hm'⟩ := (IsLocalization.eq_iff_exists M S).mp hx' + apply_fun (· * (m' : R) ^ n) at hm' + simp only [mul_assoc, zero_mul, mul_zero] at hm' + rw [← mul_left_comm, ← pow_succ', ← mul_pow] at hm' + replace hm' := IsNilpotent.eq_zero ⟨_, hm'.symm⟩ + rw [← (IsLocalization.map_units S m).mul_left_inj, hx, zero_mul, + IsLocalization.map_eq_zero_iff M] + exact ⟨m', by rw [← hm', mul_comm]⟩ + +instance {R : Type*} [CommRing R] (M : Submonoid R) [IsReduced R] : IsReduced (Localization M) := + isReduced_localizationPreserves M _ inferInstance + +/-- `R` is reduced if `Rₘ` is reduced for all maximal ideal `m`. -/ +theorem isReduced_ofLocalizationMaximal : OfLocalizationMaximal fun R hR => IsReduced R := by + introv R h + constructor + intro x hx + apply eq_zero_of_localization + intro J hJ + specialize h J hJ + exact (hx.map <| algebraMap R <| Localization.AtPrime J).eq_zero diff --git a/Mathlib/RingTheory/Localization/Finiteness.lean b/Mathlib/RingTheory/Localization/Finiteness.lean index e14b622040c88..ab340bfec9330 100644 --- a/Mathlib/RingTheory/Localization/Finiteness.lean +++ b/Mathlib/RingTheory/Localization/Finiteness.lean @@ -5,7 +5,7 @@ Authors: Christian Merten -/ import Mathlib.Algebra.Module.LocalizedModuleIntegers import Mathlib.RingTheory.Localization.Algebra -import Mathlib.RingTheory.LocalProperties +import Mathlib.RingTheory.RingHom.Finite /-! diff --git a/Mathlib/RingTheory/RingHom/Finite.lean b/Mathlib/RingTheory/RingHom/Finite.lean index 164f6abef7265..40a5dbe72b097 100644 --- a/Mathlib/RingTheory/RingHom/Finite.lean +++ b/Mathlib/RingTheory/RingHom/Finite.lean @@ -3,12 +3,22 @@ Copyright (c) 2021 Andrew Yang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ -import Mathlib.RingTheory.RingHomProperties +import Mathlib.RingTheory.LocalProperties.Basic +import Mathlib.RingTheory.Localization.Integer /-! # The meta properties of finite ring homomorphisms. +## Main results + +Let `R` be a commutative ring, `S` is an `R`-algebra, `M` be a submonoid of `R`. + +* `finite_localizationPreserves` : If `S` is a finite `R`-algebra, then `S' = M⁻¹S` is a + finite `R' = M⁻¹R`-algebra. +* `finite_ofLocalizationSpan` : `S` is a finite `R`-algebra if there exists + a set `{ r }` that spans `R` such that `Sᵣ` is a finite `Rᵣ`-algebra. + -/ @@ -38,3 +48,186 @@ theorem finite_stableUnderBaseChange : StableUnderBaseChange @Finite := by exact inferInstance end RingHom + +open scoped Pointwise Classical + +universe u + +variable {R S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (f : R →+* S) +variable (R' S' : Type u) [CommRing R'] [CommRing S'] +variable [Algebra R R'] [Algebra S S'] + +lemma Module.Finite_of_isLocalization (R S Rₚ Sₚ) [CommSemiring R] [CommRing S] [CommRing Rₚ] + [CommRing Sₚ] [Algebra R S] [Algebra R Rₚ] [Algebra R Sₚ] [Algebra S Sₚ] [Algebra Rₚ Sₚ] + [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ] + [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ] [hRS : Module.Finite R S] : + Module.Finite Rₚ Sₚ := by + classical + have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ + (algebraMap R S) (Submonoid.le_comap_map M) := by + apply IsLocalization.ringHom_ext M + simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq] + -- We claim that if `S` is generated by `T` as an `R`-module, + -- then `S'` is generated by `T` as an `R'`-module. + obtain ⟨T, hT⟩ := hRS + use T.image (algebraMap S Sₚ) + rw [eq_top_iff] + rintro x - + -- By the hypotheses, for each `x : S'`, we have `x = y / (f r)` for some `y : S` and `r : M`. + -- Since `S` is generated by `T`, the image of `y` should fall in the span of the image of `T`. + obtain ⟨y, ⟨_, ⟨r, hr, rfl⟩⟩, rfl⟩ := + IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x + rw [IsLocalization.mk'_eq_mul_mk'_one, mul_comm, Finset.coe_image] + have hy : y ∈ Submodule.span R ↑T := by rw [hT]; trivial + replace hy : algebraMap S Sₚ y ∈ Submodule.map (IsScalarTower.toAlgHom R S Sₚ).toLinearMap + (Submodule.span R (T : Set S)) := Submodule.mem_map_of_mem +-- -- Note: #8386 had to specify the value of `f` below + (f := (IsScalarTower.toAlgHom R S Sₚ).toLinearMap) hy + rw [Submodule.map_span (IsScalarTower.toAlgHom R S Sₚ).toLinearMap T] at hy + have H : Submodule.span R (algebraMap S Sₚ '' T) ≤ + (Submodule.span Rₚ (algebraMap S Sₚ '' T)).restrictScalars R := by + rw [Submodule.span_le]; exact Submodule.subset_span + -- Now, since `y ∈ span T`, and `(f r)⁻¹ ∈ R'`, `x / (f r)` is in `span T` as well. + convert (Submodule.span Rₚ (algebraMap S Sₚ '' T)).smul_mem + (IsLocalization.mk' Rₚ (1 : R) ⟨r, hr⟩) (H hy) using 1 + rw [Algebra.smul_def, this, IsLocalization.map_mk', map_one] + +/-- If `S` is a finite `R`-algebra, then `S' = M⁻¹S` is a finite `R' = M⁻¹R`-algebra. -/ +theorem RingHom.finite_localizationPreserves : RingHom.LocalizationPreserves @RingHom.Finite := by + introv R hf + letI := f.toAlgebra + letI := ((algebraMap S S').comp f).toAlgebra + let f' : R' →+* S' := IsLocalization.map S' f (Submonoid.le_comap_map M) + letI := f'.toAlgebra + have : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq' + (IsLocalization.map_comp M.le_comap_map).symm + have : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' rfl + have : IsLocalization (Algebra.algebraMapSubmonoid S M) S' := by + rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra] + have : Module.Finite R S := hf + apply Module.Finite_of_isLocalization R S R' S' M + +theorem RingHom.localization_away_map_finite (r : R) [IsLocalization.Away r R'] + [IsLocalization.Away (f r) S'] (hf : f.Finite) : (IsLocalization.Away.map R' S' f r).Finite := + finite_localizationPreserves.away r hf + +/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`. +If the image of some `x : S` falls in the span of some finite `s ⊆ S'` over `R`, +then there exists some `m : M` such that `m • x` falls in the +span of `IsLocalization.finsetIntegerMultiple _ s` over `R`. +-/ +theorem IsLocalization.smul_mem_finsetIntegerMultiple_span [Algebra R S] [Algebra R S'] + [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S') + (hx : algebraMap S S' x ∈ Submodule.span R (s : Set S')) : + ∃ m : M, m • x ∈ + Submodule.span R + (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) := by + let g : S →ₐ[R] S' := + AlgHom.mk' (algebraMap S S') fun c x => by simp [Algebra.algebraMap_eq_smul_one] + -- We first obtain the `y' ∈ M` such that `s' = y' • s` is falls in the image of `S` in `S'`. + let y := IsLocalization.commonDenomOfFinset (M.map (algebraMap R S)) s + have hx₁ : (y : S) • (s : Set S') = g '' _ := + (IsLocalization.finsetIntegerMultiple_image _ s).symm + obtain ⟨y', hy', e : algebraMap R S y' = y⟩ := y.prop + have : algebraMap R S y' • (s : Set S') = y' • (s : Set S') := by + simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul] + rw [← e, this] at hx₁ + replace hx₁ := congr_arg (Submodule.span R) hx₁ + rw [Submodule.span_smul] at hx₁ + replace hx : _ ∈ y' • Submodule.span R (s : Set S') := Set.smul_mem_smul_set hx + rw [hx₁] at hx + erw [← _root_.map_smul g, ← Submodule.map_span (g : S →ₗ[R] S')] at hx + -- Since `x` falls in the span of `s` in `S'`, `y' • x : S` falls in the span of `s'` in `S'`. + -- That is, there exists some `x' : S` in the span of `s'` in `S` and `x' = y' • x` in `S'`. + -- Thus `a • (y' • x) = a • x' ∈ span s'` in `S` for some `a ∈ M`. + obtain ⟨x', hx', hx'' : algebraMap _ _ _ = _⟩ := hx + obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ := + (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx'' + use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M) + convert (Submodule.span R + (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s : Set S)).smul_mem + a hx' using 1 + convert ha₂.symm using 1 + · rw [Subtype.coe_mk, Submonoid.smul_def, Submonoid.coe_mul, ← smul_smul] + exact Algebra.smul_def _ _ + · exact Algebra.smul_def _ _ + +/-- If `M` is an `R' = S⁻¹R` module, and `x ∈ span R' s`, +then `t • x ∈ span R s` for some `t : S`. -/ +theorem multiple_mem_span_of_mem_localization_span + {N : Type*} [AddCommMonoid N] [Module R N] [Module R' N] + [IsScalarTower R R' N] [IsLocalization M R'] (s : Set N) (x : N) + (hx : x ∈ Submodule.span R' s) : ∃ (t : M), t • x ∈ Submodule.span R s := by + classical + obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx + rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N) + · exact ⟨t, Submodule.span_mono hss' ht⟩ + clear hx hss' s + induction s' using Finset.induction_on generalizing x + · use 1; simpa using hs' + rename_i a s _ hs + simp only [Finset.coe_insert, Finset.image_insert, Finset.coe_image, Subtype.coe_mk, + Submodule.mem_span_insert] at hs' ⊢ + rcases hs' with ⟨y, z, hz, rfl⟩ + rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩ + apply congrArg (fun x ↦ x • a) at e + simp only [algebraMap_smul] at e + rcases hs _ hz with ⟨t, ht⟩ + refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩ + rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def] + simp + rfl + +/-- If `S` is an `R' = M⁻¹R` algebra, and `x ∈ adjoin R' s`, +then `t • x ∈ adjoin R s` for some `t : M`. -/ +theorem multiple_mem_adjoin_of_mem_localization_adjoin [Algebra R' S] [Algebra R S] + [IsScalarTower R R' S] [IsLocalization M R'] (s : Set S) (x : S) + (hx : x ∈ Algebra.adjoin R' s) : ∃ t : M, t • x ∈ Algebra.adjoin R s := by + change ∃ t : M, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s) + change x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s) at hx + simp_rw [Algebra.adjoin_eq_span] at hx ⊢ + exact multiple_mem_span_of_mem_localization_span M R' _ _ hx + +/-- `S` is a finite `R`-algebra if there exists a set `{ r }` that + spans `R` such that `Sᵣ` is a finite `Rᵣ`-algebra. -/ +theorem RingHom.finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.Finite := by + rw [RingHom.ofLocalizationSpan_iff_finite] + introv R hs H + -- We first setup the instances + letI := f.toAlgebra + letI := fun r : s => (Localization.awayMap f r).toAlgebra + have : ∀ r : s, + IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S)) (Localization.Away (f r)) := + by intro r; rw [Submonoid.map_powers]; exact Localization.isLocalization + haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) := + fun r => IsScalarTower.of_algebraMap_eq' + (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm + -- By the hypothesis, we may find a finite generating set for each `Sᵣ`. This set can then be + -- lifted into `R` by multiplying a sufficiently large power of `r`. I claim that the union of + -- these generates `S`. + constructor + replace H := fun r => (H r).1 + choose s₁ s₂ using H + let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x) + use s.attach.biUnion sf + rw [Submodule.span_attach_biUnion, eq_top_iff] + -- It suffices to show that `r ^ n • x ∈ span T` for each `r : s`, since `{ r ^ n }` spans `R`. + -- This then follows from the fact that each `x : R` is a linear combination of the generating set + -- of `Sᵣ`. By multiplying a sufficiently large power of `r`, we can cancel out the `r`s in the + -- denominators of both the generating set and the coefficients. + rintro x - + apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _ + intro r + obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := + multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R)) + (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x) + (by rw [s₂ r]; trivial) + dsimp only at hn₁ + rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁ + obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := + IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R)) + (Localization.Away (f r)) _ (s₁ r) hn₁ + rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂ + simp_rw [Submonoid.map_powers] at hn₂ + use n₂ + n₁ + exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂ diff --git a/Mathlib/RingTheory/RingHom/FiniteType.lean b/Mathlib/RingTheory/RingHom/FiniteType.lean index 3f927873decf1..1e07b805c0c4a 100644 --- a/Mathlib/RingTheory/RingHom/FiniteType.lean +++ b/Mathlib/RingTheory/RingHom/FiniteType.lean @@ -4,26 +4,154 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ import Mathlib.RingTheory.FiniteStability -import Mathlib.RingTheory.LocalProperties import Mathlib.RingTheory.Localization.InvSubmonoid +import Mathlib.RingTheory.RingHom.Finite /-! # The meta properties of finite-type ring homomorphisms. -The main result is `RingHom.finiteType_is_local`. +## Main results + +Let `R` be a commutative ring, `S` is an `R`-algebra, `M` be a submonoid of `R`. + +* `finiteType_localizationPreserves` : If `S` is a finite type `R`-algebra, then `S' = M⁻¹S` is a + finite type `R' = M⁻¹R`-algebra. +* `finiteType_ofLocalizationSpan` : `S` is a finite type `R`-algebra if there exists + a set `{ r }` that spans `R` such that `Sᵣ` is a finite type `Rᵣ`-algebra. +*`RingHom.finiteType_is_local`: `RingHom.FiniteType` is a local property. -/ namespace RingHom -open scoped Pointwise TensorProduct +open scoped Pointwise TensorProduct Classical + +universe u + +variable {R S : Type u} [CommRing R] [CommRing S] (M : Submonoid R) (f : R →+* S) +variable (R' S' : Type u) [CommRing R'] [CommRing S'] +variable [Algebra R R'] [Algebra S S'] theorem finiteType_stableUnderComposition : StableUnderComposition @FiniteType := by introv R hf hg exact hg.comp hf +/-- If `S` is a finite type `R`-algebra, then `S' = M⁻¹S` is a finite type `R' = M⁻¹R`-algebra. -/ +theorem finiteType_localizationPreserves : RingHom.LocalizationPreserves @RingHom.FiniteType := by + introv R hf + -- mirrors the proof of `localization_map_finite` + letI := f.toAlgebra + letI := ((algebraMap S S').comp f).toAlgebra + let f' : R' →+* S' := IsLocalization.map S' f (Submonoid.le_comap_map M) + letI := f'.toAlgebra + haveI : IsScalarTower R R' S' := + IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp M.le_comap_map).symm + let fₐ : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') fun c x => RingHom.map_mul _ _ _ + obtain ⟨T, hT⟩ := hf + use T.image (algebraMap S S') + rw [eq_top_iff] + rintro x - + obtain ⟨y, ⟨_, ⟨r, hr, rfl⟩⟩, rfl⟩ := IsLocalization.mk'_surjective (M.map f) x + rw [IsLocalization.mk'_eq_mul_mk'_one, mul_comm, Finset.coe_image] + have hy : y ∈ Algebra.adjoin R (T : Set S) := by rw [hT]; trivial + replace hy : algebraMap S S' y ∈ (Algebra.adjoin R (T : Set S)).map fₐ := + Subalgebra.mem_map.mpr ⟨_, hy, rfl⟩ + rw [fₐ.map_adjoin T] at hy + have H : Algebra.adjoin R (algebraMap S S' '' T) ≤ + (Algebra.adjoin R' (algebraMap S S' '' T)).restrictScalars R := by + rw [Algebra.adjoin_le_iff]; exact Algebra.subset_adjoin + convert (Algebra.adjoin R' (algebraMap S S' '' T)).smul_mem (H hy) + (IsLocalization.mk' R' (1 : R) ⟨r, hr⟩) using 1 + rw [Algebra.smul_def] + erw [IsLocalization.map_mk' M.le_comap_map] + rw [map_one] + +theorem localization_away_map_finiteType (r : R) [IsLocalization.Away r R'] + [IsLocalization.Away (f r) S'] (hf : f.FiniteType) : + (IsLocalization.Away.map R' S' f r).FiniteType := + finiteType_localizationPreserves.away r hf + +variable {S'} + +/-- Let `S` be an `R`-algebra, `M` a submonoid of `S`, `S' = M⁻¹S`. +Suppose the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`, +and `A` is an `R`-subalgebra of `S` containing both `M` and the numerators of `s`. +Then, there exists some `m : M` such that `m • x` falls in `A`. +-/ +theorem IsLocalization.exists_smul_mem_of_mem_adjoin [Algebra R S] [Algebra R S'] + [IsScalarTower R S S'] (M : Submonoid S) [IsLocalization M S'] (x : S) (s : Finset S') + (A : Subalgebra R S) (hA₁ : (IsLocalization.finsetIntegerMultiple M s : Set S) ⊆ A) + (hA₂ : M ≤ A.toSubmonoid) (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) : + ∃ m : M, m • x ∈ A := by + let g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S' + let y := IsLocalization.commonDenomOfFinset M s + have hx₁ : (y : S) • (s : Set S') = g '' _ := + (IsLocalization.finsetIntegerMultiple_image _ s).symm + obtain ⟨n, hn⟩ := + Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin (y : S) (s : Set S') (A.map g) + (by rw [hx₁]; exact Set.image_subset _ hA₁) hx (Set.mem_image_of_mem _ (hA₂ y.2)) + obtain ⟨x', hx', hx''⟩ := hn n (le_of_eq rfl) + rw [Algebra.smul_def, ← _root_.map_mul] at hx'' + obtain ⟨a, ha₂⟩ := (IsLocalization.eq_iff_exists M S').mp hx'' + use a * y ^ n + convert A.mul_mem hx' (hA₂ a.prop) using 1 + rw [Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul, SubmonoidClass.coe_pow, mul_assoc, ← ha₂, + mul_comm] + +/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`. +If the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`, +then there exists some `m : M` such that `m • x` falls in the +adjoin of `IsLocalization.finsetIntegerMultiple _ s` over `R`. +-/ +theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple [Algebra R S] [Algebra R S'] + [IsScalarTower R S S'] [IsLocalization (M.map (algebraMap R S)) S'] (x : S) (s : Finset S') + (hx : algebraMap S S' x ∈ Algebra.adjoin R (s : Set S')) : + ∃ m : M, m • x ∈ + Algebra.adjoin R + (IsLocalization.finsetIntegerMultiple (M.map (algebraMap R S)) s : Set S) := by + obtain ⟨⟨_, a, ha, rfl⟩, e⟩ := + IsLocalization.exists_smul_mem_of_mem_adjoin (M.map (algebraMap R S)) x s (Algebra.adjoin R _) + Algebra.subset_adjoin (by rintro _ ⟨a, _, rfl⟩; exact Subalgebra.algebraMap_mem _ a) hx + refine ⟨⟨a, ha⟩, ?_⟩ + simpa only [Submonoid.smul_def, algebraMap_smul] using e + +theorem finiteType_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.FiniteType := by + rw [RingHom.ofLocalizationSpan_iff_finite] + introv R hs H + -- mirrors the proof of `finite_ofLocalizationSpan` + letI := f.toAlgebra + letI := fun r : s => (Localization.awayMap f r).toAlgebra + have : ∀ r : s, + IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S)) (Localization.Away (f r)) := + by intro r; rw [Submonoid.map_powers]; exact Localization.isLocalization + haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) := + fun r => IsScalarTower.of_algebraMap_eq' + (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm + constructor + replace H := fun r => (H r).1 + choose s₁ s₂ using H + let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x) + use s.attach.biUnion sf + convert (Algebra.adjoin_attach_biUnion (R := R) sf).trans _ + rw [eq_top_iff] + rintro x - + apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem + _ hs _ _ + intro r + obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := + multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R)) + (Localization.Away (r : R)) (s₁ r : Set (Localization.Away (f r))) + (algebraMap S (Localization.Away (f r)) x) (by rw [s₂ r]; trivial) + rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁ + obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := + IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : R)) _ (s₁ r) hn₁ + rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂ + simp_rw [Submonoid.map_powers] at hn₂ + use n₂ + n₁ + exact le_iSup (fun x : s => Algebra.adjoin R (sf x : Set S)) r hn₂ + theorem finiteType_holdsForLocalizationAway : HoldsForLocalizationAway @FiniteType := by introv R _ suffices Algebra.FiniteType R S by @@ -88,7 +216,7 @@ theorem finiteType_ofLocalizationSpanTarget : OfLocalizationSpanTarget @FiniteTy · rw [ht]; trivial theorem finiteType_is_local : PropertyIsLocal @FiniteType := - ⟨localization_finiteType, finiteType_ofLocalizationSpanTarget, + ⟨finiteType_localizationPreserves, finiteType_ofLocalizationSpanTarget, finiteType_stableUnderComposition.stableUnderCompositionWithLocalizationAway finiteType_holdsForLocalizationAway⟩ diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean index 11bc6f10f5271..b20eeffe62179 100644 --- a/Mathlib/RingTheory/RingHom/Surjective.lean +++ b/Mathlib/RingTheory/RingHom/Surjective.lean @@ -3,12 +3,22 @@ Copyright (c) 2022 Andrew Yang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Andrew Yang -/ -import Mathlib.RingTheory.LocalProperties +import Mathlib.RingTheory.LocalProperties.Basic /-! # The meta properties of surjective ring homomorphisms. +## Main results + +Let `R` be a commutative ring, `M` be a submonoid of `R`. + +* `surjective_localizationPreserves` : `M⁻¹R →+* M⁻¹S` is surjective if `R →+* S` is surjective. +* `surjective_ofLocalizationSpan` : `R →+* S` is surjective if there exists a set `{ r }` that + spans `R` such that `Rᵣ →+* Sᵣ` is surjective. +* `surjective_localRingHom_of_surjective` : A surjective ring homomorphism `R →+* S` induces a + surjective homomorphism `R_{f⁻¹(P)} →+* S_P` for every prime ideal `P` of `S`. + -/ @@ -18,6 +28,8 @@ open scoped TensorProduct open TensorProduct Algebra.TensorProduct +universe u + local notation "surjective" => fun {X Y : Type _} [CommRing X] [CommRing Y] => fun f : X →+* Y => Function.Surjective f @@ -40,28 +52,41 @@ theorem surjective_stableUnderBaseChange : StableUnderBaseChange surjective := b rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one] | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩ +/-- `M⁻¹R →+* M⁻¹S` is surjective if `R →+* S` is surjective. -/ +theorem surjective_localizationPreserves : + LocalizationPreserves surjective := by + introv R H x + obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (M.map f) x + obtain ⟨y, rfl⟩ := H x + use IsLocalization.mk' R' y ⟨s, hs⟩ + rw [IsLocalization.map_mk'] + +/-- `R →+* S` is surjective if there exists a set `{ r }` that spans `R` such that + `Rᵣ →+* Sᵣ` is surjective. -/ theorem surjective_ofLocalizationSpan : OfLocalizationSpan surjective := by - introv R hs H + introv R e H + rw [← Set.range_iff_surjective, Set.eq_univ_iff_forall] letI := f.toAlgebra - show Function.Surjective (Algebra.ofId R S) - rw [← Algebra.range_top_iff_surjective, eq_top_iff] - rintro x - - obtain ⟨l, hl⟩ := - (Finsupp.mem_span_iff_linearCombination R s 1).mp (show _ ∈ Ideal.span s by rw [hs]; trivial) - fapply - Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem _ l.support (fun x : s => f x) fun x : s => - f (l x) - · simp_rw [← _root_.map_mul, ← map_sum, ← f.map_one]; exact f.congr_arg hl - · exact fun _ => Set.mem_range_self _ - · exact fun _ => Set.mem_range_self _ - · intro r - obtain ⟨y, hy⟩ := H r (IsLocalization.mk' _ x (1 : Submonoid.powers (f r))) - obtain ⟨z, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (r : R)) y - erw [IsLocalization.map_mk', IsLocalization.eq] at hy - obtain ⟨⟨_, m, rfl⟩, hm⟩ := hy - refine ⟨m + n, ?_⟩ - dsimp at hm ⊢ - simp_rw [_root_.one_mul, ← _root_.mul_assoc, ← map_pow, ← f.map_mul, ← pow_add, map_pow] at hm - exact ⟨_, hm⟩ + intro x + apply Submodule.mem_of_span_eq_top_of_smul_pow_mem + (LinearMap.range (Algebra.linearMap R S)) s e + intro r + obtain ⟨a, e'⟩ := H r (algebraMap _ _ x) + obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (r : R)) a + erw [IsLocalization.map_mk'] at e' + rw [eq_comm, IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, Subtype.coe_mk, ← map_mul] at e' + obtain ⟨⟨_, n', rfl⟩, e''⟩ := (IsLocalization.eq_iff_exists (Submonoid.powers (f r)) _).mp e' + dsimp only at e'' + rw [mul_comm x, ← mul_assoc, ← map_pow, ← map_mul, ← map_mul, ← pow_add] at e'' + exact ⟨n' + n, _, e''.symm⟩ + +/-- A surjective ring homomorphism `R →+* S` induces a surjective homomorphism `R_{f⁻¹(P)} →+* S_P` +for every prime ideal `P` of `S`. -/ +theorem surjective_localRingHom_of_surjective {R S : Type u} [CommRing R] [CommRing S] + (f : R →+* S) (h : Function.Surjective f) (P : Ideal S) [P.IsPrime] : + Function.Surjective (Localization.localRingHom (P.comap f) P f rfl) := + have : IsLocalization (Submonoid.map f (Ideal.comap f P).primeCompl) (Localization.AtPrime P) := + (Submonoid.map_comap_eq_of_surjective h P.primeCompl).symm ▸ Localization.isLocalization + surjective_localizationPreserves _ _ _ _ h end RingHom