feat(RingTheory/Localization): more API and kernels of localized maps (#14751)

This PR adds various API lemmas on localization. In particular it computes the kernel of a localized map as the localization of the kernel.

Author: chrisflav

Mathlib/Algebra/Algebra/Hom.lean

@@ -585,6 +585,27 @@ theorem smul_units_def (f : A →ₐ[R] A) (x : Aˣ) :
     f • x = Units.map (f : A →* A) x := rfl
 
 end MulDistribMulAction
+
+variable (M : Submonoid R) {B : Type w} [CommRing B] [Algebra R B] {A}
+
+lemma algebraMapSubmonoid_map_eq (f : A →ₐ[R] B) :
+    (algebraMapSubmonoid A M).map f = algebraMapSubmonoid B M := by
+  ext x
+  constructor
+  · rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩
+    simp only [AlgHom.commutes]
+    use r
+  · rintro ⟨r, hr, rfl⟩
+    simp only [Submonoid.mem_map]
+    use (algebraMap R A r)
+    simp only [AlgHom.commutes, and_true]
+    use r
+
+lemma algebraMapSubmonoid_le_comap (f : A →ₐ[R] B) :
+    algebraMapSubmonoid A M ≤ (algebraMapSubmonoid B M).comap f.toRingHom := by
+  rw [← algebraMapSubmonoid_map_eq M f]
+  exact Submonoid.le_comap_map (Algebra.algebraMapSubmonoid A M)
+
 end Algebra
 
 namespace MulSemiringAction

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -1123,6 +1123,14 @@ lemma map_comp (h : M →ₗ[R] N) : (map S f g h) ∘ₗ f = g ∘ₗ h :=
 lemma map_apply (h : M →ₗ[R] N) (x) : map S f g h (f x) = g (h x) :=
   lift_apply S f (g ∘ₗ h) (IsLocalizedModule.map_units g) x
 
+@[simp]
+lemma map_mk' (h : M →ₗ[R] N) (x) (s : S) :
+    map S f g h (IsLocalizedModule.mk' f x s) = (IsLocalizedModule.mk' g (h x) s) := by
+  simp only [map, lift, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.coe_comp, LinearEquiv.coe_coe,
+    Function.comp_apply]
+  rw [iso_symm_apply' S f (mk' f x s) x s (mk'_cancel' f x s), LocalizedModule.lift_mk]
+  rfl
+
 open LocalizedModule LinearEquiv LinearMap Submonoid
 
 variable (M)

Mathlib/Algebra/Module/Submodule/Localization.lean

@@ -5,6 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.Algebra.Module.LocalizedModule
 import Mathlib.LinearAlgebra.Quotient
+import Mathlib.RingTheory.Localization.Module
 
 /-!
 # Localization of Submodules
@@ -27,7 +28,7 @@ Results about localizations of submodules and quotient modules are provided in t
 
 open nonZeroDivisors
 
-universe u u' v v'
+universe u u' v v' w w'
 
 variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'}
 variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N]
@@ -48,6 +49,10 @@ def Submodule.localized' : Submodule S N where
     have ⟨y, t, hyt⟩ := IsLocalization.mk'_surjective p r
     exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩
 
