feat(ring_theory/localization): localization of a basis, again (#18261)

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 <vierkantor@vierkantor.com>

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,18 +1143,81 @@ 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)
   : Rₘ →+* Sₘ).to_algebra
 
 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ₘ)
 

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