chore(RingTheory/Localization): mirror tensor product compatibilities and golf (leanprover-community#38177)

We add a mirrored version of `IsLocalization.tensorProduct_tensorProduct` and some related isomorphisms. We use this to golf the proof of `RingHom.locally_isStableUnderBaseChange`.

Author: chrisflav

Mathlib/RingTheory/Localization/BaseChange.lean

@@ -238,7 +238,7 @@ instance IsLocalization.tensor (M : Submonoid R) [IsLocalization M A] :
   rw [Algebra.isLocalization_iff_isPushout _ A]
   infer_instance
 
-attribute [local instance] Algebra.TensorProduct.rightAlgebra
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 instance IsLocalization.tensorRight (M : Submonoid R) [IsLocalization M A] :
     IsLocalization (Algebra.algebraMapSubmonoid S M) (A ⊗[R] S) := by
   rw [Algebra.isLocalization_iff_isPushout _ A]
@@ -254,6 +254,7 @@ lemma IsLocalization.tmul_mk' (M : Submonoid R) [IsLocalization M A] (s : S) (x
     IsLocalization.mk'_spec', algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
     ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
 
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 open Algebra.TensorProduct in
 lemma IsLocalization.mk'_tmul (M : Submonoid R) [IsLocalization M A] (s : S) (x : R) (y : M) :
     IsLocalization.mk' A x y ⊗ₜ s =
@@ -318,7 +319,7 @@ end Localization
 variable (R S) {A} in
 /-- `A[M⁻¹] ⊗[R] S` is the localization of `A ⊗[R] S` at `M`. -/
 lemma IsLocalization.tensorProduct_tensorProduct (M : Submonoid A)
-    (B : Type*) [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
+    (B : Type*) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
     [IsLocalization M B]
     [Algebra (A ⊗[R] S) (B ⊗[R] S)] [IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)]
     (H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp Algebra.TensorProduct.includeRight.toRingHom =
@@ -327,6 +328,88 @@ lemma IsLocalization.tensorProduct_tensorProduct (M : Submonoid A)
   (Algebra.isLocalization_iff_isPushout M _).mpr
     (Algebra.IsPushout.tensorProduct_tensorProduct R S A B H).symm
 
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+variable (R S) {A} in
+/-- `S ⊗[R] A[M⁻¹]` is the localization of `S ⊗[R] A` at `M`. -/
+lemma IsLocalization.tensorProduct_tensorProduct_right (M : Submonoid A)
+    (B : Type*) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
+    [IsLocalization M B]
+    [Algebra (S ⊗[R] A) (S ⊗[R] B)] [IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)]
+    (H : (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
+      Algebra.TensorProduct.includeRight.toRingHom.comp (algebraMap A B)) :
+    IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S))) (S ⊗[R] B) := by
+  change IsLocalization (Algebra.algebraMapSubmonoid _ M) (S ⊗[R] B)
+  let : Algebra A (S ⊗[R] B) := .compHom _ (algebraMap A B)
+  have : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B) := .of_algebraMap_eq' H.symm
+  have : IsScalarTower R A (S ⊗[R] B) :=
+    .of_algebraMap_eq' <| by
+      rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
+        IsScalarTower.algebraMap_eq R B]
+  have : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B) := .to₁₃₄ _ A _ _
+  have : IsScalarTower A B (S ⊗[R] B) := .of_algebraMap_eq' rfl
+  rw [Algebra.isLocalization_iff_isPushout _ B, Algebra.IsPushout.comm,
+    ← Algebra.IsPushout.comp_iff R _ S]
+  infer_instance
+
+variable (R S) {A} in
+/-- The natural isomorphism `S ⊗[R] A[M⁻¹] ≃ (S ⊗[R] A)[M⁻¹]`. -/
+noncomputable
+def IsLocalization.tensorProductEquivOfMapIncludeRight (M : Submonoid A)
+    (B : Type*) [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
+    [IsLocalization M B]
+    (C : Type*) [CommSemiring C] [Algebra S C] [Algebra (S ⊗[R] A) C] [IsScalarTower S (S ⊗[R] A) C]
+    [IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S))) C] :
+    S ⊗[R] B ≃ₐ[S] C :=
+  letI M' : Submonoid (S ⊗[R] A) := M.map (Algebra.TensorProduct.includeRight (R := R) (A := S))
+  letI : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
+    (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R _ _)).toAlgebra
+  haveI : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B) :=
+    .of_algebraMap_eq <| by intro; simp [RingHom.algebraMap_toAlgebra]
+  haveI := IsLocalization.tensorProduct_tensorProduct_right R S M B
+    (by ext; simp [RingHom.algebraMap_toAlgebra])
+  (IsLocalization.algEquiv M' _ _).restrictScalars S
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+lemma IsLocalization.tensorProductEquivOfMapIncludeRight_tmul (M : Submonoid A)
+    (B : Type*) [CommSemiring B] [Algebra R B] [Algebra A B]
+    [IsScalarTower R A B] [IsLocalization M B]
+    (C : Type*) [CommSemiring C] [Algebra S C] [Algebra (S ⊗[R] A) C] [IsScalarTower S (S ⊗[R] A) C]
+    [IsLocalization (M.map (Algebra.TensorProduct.includeRight (R := R) (A := S))) C]
+    (x : S) (a : A) :
+    IsLocalization.tensorProductEquivOfMapIncludeRight R S M B C (x ⊗ₜ algebraMap A B a) =
+      algebraMap _ _ (x ⊗ₜ[R] a) := by
+  letI : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
+    (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R _ _)).toAlgebra
+  have heq : x ⊗ₜ[R] (algebraMap A B) a = algebraMap _ _ (x ⊗ₜ[R] a) := rfl
+  simp [heq, IsLocalization.tensorProductEquivOfMapIncludeRight]
+
+variable (R S) {A} in
+/-- The natural isomorphism `S ⊗[R] A[1/g] ≃ (S ⊗[R] A)[1/g]`. -/
+noncomputable
+def IsLocalization.Away.tensorProductEquivTMulRight (g : A) (B : Type*) [CommSemiring B]
+    [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsLocalization.Away g B] :
+    S ⊗[R] B ≃ₐ[S] Localization.Away ((1 : S) ⊗ₜ[R] g) :=
+  haveI : IsLocalization
+      ((Submonoid.powers g).map (Algebra.TensorProduct.includeRight (R := R) (A := S)))
+      (Localization.Away ((1 : S) ⊗ₜ[R] g)) := by
+    simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
+    infer_instance
+  IsLocalization.tensorProductEquivOfMapIncludeRight _ _ (.powers g) _ _
+
+@[simp]
+lemma IsLocalization.Away.tensorProductEquivTMulRight_tmul (g : A) (B : Type*) [CommSemiring B]
+    [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsLocalization.Away g B]
+    (x : S) (a : A) :
+    IsLocalization.Away.tensorProductEquivTMulRight R S g B (x ⊗ₜ algebraMap _ _ a) =
+      algebraMap _ _ (x ⊗ₜ[R] a) :=
+  haveI : IsLocalization
+      ((Submonoid.powers g).map (Algebra.TensorProduct.includeRight (R := R) (A := S)))
+      (Localization.Away ((1 : S) ⊗ₜ[R] g)) := by
+    simp only [Submonoid.map_powers, Algebra.TensorProduct.includeRight_apply]
+    infer_instance
+  IsLocalization.tensorProductEquivOfMapIncludeRight_tmul _ _ _ _ _ _
+
 namespace IsLocalization.Away
 
 instance tensor [IsLocalization.Away r A] :