+lemma Submodule.mem_localized' (x : N) :
+    x ∈ Submodule.localized' S p f M' ↔ ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x :=
+  Iff.rfl
+
 /-- The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`. -/
 abbrev Submodule.localized : Submodule (Localization p) (LocalizedModule p M) :=
   M'.localized' (Localization p) p (LocalizedModule.mkLinearMap p M)
@@ -113,3 +118,52 @@ instance IsLocalizedModule.toLocalizedQuotient' (M' : Submodule R M) :
 
 instance (M' : Submodule R M) : IsLocalizedModule p (M'.toLocalizedQuotient p) :=
   IsLocalizedModule.toLocalizedQuotient' _ _ _ _
+
+section LinearMap
+
+variable {P : Type w} [AddCommGroup P] [Module R P]
+variable {Q : Type w'} [AddCommGroup Q] [Module R Q] [Module S Q] [IsScalarTower R S Q]
+variable (f' : P →ₗ[R] Q) [IsLocalizedModule p f']
+
+lemma LinearMap.localized'_ker_eq_ker_localizedMap (g : M →ₗ[R] P) :
+    Submodule.localized' S p f (LinearMap.ker g) =
+      LinearMap.ker ((IsLocalizedModule.map p f f' g).extendScalarsOfIsLocalization p S) := by
+  ext x
+  simp only [Submodule.mem_localized', mem_ker, extendScalarsOfIsLocalization_apply']
+  constructor
+  · rintro ⟨m, hm, a, ha, rfl⟩
+    rw [IsLocalizedModule.map_mk', hm]
+    simp
+  · intro h
+    obtain ⟨⟨a, b⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x
+    simp only [Function.uncurry_apply_pair, IsLocalizedModule.map_mk',
+      IsLocalizedModule.mk'_eq_zero, IsLocalizedModule.eq_zero_iff p f'] at h
+    obtain ⟨c, hc⟩ := h
+    refine ⟨c • a, by simpa, c * b, by simp⟩
+
+lemma LinearMap.ker_localizedMap_eq_localized'_ker (g : M →ₗ[R] P) :
+    LinearMap.ker (IsLocalizedModule.map p f f' g) =
+      ((LinearMap.ker g).localized' S p f).restrictScalars _ := by
+  rw [localized'_ker_eq_ker_localizedMap S p f f']
+  rfl
+
+/--
+The canonical map from the kernel of `g` to the kernel of `g` localized at a submonoid.
+
+This is a localization map by `LinearMap.toKerLocalized_isLocalizedModule`.
+-/
+@[simps!]
+noncomputable def LinearMap.toKerIsLocalized (g : M →ₗ[R] P) :
+    ker g →ₗ[R] ker (IsLocalizedModule.map p f f' g) :=
+  f.restrict (fun x hx ↦ by simp [LinearMap.mem_ker, LinearMap.mem_ker.mp hx])
+
+/-- The canonical map to the kernel of the localization of `g` is localizing.
+In other words, localization commutes with kernels. -/
+lemma LinearMap.toKerLocalized_isLocalizedModule (g : M →ₗ[R] P) :
+    IsLocalizedModule p (toKerIsLocalized p f f' g) :=
+  let e : Submodule.localized' S p f (ker g) ≃ₗ[S]
+      ker ((IsLocalizedModule.map p f f' g).extendScalarsOfIsLocalization p S) :=
+    LinearEquiv.ofEq _ _ (localized'_ker_eq_ker_localizedMap S p f f' g)
+  IsLocalizedModule.of_linearEquiv p (Submodule.toLocalized' S p f (ker g)) (e.restrictScalars R)
+
+end LinearMap

Mathlib/GroupTheory/MonoidLocalization.lean

@@ -1188,6 +1188,20 @@ theorem map_injective_of_injective (hg : Injective g) (k : LocalizationMap (S.ma
   rw [← (f.map_units x).mul_left_inj, hxz, hxw, f.eq_iff_exists]
   exact ⟨⟨c, hc⟩, eq⟩
 
+/-- Given a surjective `CommMonoid` homomorphism `g : M →* P`, and a submonoid `S ⊆ M`,
+the induced monoid homomorphism from the localization of `M` at `S` to the
+localization of `P` at `g S`, is surjective.
+-/
+@[to_additive "Given a surjective `AddCommMonoid` homomorphism `g : M →+ P`, and a
+submonoid `S ⊆ M`, the induced monoid homomorphism from the localization of `M` at `S`
+to the localization of `P` at `g S`, is surjective. "]
+theorem map_surjective_of_surjective (hg : Surjective g) (k : LocalizationMap (S.map g) Q) :
+    Surjective (map f (apply_coe_mem_map g S) k) := fun z ↦ by
+  obtain ⟨y, ⟨y', s, hs, rfl⟩, rfl⟩ := k.mk'_surjective z
+  obtain ⟨x, rfl⟩ := hg y
+  use f.mk' x ⟨s, hs⟩
+  rw [map_mk']
+
 section AwayMap
 
 variable (x : M)

Mathlib/RingTheory/Ideal/Maps.lean

@@ -908,3 +908,15 @@ lemma coe_ideal_map (I : Ideal A) :
     Ideal.map f I = Ideal.map (f : A →+* B) I := rfl
 
 end AlgHom
+
+namespace Algebra
+
+variable {R : Type*} [CommSemiring R] (S : Type*) [Semiring S] [Algebra R S]
+
+/-- The induced linear map from `I` to the span of `I` in an `R`-algebra `S`. -/
+@[simps!]
+def idealMap (I : Ideal R) : I →ₗ[R] I.map (algebraMap R S) :=
+  (Algebra.linearMap R S).restrict (q := (I.map (algebraMap R S)).restrictScalars R)
+    (fun _ ↦ Ideal.mem_map_of_mem _)
+
+end Algebra

Mathlib/RingTheory/Localization/Away/Basic.lean

@@ -117,6 +117,45 @@ noncomputable def map (f : R →+* P) (r : R) [IsLocalization.Away r S]
       simp)
 #align is_localization.away.map IsLocalization.Away.map
 
+section Algebra
+
+variable {A : Type*} [CommRing A] [Algebra R A]
+variable {B : Type*} [CommRing B] [Algebra R B]
+variable (Aₚ : Type*) [CommRing Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ]
+variable (Bₚ : Type*) [CommRing Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ]
+
+instance {f : A →+* B} (a : A) [Away (f a) Bₚ] : IsLocalization (.map f (.powers a)) Bₚ := by
+  simpa
+
+/-- Given a algebra map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map
+`Aₐ →ₐ[R] Bₐ`. -/
+noncomputable def mapₐ (f : A →ₐ[R] B) (a : A) [Away a Aₚ] [Away (f a) Bₚ] : Aₚ →ₐ[R] Bₚ :=
+  ⟨map Aₚ Bₚ f.toRingHom a, fun r ↦ by
+    dsimp only [AlgHom.toRingHom_eq_coe, map, RingHom.coe_coe, OneHom.toFun_eq_coe]
+    rw [IsScalarTower.algebraMap_apply R A Aₚ, IsScalarTower.algebraMap_eq R B Bₚ]
+    erw [IsLocalization.map_eq]
+    simp⟩
+
+@[simp]
+lemma mapₐ_apply (f : A →ₐ[R] B) (a : A) [Away a Aₚ] [Away (f a) Bₚ] (x : Aₚ) :
+    mapₐ Aₚ Bₚ f a x = map Aₚ Bₚ f.toRingHom a x :=
+  rfl
+
+variable {Aₚ} {Bₚ}
+
+lemma mapₐ_injective_of_injective {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ]
+    (hf : Function.Injective f) : Function.Injective (mapₐ Aₚ Bₚ f a) :=
+  IsLocalization.map_injective_of_injective _ _ _ hf
+
+lemma mapₐ_surjective_of_surjective {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ]
+    (hf : Function.Surjective f) : Function.Surjective (mapₐ Aₚ Bₚ f a) :=
+  have : IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ := by
+    simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe]
+    infer_instance
+  IsLocalization.map_surjective_of_surjective _ _ _ hf
+
+end Algebra
+
 end Away
 
 end Away
@@ -228,6 +267,14 @@ noncomputable abbrev awayMap (f : R →+* P) (r : R) :
   IsLocalization.Away.map _ _ f r
 #align localization.away_map Localization.awayMap
 
+variable {A : Type*} [CommRing A] [Algebra R A]
+variable {B : Type*} [CommRing B] [Algebra R B]
+
+/-- Given a map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map `Aₐ →ₐ[R] Bₐ`. -/
+noncomputable abbrev awayMapₐ (f : A →ₐ[R] B) (a : A) :
+    Localization.Away a →ₐ[R] Localization.Away (f a) :=
+  IsLocalization.Away.mapₐ _ _ f a
+
 end Localization
 
 end CommSemiring

Mathlib/RingTheory/Localization/Basic.lean

@@ -799,6 +799,11 @@ theorem map_injective_of_injective (h : Function.Injective g) [IsLocalization (M
     Function.Injective (map Q g M.le_comap_map : S → Q) :=
   (toLocalizationMap M S).map_injective_of_injective h (toLocalizationMap (M.map g) Q)
 
+/-- Surjectivity of a map descends to the map induced on localizations. -/
+theorem map_surjective_of_surjective (h : Function.Surjective g) [IsLocalization (M.map g) Q] :
+    Function.Surjective (map Q g M.le_comap_map : S → Q) :=
+  (toLocalizationMap M S).map_surjective_of_surjective h (toLocalizationMap (M.map g) Q)
+
 end
 
 end IsLocalization

Mathlib/RingTheory/Localization/Ideal.lean

@@ -64,6 +64,14 @@ theorem mem_map_algebraMap_iff {I : Ideal R} {z} : z ∈ Ideal.map (algebraMap R
     exact h.symm ▸ Ideal.mem_map_of_mem _ a.2
 #align is_localization.mem_map_algebra_map_iff IsLocalization.mem_map_algebraMap_iff
 
+lemma mk'_mem_map_algebraMap_iff (I : Ideal R) (x : R) (s : M) :
+    IsLocalization.mk' S x s ∈ I.map (algebraMap R S) ↔ ∃ s ∈ M, s * x ∈ I := by
+  rw [← Ideal.unit_mul_mem_iff_mem _ (IsLocalization.map_units S s), IsLocalization.mk'_spec',
+    IsLocalization.mem_map_algebraMap_iff M]
+  simp_rw [← map_mul, IsLocalization.eq_iff_exists M, mul_comm x, ← mul_assoc, ← Submonoid.coe_mul]
+  exact ⟨fun ⟨⟨y, t⟩, c, h⟩ ↦ ⟨_, (c * t).2, h ▸ I.mul_mem_left c.1 y.2⟩, fun ⟨s, hs, h⟩ ↦
+    ⟨⟨⟨_, h⟩, ⟨s, hs⟩⟩, 1, by simp⟩⟩
+
 theorem map_comap (J : Ideal S) : Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J) = J :=
   le_antisymm (Ideal.map_le_iff_le_comap.2 le_rfl) fun x hJ => by
     obtain ⟨r, s, hx⟩ := mk'_surjective M x

Mathlib/RingTheory/Localization/Module.lean

@@ -213,6 +213,9 @@ def LinearMap.extendScalarsOfIsLocalization (f : M →ₗ[R] N) : M →ₗ[A] N
 @[simp] lemma LinearMap.extendScalarsOfIsLocalization_apply (f : M →ₗ[A] N) :
     f.extendScalarsOfIsLocalization S A = f := rfl
 
+@[simp] lemma LinearMap.extendScalarsOfIsLocalization_apply' (f : M →ₗ[R] N) (x : M) :
+    (f.extendScalarsOfIsLocalization S A) x = f x := rfl
+
 end
 
 end Localization