From b69c9a770ecf37eb21f7b8cf4fa00de3b62694ec Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Tue, 24 Jan 2023 12:36:48 +0000 Subject: [PATCH] feat(ring_theory/localization): localization of a basis, again (#18261) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR replaces `basis.localization` with `basis.localization_localization`, which maps `basis ι R S` to `basis ι Rm Sm`, where `Rm` and `Sm` are the localizations of `R` and `S` at `m`. This differs from the existing `basis.localization` by localizing in two places at once, since localizing only the coefficients is probably not useful. See also: #18150 Co-authored-by: Vierkantor --- src/ring_theory/localization/basic.lean | 75 ++++++++++++++++++++-- src/ring_theory/localization/module.lean | 82 +++++++++++++++++++++--- 2 files changed, 141 insertions(+), 16 deletions(-) diff --git a/src/ring_theory/localization/basic.lean b/src/ring_theory/localization/basic.lean index 63038c1b0b0f0..f26c26a139e19 100644 --- a/src/ring_theory/localization/basic.lean +++ b/src/ring_theory/localization/basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen -/ -import algebra.algebra.equiv +import algebra.algebra.tower import algebra.ring.equiv import group_theory.monoid_localization import ring_theory.ideal.basic @@ -1143,7 +1143,12 @@ variables (S M) Given an algebra `R → S`, a submonoid `R` of `M`, and a localization `Rₘ` for `M`, let `Sₘ` be the localization of `S` to the image of `M` under `algebra_map R S`. Then this is the natural algebra structure on `Rₘ → Sₘ`, such that the entire square commutes, -where `localization_map.map_comp` gives the commutativity of the underlying maps -/ +where `localization_map.map_comp` gives the commutativity of the underlying maps. + +This instance can be helpful if you define `Sₘ := localization (algebra.algebra_map_submonoid S M)`, +however we will instead use the hypotheses `[algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ]` in lemmas +since the algebra structure may arise in different ways. +-/ noncomputable def localization_algebra : algebra Rₘ Sₘ := (map Sₘ (algebra_map R S) (show _ ≤ (algebra.algebra_map_submonoid S M).comap _, from M.le_comap_map) @@ -1151,10 +1156,68 @@ noncomputable def localization_algebra : algebra Rₘ Sₘ := end -lemma algebra_map_mk' (r : R) (m : M) : - (@algebra_map Rₘ Sₘ _ _ (localization_algebra M S)) (mk' Rₘ r m) = - mk' Sₘ (algebra_map R S r) ⟨algebra_map R S m, algebra.mem_algebra_map_submonoid_of_mem m⟩ := -map_mk' _ _ _ +section + +variables [algebra Rₘ Sₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ] + +variables (S Rₘ Sₘ) +include S + +lemma is_localization.map_units_map_submonoid (y : M) : is_unit (algebra_map R Sₘ y) := +begin + rw is_scalar_tower.algebra_map_apply _ S, + exact is_localization.map_units Sₘ ⟨algebra_map R S y, algebra.mem_algebra_map_submonoid_of_mem y⟩ +end + +@[simp] lemma is_localization.algebra_map_mk' (x : R) (y : M) : + algebra_map Rₘ Sₘ (is_localization.mk' Rₘ x y) = + is_localization.mk' Sₘ (algebra_map R S x) ⟨algebra_map R S y, + algebra.mem_algebra_map_submonoid_of_mem y⟩ := +begin + rw [is_localization.eq_mk'_iff_mul_eq, subtype.coe_mk, ← is_scalar_tower.algebra_map_apply, + ← is_scalar_tower.algebra_map_apply, is_scalar_tower.algebra_map_apply R Rₘ Sₘ, + is_scalar_tower.algebra_map_apply R Rₘ Sₘ, ← _root_.map_mul, + mul_comm, is_localization.mul_mk'_eq_mk'_of_mul], + exact congr_arg (algebra_map Rₘ Sₘ) (is_localization.mk'_mul_cancel_left x y) +end + +variables (M) + +/-- If the square below commutes, the bottom map is uniquely specified: +``` +R → S +↓ ↓ +Rₘ → Sₘ +``` +-/ +lemma is_localization.algebra_map_eq_map_map_submonoid : + algebra_map Rₘ Sₘ = map Sₘ (algebra_map R S) + (show _ ≤ (algebra.algebra_map_submonoid S M).comap _, from M.le_comap_map) := +eq.symm $ is_localization.map_unique _ (algebra_map Rₘ Sₘ) (λ x, + by rw [← is_scalar_tower.algebra_map_apply R S Sₘ, ← is_scalar_tower.algebra_map_apply R Rₘ Sₘ]) + +/-- If the square below commutes, the bottom map is uniquely specified: +``` +R → S +↓ ↓ +Rₘ → Sₘ +``` +-/ +lemma is_localization.algebra_map_apply_eq_map_map_submonoid (x) : + algebra_map Rₘ Sₘ x = map Sₘ (algebra_map R S) + (show _ ≤ (algebra.algebra_map_submonoid S M).comap _, from M.le_comap_map) + x := +fun_like.congr_fun (is_localization.algebra_map_eq_map_map_submonoid _ _ _ _) x + +variables {R} + +lemma is_localization.lift_algebra_map_eq_algebra_map : + @is_localization.lift R _ M Rₘ _ _ Sₘ _ _ (algebra_map R Sₘ) + (is_localization.map_units_map_submonoid S Sₘ) = + algebra_map Rₘ Sₘ := +is_localization.lift_unique _ (λ x, (is_scalar_tower.algebra_map_apply _ _ _ _).symm) + +end variables (Rₘ Sₘ) diff --git a/src/ring_theory/localization/module.lean b/src/ring_theory/localization/module.lean index 68953652dc66a..b83bb0035a09f 100644 --- a/src/ring_theory/localization/module.lean +++ b/src/ring_theory/localization/module.lean @@ -16,8 +16,8 @@ This file contains some results about vector spaces over the field of fractions * `linear_independent.localization`: `b` is linear independent over a localization of `R` if it is linear independent over `R` itself - * `basis.localization`: promote an `R`-basis `b` to an `Rₛ`-basis, - where `Rₛ` is a localization of `R` + * `basis.localization_localization`: promote an `R`-basis `b` of `A` to an `Rₛ`-basis of `Aₛ`, + where `Rₛ` and `Aₛ` are localizations of `R` and `A` at `s` respectively * `linear_independent.iff_fraction_ring`: `b` is linear independent over `R` iff it is linear independent over `Frac(R)` -/ @@ -54,16 +54,78 @@ begin end end add_comm_monoid -section add_comm_group -variables {M : Type*} [add_comm_group M] [module R M] [module Rₛ M] [is_scalar_tower R Rₛ M] +section localization_localization -/-- Promote a basis for `M` over `R` to a basis for `M` over the localization `Rₛ` -/ -noncomputable def basis.localization {ι : Type*} (b : basis ι R M) : basis ι Rₛ M := -basis.mk (b.linear_independent.localization Rₛ S) $ -by { rw [← eq_top_iff, ← @submodule.restrict_scalars_eq_top_iff Rₛ R, eq_top_iff, ← b.span_eq], - apply submodule.span_le_restrict_scalars } +variables {A : Type*} [comm_ring A] [algebra R A] +variables (Aₛ : Type*) [comm_ring Aₛ] [algebra A Aₛ] +variables [algebra Rₛ Aₛ] [algebra R Aₛ] [is_scalar_tower R Rₛ Aₛ] [is_scalar_tower R A Aₛ] +variables [hA : is_localization (algebra.algebra_map_submonoid A S) Aₛ] +include hA -end add_comm_group +open submodule + +lemma linear_independent.localization_localization {ι : Type*} + {v : ι → A} (hv : linear_independent R v) (hS : algebra.algebra_map_submonoid A S ≤ A⁰) : + linear_independent Rₛ (algebra_map A Aₛ ∘ v) := +begin + refine (hv.map' ((algebra.linear_map A Aₛ).restrict_scalars R) _).localization Rₛ S, + rw [linear_map.ker_restrict_scalars, restrict_scalars_eq_bot_iff, linear_map.ker_eq_bot, + algebra.coe_linear_map], + exact is_localization.injective Aₛ hS +end + +lemma span_eq_top.localization_localization {v : set A} (hv : span R v = ⊤) : + span Rₛ (algebra_map A Aₛ '' v) = ⊤ := +begin + rw eq_top_iff, + rintros a' -, + obtain ⟨a, ⟨_, s, hs, rfl⟩, rfl⟩ := is_localization.mk'_surjective + (algebra.algebra_map_submonoid A S) a', + rw [is_localization.mk'_eq_mul_mk'_one, mul_comm, ← map_one (algebra_map R A)], + erw ← is_localization.algebra_map_mk' A Rₛ Aₛ (1 : R) ⟨s, hs⟩, -- `erw` needed to unify `⟨s, hs⟩` + rw ← algebra.smul_def, + refine smul_mem _ _ (span_subset_span R _ _ _), + rw [← algebra.coe_linear_map, ← linear_map.coe_restrict_scalars R, ← linear_map.map_span], + exact mem_map_of_mem (hv.symm ▸ mem_top), + { apply_instance } +end + +/-- If `A` has an `R`-basis, then localizing `A` at `S` has a basis over `R` localized at `S`. + +A suitable instance for `[algebra A Aₛ]` is `localization_algebra`. +-/ +noncomputable def basis.localization_localization {ι : Type*} (b : basis ι R A) + (hS : algebra.algebra_map_submonoid A S ≤ A⁰) : + basis ι Rₛ Aₛ := +basis.mk + (b.linear_independent.localization_localization _ S _ hS) + (by { rw [set.range_comp, span_eq_top.localization_localization Rₛ S Aₛ b.span_eq], + exact le_rfl }) + +@[simp] lemma basis.localization_localization_apply {ι : Type*} (b : basis ι R A) + (hS : algebra.algebra_map_submonoid A S ≤ A⁰) (i) : + b.localization_localization Rₛ S Aₛ hS i = algebra_map A Aₛ (b i) := +basis.mk_apply _ _ _ + +@[simp] lemma basis.localization_localization_repr_algebra_map {ι : Type*} (b : basis ι R A) + (hS : algebra.algebra_map_submonoid A S ≤ A⁰) (x i) : + (b.localization_localization Rₛ S Aₛ hS).repr (algebra_map A Aₛ x) i = + algebra_map R Rₛ (b.repr x i) := +calc (b.localization_localization Rₛ S Aₛ hS).repr (algebra_map A Aₛ x) i + = (b.localization_localization Rₛ S Aₛ hS).repr + ((b.repr x).sum (λ j c, algebra_map R Rₛ c • algebra_map A Aₛ (b j))) i : + by simp_rw [is_scalar_tower.algebra_map_smul, algebra.smul_def, + is_scalar_tower.algebra_map_apply R A Aₛ, ← _root_.map_mul, ← map_finsupp_sum, + ← algebra.smul_def, ← finsupp.total_apply, basis.total_repr] +... = (b.repr x).sum (λ j c, algebra_map R Rₛ c • finsupp.single j 1 i) : + by simp_rw [← b.localization_localization_apply Rₛ S Aₛ hS, map_finsupp_sum, + linear_equiv.map_smul, basis.repr_self, finsupp.sum_apply, finsupp.smul_apply] +... = _ : finset.sum_eq_single i + (λ j _ hj, by simp [hj]) + (λ hi, by simp [finsupp.not_mem_support_iff.mp hi]) +... = algebra_map R Rₛ (b.repr x i) : by simp [algebra.smul_def] + +end localization_localization end localization