Mathlib/RingTheory/Localization/Basic.lean

@@ -533,9 +533,17 @@ noncomputable def localizationAlgebra : Algebra Rₘ Sₘ :=
 noncomputable instance : Algebra (Localization M)
     (Localization (Algebra.algebraMapSubmonoid S M)) := localizationAlgebra M S
 
+-- This is not an instance, because the discrimination tree key is `IsScalarTower _ _ _ _ _ _`, so
+-- it would cause significant slowdowns.
+lemma isScalarTower_localizationAlgebra [Algebra R Sₘ] [IsScalarTower R S Sₘ] :
+    letI : Algebra Rₘ Sₘ := localizationAlgebra M S
+    IsScalarTower R Rₘ Sₘ :=
+  letI : Algebra Rₘ Sₘ := localizationAlgebra M S
+  .of_algebraMap_eq' <| by
+    simp [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R S Sₘ]
+
 instance : IsScalarTower R (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)) :=
-  IsScalarTower.of_algebraMap_eq (fun x ↦
-    (IsLocalization.map_eq (T := (Algebra.algebraMapSubmonoid S M)) M.le_comap_map x).symm)
+  isScalarTower_localizationAlgebra _ _
 
 end
 

Mathlib/RingTheory/Localization/Finiteness.lean

@@ -155,8 +155,6 @@ instance {R S : Type*} [CommRing R] {P : Ideal R} [CommRing S] [Algebra R S]
 open Algebra nonZeroDivisors in
 instance {A C : Type*} [CommRing A] [CommRing C] [Algebra A C] [Module.Finite A C] :
     Module.Finite (FractionRing A) (Localization (algebraMapSubmonoid C A⁰)) :=
-  have : IsScalarTower A (FractionRing A) (Localization (algebraMapSubmonoid C A⁰)) :=
-    instIsScalarTowerLocalizationAlgebraMapSubmonoid A⁰ C
   .of_isLocalization A C A⁰
 
 include S f in

Mathlib/RingTheory/RingHom/Locally.lean

@@ -65,6 +65,15 @@ def Locally {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : Prop :=
 
 variable {R S : Type u} [CommRing R] [CommRing S]
 
+lemma locally_iff_span_eq_top {f : R →+* S} :
+    Locally P f ↔ Ideal.span {g : S | P ((algebraMap S (Localization.Away g)).comp f)} = ⊤ := by
+  refine ⟨fun ⟨s, hs, h⟩ ↦ ?_, fun h ↦ ⟨_, h, fun g hg ↦ hg⟩⟩
+  rw [eq_top_iff, ← hs, Ideal.span_le]
+  intro g hg
+  exact Ideal.subset_span (h _ hg)
+
+alias ⟨Locally.span_eq_top, _⟩ := locally_iff_span_eq_top
+
 lemma locally_iff_finite (f : R →+* S) :
     Locally P f ↔ ∃ (s : Finset S) (_ : Ideal.span (s : Set S) = ⊤),
       ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f) := by
