From 01c60b260407a412348eef39158ecc25dffb8e75 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Wed, 27 Jul 2022 11:14:36 +0000 Subject: [PATCH] feat(ring_theory/ring_hom/finite): Finite type is a local property (#15379) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- src/algebra/algebra/subalgebra/basic.lean | 35 +++++++++ src/ring_theory/adjoin/basic.lean | 27 +++++-- src/ring_theory/local_properties.lean | 93 ++++++++++++++++------- src/ring_theory/ring_hom/finite_type.lean | 92 ++++++++++++++++++++++ 4 files changed, 213 insertions(+), 34 deletions(-) create mode 100644 src/ring_theory/ring_hom/finite_type.lean diff --git a/src/algebra/algebra/subalgebra/basic.lean b/src/algebra/algebra/subalgebra/basic.lean index 542838a9a4a4d..e37628792f246 100644 --- a/src/algebra/algebra/subalgebra/basic.lean +++ b/src/algebra/algebra/subalgebra/basic.lean @@ -5,6 +5,8 @@ Authors: Kenny Lau, Yury Kudryashov -/ import algebra.algebra.basic import data.set.Union_lift +import linear_algebra.finsupp +import ring_theory.ideal.operations /-! # Subalgebras over Commutative Semiring @@ -1064,6 +1066,39 @@ set_like.ext' (set.centralizer_univ A) end centralizer +/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` in `S`, and `S'` a subalgebra of `S` that contains +`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that +`r ^ n • x ∈ M'` for some `n` for each `r : s`. -/ +lemma mem_of_span_eq_top_of_smul_pow_mem {S : Type*} [comm_ring S] [algebra R S] + (S' : subalgebra R S) (s : set S) (l : s →₀ S) (hs : finsupp.total s S S coe l = 1) + (hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) + (H : ∀ r : s, ∃ (n : ℕ), (r ^ n : S) • x ∈ S') : x ∈ S' := +begin + let s' : set S' := coe ⁻¹' s, + let e : s' ≃ s := ⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨⟨_, hs' x.2⟩, x.2⟩, λ ⟨⟨_, _⟩, _⟩, rfl, λ ⟨_, _⟩, rfl⟩, + let l' : s →₀ S' := ⟨l.support, λ x, ⟨_, hl x⟩, + λ _, finsupp.mem_support_iff.trans $ iff.not $ by { rw ← subtype.coe_inj, refl }⟩, + have : ideal.span s' = ⊤, + { rw [ideal.eq_top_iff_one, ideal.span, finsupp.mem_span_iff_total], + refine ⟨finsupp.equiv_map_domain e.symm l', subtype.ext $ eq.trans _ hs⟩, + rw finsupp.total_equiv_map_domain, + exact finsupp.apply_total _ (algebra.of_id S' S).to_linear_map _ _ }, + obtain ⟨s'', hs₁, hs₂⟩ := (ideal.span_eq_top_iff_finite _).mp this, + replace H : ∀ r : s'', ∃ (n : ℕ), (r ^ n : S) • x ∈ S' := λ r, H ⟨r, hs₁ r.2⟩, + choose n₁ n₂ using H, + let N := s''.attach.sup n₁, + have hs' := ideal.span_pow_eq_top _ hs₂ N, + have : ∀ {x : S}, x ∈ (algebra.of_id S' S).range.to_submodule ↔ x ∈ S' := + λ x, ⟨by { rintro ⟨x, rfl⟩, exact x.2 }, λ h, ⟨⟨x, h⟩, rfl⟩⟩, + rw ← this, + apply (algebra.of_id S' S).range.to_submodule.mem_of_span_top_of_smul_mem _ hs', + rintro ⟨_, r, hr, rfl⟩, + convert submodule.smul_mem _ (r ^ (N - n₁ ⟨r, hr⟩)) (this.mpr $ n₂ ⟨r, hr⟩) using 1, + simp only [_root_.coe_coe, subtype.coe_mk, + subalgebra.smul_def, smul_smul, ← pow_add, subalgebra.coe_pow], + rw tsub_add_cancel_of_le (finset.le_sup (s''.mem_attach _) : n₁ ⟨r, hr⟩ ≤ N), +end + end subalgebra section nat diff --git a/src/ring_theory/adjoin/basic.lean b/src/ring_theory/adjoin/basic.lean index 51357c46d4265..63a64bcbc86e7 100644 --- a/src/ring_theory/adjoin/basic.lean +++ b/src/ring_theory/adjoin/basic.lean @@ -270,8 +270,13 @@ begin congr' 1 with z, simp [submonoid.closure_union, submonoid.mem_sup, set.mem_mul] end -lemma pow_smul_mem_adjoin_smul (r : R) (s : set A) {x : A} (hx : x ∈ adjoin R s) : - ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ adjoin R (r • s) := +variable {R} + +lemma pow_smul_mem_of_smul_subset_of_mem_adjoin + [comm_semiring B] [algebra R B] [algebra A B] [is_scalar_tower R A B] + (r : A) (s : set B) (B' : subalgebra R B) (hs : r • s ⊆ B') {x : B} (hx : x ∈ adjoin R s) + (hr : algebra_map A B r ∈ B') : + ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ B' := begin change x ∈ (adjoin R s).to_submodule at hx, rw [adjoin_eq_span, finsupp.mem_span_iff_total] at hx, @@ -280,16 +285,24 @@ begin use l.support.sup n₁, intros n hn, rw finsupp.smul_sum, - refine (adjoin R (r • s)).to_submodule.sum_mem _, + refine B'.to_submodule.sum_mem _, intros a ha, have : n ≥ n₁ a := le_trans (finset.le_sup ha) hn, dsimp only, - rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul, smul_smul _ (l a), mul_comm, - ← smul_smul, adjoin_eq_span], - refine submodule.smul_mem _ _ _, - exact submodule.smul_mem _ _ (submodule.subset_span (n₂ a)) + rw [← tsub_add_cancel_of_le this, pow_add, ← smul_smul, + ← is_scalar_tower.algebra_map_smul A (l a) (a : B), smul_smul (r ^ n₁ a), + mul_comm, ← smul_smul, smul_def, map_pow, is_scalar_tower.algebra_map_smul], + apply subalgebra.mul_mem _ (subalgebra.pow_mem _ hr _) _, + refine subalgebra.smul_mem _ _ _, + change _ ∈ B'.to_submonoid, + rw ← submonoid.closure_eq B'.to_submonoid, + apply submonoid.closure_mono hs (n₂ a), end +lemma pow_smul_mem_adjoin_smul (r : R) (s : set A) {x : A} (hx : x ∈ adjoin R s) : + ∃ n₀ : ℕ, ∀ n ≥ n₀, r ^ n • x ∈ adjoin R (r • s) := +pow_smul_mem_of_smul_subset_of_mem_adjoin r s _ subset_adjoin hx (subalgebra.algebra_map_mem _ _) + end comm_semiring section ring diff --git a/src/ring_theory/local_properties.lean b/src/ring_theory/local_properties.lean index a76ad1b435a1e..70f52e77a63c5 100644 --- a/src/ring_theory/local_properties.lean +++ b/src/ring_theory/local_properties.lean @@ -111,9 +111,24 @@ 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` +/-- A property `P` of ring homs satisfies `ring_hom.of_localization_finite_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ᵣ`. -/ +`P` holds for `R →+* Sᵣ`. + +Note that this is equivalent to `ring_hom.of_localization_span_target` via +`ring_hom.of_localization_span_target_iff_finite`, but this is easier to prove. -/ +def ring_hom.of_localization_finite_span_target : Prop := +∀ ⦃R S : Type u⦄ [comm_ring R] [comm_ring S] (f : by exactI R →+* S) + (s : finset S) (hs : by exactI ideal.span (s : set 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 `ring_hom.of_localization_span_target` +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 `ring_hom.of_localization_finite_span_target` via +`ring_hom.of_localization_span_target_iff_finite`, but this has less restrictions when applying. -/ 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 = ⊤) @@ -148,6 +163,19 @@ begin exact h s' h₂ (λ x, hs' ⟨_, h₁ x.prop⟩) } end +lemma ring_hom.of_localization_span_target_iff_finite : + ring_hom.of_localization_span_target @P ↔ ring_hom.of_localization_finite_span_target @P := +begin + delta ring_hom.of_localization_span_target ring_hom.of_localization_finite_span_target, + apply forall₅_congr, -- TODO: Using `refine` here breaks `resetI`. + introsI, + split, + { intros h s, exact h s }, + { intros h s hs hs', + obtain ⟨s', h₁, h₂⟩ := (ideal.span_eq_top_iff_finite s).mp hs, + exact h s' h₂ (λ x, hs' ⟨_, h₁ x.prop⟩) } +end + variables {P f R' S'} lemma _root_.ring_hom.property_is_local.respects_iso (hP : ring_hom.property_is_local @P) : @@ -543,6 +571,37 @@ lemma localization_away_map_finite_type (r : R) [is_localization.away r R'] (is_localization.away.map R' S' f r).finite_type := localization_finite_type.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`. +-/ +lemma is_localization.exists_smul_mem_of_mem_adjoin [algebra R S] + [algebra R S'] [is_scalar_tower R S S'] (M : submonoid S) + [is_localization M S'] (x : S) (s : finset S') (A : subalgebra R S) + (hA₁ : (is_localization.finset_integer_multiple M s : set S) ⊆ A) + (hA₂ : M ≤ A.to_submonoid) + (hx : algebra_map S S' x ∈ algebra.adjoin R (s : set S')) : + ∃ m : M, m • x ∈ A := +begin + let g : S →ₐ[R] S' := is_scalar_tower.to_alg_hom R S S', + let y := is_localization.common_denom_of_finset M s, + have hx₁ : (y : S) • ↑s = g '' _ := (is_localization.finset_integer_multiple_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₂⟩ := (is_localization.eq_iff_exists M S').mp hx'', + use a * y ^ n, + convert A.mul_mem hx' (hA₂ a.2), + convert ha₂.symm, + simp only [submonoid.smul_def, submonoid.coe_pow, smul_eq_mul, submonoid.coe_mul], + ring, +end + /-- Let `S` be an `R`-algebra, `M` an 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`, @@ -556,30 +615,10 @@ lemma is_localization.lift_mem_adjoin_finset_integer_multiple [algebra R S] ∃ m : M, m • x ∈ algebra.adjoin R (is_localization.finset_integer_multiple (M.map (algebra_map R S : R →* S)) s : set S) := begin - -- mirrors the proof of `is_localization.smul_mem_finset_integer_multiple_span` - let g : S →ₐ[R] S' := alg_hom.mk' (algebra_map S S') - (λ c x, by simp [algebra.algebra_map_eq_smul_one]), - - let y := is_localization.common_denom_of_finset (M.map (algebra_map R S : R →* S)) s, - have hx₁ : (y : S) • ↑s = g '' _ := (is_localization.finset_integer_multiple_image _ s).symm, - obtain ⟨y', hy', e : algebra_map R S y' = y⟩ := y.prop, - have : algebra_map R S y' • (s : set S') = y' • s := - by simp_rw [algebra.algebra_map_eq_smul_one, smul_assoc, one_smul], - rw [← e, this] at hx₁, - replace hx₁ := congr_arg (algebra.adjoin R) hx₁, - obtain ⟨n, hn⟩ := algebra.pow_smul_mem_adjoin_smul _ y' (s : set S') hx, - specialize hn n (le_of_eq rfl), - erw [hx₁, ← g.map_smul, ← g.map_adjoin] at hn, - obtain ⟨x', hx', hx''⟩ := hn, - obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ := (is_localization.eq_iff_exists - (M.map (algebra_map R S : R →* S)) S').mp hx'', - use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M) ^ n, - convert (algebra.adjoin R (is_localization.finset_integer_multiple - (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 }, - { rw mul_comm, exact algebra.smul_def _ _ } + obtain ⟨⟨_, a, ha, rfl⟩, e⟩ := is_localization.exists_smul_mem_of_mem_adjoin + (M.map (algebra_map R S : R →* S)) x s (algebra.adjoin R _) algebra.subset_adjoin _ hx, + { exact ⟨⟨a, ha⟩, by simpa [submonoid.smul_def] using e⟩ }, +{ rintros _ ⟨a, ha, rfl⟩, exact subalgebra.algebra_map_mem _ a } end lemma finite_type_of_localization_span : ring_hom.of_localization_span @ring_hom.finite_type := @@ -613,7 +652,7 @@ begin rw [submonoid.smul_def, algebra.smul_def, is_scalar_tower.algebra_map_apply R S, subtype.coe_mk, ← map_mul] at hn₁, obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := is_localization.lift_mem_adjoin_finset_integer_multiple - (submonoid.powers (r : R)) (localization.away (f r)) _ (s₁ r) hn₁, + (submonoid.powers (r : R)) _ (s₁ r) hn₁, rw [submonoid.smul_def, ← algebra.smul_def, smul_smul, subtype.coe_mk, ← pow_add] at hn₂, use n₂ + n₁, refine le_supr (λ (x : s), algebra.adjoin R (sf x : set S)) r _, diff --git a/src/ring_theory/ring_hom/finite_type.lean b/src/ring_theory/ring_hom/finite_type.lean new file mode 100644 index 0000000000000..ecce446a133de --- /dev/null +++ b/src/ring_theory/ring_hom/finite_type.lean @@ -0,0 +1,92 @@ +/- +Copyright (c) 2021 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import ring_theory.local_properties +import ring_theory.localization.inv_submonoid + +/-! + +# The meta properties of finite-type ring homomorphisms. + +The main result is `ring_hom.finite_is_local`. + +-/ + +namespace ring_hom + +open_locale pointwise + +lemma finite_type_stable_under_composition : + stable_under_composition @finite_type := +by { introv R hf hg, exactI hg.comp hf } + +lemma finite_type_holds_for_localization_away : + holds_for_localization_away @finite_type := +begin + introv R _, + resetI, + suffices : algebra.finite_type R S, + { change algebra.finite_type _ _, convert this, ext, rw algebra.smul_def, refl }, + exact is_localization.finite_type_of_monoid_fg (submonoid.powers r) S, +end + +lemma finite_type_of_localization_span_target : of_localization_span_target @finite_type := +begin + -- Setup algebra intances. + rw of_localization_span_target_iff_finite, + introv R hs H, + resetI, + classical, + letI := f.to_algebra, + replace H : ∀ r : s, algebra.finite_type R (localization.away (r : S)), + { intro r, convert H r, ext, rw algebra.smul_def, refl }, + replace H := λ r, (H r).1, + constructor, + -- Suppose `s : finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra. + -- Say `t r : finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that + -- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`. + choose t ht using H, + obtain ⟨l, hl⟩ := (finsupp.mem_span_iff_total S (s : set S) 1).mp + (show (1 : S) ∈ ideal.span (s : set S), by { rw hs, trivial }), + let sf := λ (x : s), is_localization.finset_integer_multiple (submonoid.powers (x : S)) (t x), + use s.attach.bUnion sf ∪ s ∪ l.support.image l, + rw eq_top_iff, + -- We need to show that every `x` falls in the subalgebra generated by those elements. + -- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in + -- the algebra for each `sᵢ` and some `nᵢ`. + rintro x -, + apply subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : set S) l hl _ _ x _, + { intros x hx, + apply algebra.subset_adjoin, + rw [finset.coe_union, finset.coe_union], + exact or.inl (or.inr hx) }, + { intros i, + by_cases h : l i = 0, { rw h, exact zero_mem _ }, + apply algebra.subset_adjoin, + rw [finset.coe_union, finset.coe_image], + exact or.inr (set.mem_image_of_mem _ (finsupp.mem_support_iff.mpr h)) }, + { intro r, + rw [finset.coe_union, finset.coe_union, finset.coe_bUnion], + -- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the + -- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true. + obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := is_localization.exists_smul_mem_of_mem_adjoin + (submonoid.powers (r : S)) x (t r) + (algebra.adjoin R _) _ _ _, + { exact ⟨n₂, hn₂⟩ }, + { intros x hx, + apply algebra.subset_adjoin, + refine or.inl (or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩) }, + { rw [submonoid.powers_eq_closure, submonoid.closure_le, set.singleton_subset_iff], + apply algebra.subset_adjoin, + exact or.inl (or.inr r.2) }, + { rw ht, trivial } } +end + +lemma finite_is_local : + property_is_local @finite_type := +⟨localization_finite_type, finite_type_of_localization_span_target, + finite_type_stable_under_composition, finite_type_holds_for_localization_away⟩ + +end ring_hom