feat(ring_theory): (strict) monotonicity of coe_submodule (#8273)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/ring_theory/localization.lean

@@ -1005,6 +1005,10 @@ lemma mem_coe_submodule (I : ideal R) {x : S} :
   x ∈ coe_submodule S I ↔ ∃ y : R, y ∈ I ∧ algebra_map R S y = x :=
 iff.rfl
 
+lemma coe_submodule_mono {I J : ideal R} (h : I ≤ J) :
+  coe_submodule S I ≤ coe_submodule S J :=
+submodule.map_mono h
+
 @[simp] lemma coe_submodule_top : coe_submodule S (⊤ : ideal R) = 1 :=
 by rw [coe_submodule, submodule.map_top, submodule.one_eq_range]
 
@@ -1149,6 +1153,19 @@ begin
   convert is_localization.injective _ hM hxy; simp,
 end
 
+variables {S Q M}
+
+@[mono]
+lemma coe_submodule_le_coe_submodule (h : M ≤ non_zero_divisors R)
+  {I J : ideal R} :
+  coe_submodule S I ≤ coe_submodule S J ↔ I ≤ J :=
+submodule.map_le_map_iff_of_injective (is_localization.injective _ h) _ _
+
+@[mono]
+lemma coe_submodule_strict_mono (h : M ≤ non_zero_divisors R) :
+  strict_mono (coe_submodule S : ideal R → submodule R S) :=
+strict_mono_of_le_iff_le (λ _ _, (coe_submodule_le_coe_submodule h).symm)
+
 variables (S) {Q M}
 
 /-- A `comm_ring` `S` which is the localization of an integral domain `R` at a subset of
@@ -1372,6 +1389,16 @@ is_localization.injective _ (le_of_eq rfl)
 
 variables {R K}
 
+@[simp, mono]
+lemma coe_submodule_le_coe_submodule
+  {I J : ideal R} : coe_submodule K I ≤ coe_submodule K J ↔ I ≤ J :=
+is_localization.coe_submodule_le_coe_submodule (le_refl _)
+
+@[mono]
+lemma coe_submodule_strict_mono :
+  strict_mono (coe_submodule K : ideal R → submodule R K) :=
+strict_mono_of_le_iff_le (λ _ _, coe_submodule_le_coe_submodule.symm)
+
 protected lemma to_map_ne_zero_of_mem_non_zero_divisors [nontrivial R]
   {x : R} (hx : x ∈ non_zero_divisors R) : algebra_map R K x ≠ 0 :=
 is_localization.to_map_ne_zero_of_mem_non_zero_divisors _ (le_refl _) hx