@@ -280,48 +289,20 @@ lemma locally_stableUnderCompositionWithLocalizationAwaySource
 alias locally_StableUnderCompositionWithLocalizationAwaySource :=
   locally_stableUnderCompositionWithLocalizationAwaySource
 
-
-attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 /-- If `P` is stable under base change, then so is `Locally P`. -/
 lemma locally_isStableUnderBaseChange (hPi : RespectsIso P) (hPb : IsStableUnderBaseChange P) :
     IsStableUnderBaseChange (Locally P) := by
   apply IsStableUnderBaseChange.mk (locally_respectsIso hPi)
   introv hf
-  obtain ⟨s, hsone, hs⟩ := hf
-  rw [locally_iff_exists hPi]
-  letI (a : s) : Algebra (S ⊗[R] T) (S ⊗[R] Localization.Away a.val) :=
-    (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R _ _)).toRingHom.toAlgebra
-  letI (a : s) : Algebra T (S ⊗[R] Localization.Away a.val) :=
-    ((algebraMap _ (S ⊗[R] Localization.Away a.val)).comp (algebraMap T (S ⊗[R] T))).toAlgebra
-  haveI (a : s) : IsScalarTower T (S ⊗[R] T) (S ⊗[R] Localization.Away a.val) :=
-    IsScalarTower.of_algebraMap_eq' rfl
-  haveI (a : s) : IsScalarTower T (Localization.Away a.val) (S ⊗[R] Localization.Away a.val) :=
-    IsScalarTower.of_algebraMap_eq' rfl
-  haveI (a : s) : IsScalarTower S (S ⊗[R] T) (S ⊗[R] Localization.Away a.val) :=
-      IsScalarTower.of_algebraMap_eq <| by
-    intro x
-    simp [RingHom.algebraMap_toAlgebra]
-  haveI (a : s) : Algebra.IsPushout T (Localization.Away a.val) (S ⊗[R] T)
-      (S ⊗[R] Localization.Away a.val) := by
-    rw [← Algebra.IsPushout.comp_iff R _ S]
-    infer_instance
-  refine ⟨s, fun a ↦ Algebra.TensorProduct.includeRight a.val, ?_,
-      fun a ↦ (S ⊗[R] Localization.Away a.val), inferInstance, inferInstance, ?_, ?_⟩
-  · rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
-  · intro a
-    convert_to IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] T) (Submonoid.powers a.val))
-        (S ⊗[R] Localization.Away a.val)
-    · simp only [Algebra.TensorProduct.includeRight_apply, Algebra.algebraMapSubmonoid,
-        Submonoid.map_powers]
-      rfl
-    · rw [← isLocalizedModule_iff_isLocalization, isLocalizedModule_iff_isBaseChange
-        (S := Submonoid.powers a.val) (A := Localization.Away a.val)]
-      exact Algebra.IsPushout.out
-  · intro a
-    rw [← IsScalarTower.algebraMap_eq]
-    apply hPb R (Localization.Away a.val)
-    rw [IsScalarTower.algebraMap_eq R T]
-    exact hs a a.property
+  rw [locally_iff_span_eq_top, eq_top_iff, ← Ideal.map_top Algebra.TensorProduct.includeRight,
+    ← hf.span_eq_top, Ideal.map_le_iff_le_comap, Ideal.span_le]
+  intro g hg
+  apply Ideal.subset_span
+  simp only [Set.mem_setOf_eq, Algebra.TensorProduct.includeRight_apply,
+    ← IsScalarTower.algebraMap_eq] at hg ⊢
+  let e := IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
+  rw [← e.toAlgHom.comp_algebraMap]
+  exact hPi.left _ _ (hPb.tensorProduct _ hg)
 
 /-- If `P` is preserved by localization away, then so is `Locally P`. -/
 lemma locally_localizationAwayPreserves (hPl : LocalizationAwayPreserves P) :

Mathlib/RingTheory/RingHomProperties.lean

@@ -154,6 +154,13 @@ theorem IsStableUnderBaseChange.mk (h₁ : RespectsIso @P)
 
 attribute [local instance] Algebra.TensorProduct.rightAlgebra
 
+lemma IsStableUnderBaseChange.tensorProduct (hP : RingHom.IsStableUnderBaseChange P)
+    {R S : Type u} (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
+    (h : P (algebraMap R S)) :
+    P (algebraMap T (T ⊗[R] S)) :=
+  -- This only works because the `Algebra.TensorProduct.rightAlgebra` instance is present here.
+  hP _ _ _ _ h
+
 set_option backward.isDefEq.respectTransparency false in
 theorem IsStableUnderBaseChange.pushout_inl (hP : RingHom.IsStableUnderBaseChange @P)
     (hP' : RingHom.RespectsIso @P) {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T) (H : P g.hom) :