feat(ring_theory/localization): lemmas about Frac(R)-spans (#12425)

Vierkantor · Vierkantor · commit 1ebb20602a8c · 2022-03-28T11:38:54.000Z
A couple of lemmas relating spans in the localization of `R` to spans in `R` itself.





Co-authored-by: Anne Baanen &lt;Vierkantor@users.noreply.github.com&gt;
diff --git a/src/algebra/algebra/tower.lean b/src/algebra/algebra/tower.lean
@@ -308,6 +308,25 @@ le_antisymm (span_le.2 $ λ x hx, let ⟨p, q, hps, hqt, hpqx⟩ := set.mem_smul
   (λ _ _, add_mem _)
   (λ k x hx, smul_mem_span_smul' hs hx)
 
+/-- A variant of `submodule.span_image` for `algebra_map`. -/
+lemma span_algebra_map_image (a : set R) :
+  submodule.span R (algebra_map R S '' a) =
+    (submodule.span R a).map (algebra.linear_map R S) :=
+(submodule.span_image $ algebra.linear_map R S).trans rfl
+
+lemma span_algebra_map_image_of_tower {S T : Type*} [comm_semiring S] [semiring T]
+  [module R S] [is_scalar_tower R S S] [algebra R T] [algebra S T] [is_scalar_tower R S T]
+  (a : set S) :
+  submodule.span R (algebra_map S T '' a) =
+    (submodule.span R a).map ((algebra.linear_map S T).restrict_scalars R) :=
+(submodule.span_image $ (algebra.linear_map S T).restrict_scalars R).trans rfl
+
+lemma map_mem_span_algebra_map_image {S T : Type*} [comm_semiring S] [semiring T]
+  [algebra R S] [algebra R T] [algebra S T] [is_scalar_tower R S T]
+  (x : S) (a : set S) (hx : x ∈ submodule.span R a) :
+  algebra_map S T x ∈ submodule.span R (algebra_map S T '' a) :=
+by { rw [span_algebra_map_image_of_tower, mem_map], exact ⟨x, hx, rfl⟩ }
+
 end submodule
 
 end semiring
diff --git a/src/ring_theory/localization/integral.lean b/src/ring_theory/localization/integral.lean
@@ -349,4 +349,42 @@ begin
       (no_zero_smul_divisors.algebra_map_injective _ _) _ hf₂ }
 end
 
+open_locale non_zero_divisors
+
+variables (R) {S K}
+/-- If the `S`-multiples of `a` are contained in some `R`-span, then `Frac(S)`-multiples of `a`
+are contained in the equivalent `Frac(R)`-span. -/
+lemma ideal_span_singleton_map_subset {L : Type*}
+  [is_domain R] [is_domain S] [field K] [field L]
+  [algebra R K] [algebra R L] [algebra S L] [is_integral_closure S R L]
+  [is_fraction_ring S L] [algebra K L] [is_scalar_tower R S L] [is_scalar_tower R K L]
+  {a : S} {b : set S} (alg : algebra.is_algebraic R L) (inj : function.injective (algebra_map R L))
+  (h : (ideal.span ({a} : set S) : set S) ⊆ submodule.span R b) :
+  (ideal.span ({algebra_map S L a} : set L) : set L) ⊆ submodule.span K (algebra_map S L '' b) :=
+begin
+  intros x hx,
+  obtain ⟨x', rfl⟩ := ideal.mem_span_singleton.mp hx,
+  obtain ⟨y', z', rfl⟩ := is_localization.mk'_surjective (S⁰) x',
+  obtain ⟨y, z, hz0, yz_eq⟩ := is_integral_closure.exists_smul_eq_mul alg inj y'
+    (non_zero_divisors.coe_ne_zero z'),
+  have injRS : function.injective (algebra_map R S),
+  { refine function.injective.of_comp
+      (show function.injective (algebra_map S L ∘ algebra_map R S), from _),
+    rwa [← ring_hom.coe_comp, ← is_scalar_tower.algebra_map_eq] },
+  have hz0' : algebra_map R S z ∈ S⁰ := map_mem_non_zero_divisors (algebra_map R S) injRS
+    (mem_non_zero_divisors_of_ne_zero hz0),
+  have mk_yz_eq : is_localization.mk' L y' z' = is_localization.mk' L y ⟨_, hz0'⟩,
+  { rw [algebra.smul_def, mul_comm _ y, mul_comm _ y', ← set_like.coe_mk (algebra_map R S z) hz0']
+        at yz_eq,
+    exact is_localization.mk'_eq_of_eq yz_eq.symm },
+  suffices hy : algebra_map S L (a * y) ∈ submodule.span K (⇑(algebra_map S L) '' b),
+  { rw [mk_yz_eq, is_fraction_ring.mk'_eq_div, set_like.coe_mk,
+        ← is_scalar_tower.algebra_map_apply, is_scalar_tower.algebra_map_apply R K L,
+        div_eq_mul_inv, ← mul_assoc, mul_comm, ← ring_hom.map_inv, ← algebra.smul_def,
+        ← _root_.map_mul],
+    exact (submodule.span K _).smul_mem _ hy },
+  refine submodule.span_subset_span R K _ _,
+  rw submodule.span_algebra_map_image_of_tower,
+  exact submodule.mem_map_of_mem (h (ideal.mem_span_singleton.mpr ⟨y, rfl⟩))
+end
 end is_fraction_ring
diff --git a/src/ring_theory/localization/submodule.lean b/src/ring_theory/localization/submodule.lean
@@ -114,6 +114,52 @@ begin
     rw [hx, ideal.submodule_span_eq, coe_submodule_span_singleton] }
 end
 
+variables {S} (M)
+lemma mem_span_iff {N : Type*} [add_comm_group N] [module R N] [module S N] [is_scalar_tower R S N]
+  {x : N} {a : set N} :
+  x ∈ submodule.span S a ↔ ∃ (y ∈ submodule.span R a) (z : M), x = mk' S 1 z • y :=
+begin
+  split, intro h,
+  { refine submodule.span_induction h _ _ _ _,
+    { rintros x hx,
+      exact ⟨x, submodule.subset_span hx, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩ },
+    { exact ⟨0, submodule.zero_mem _, 1, by rw [mk'_one, _root_.map_one, one_smul]⟩ },
+    { rintros _ _ ⟨y, hy, z, rfl⟩ ⟨y', hy', z', rfl⟩,
+      refine ⟨(z' : R) • y + (z : R) • y',
+        (submodule.add_mem _ (submodule.smul_mem _ _ hy) (submodule.smul_mem _ _ hy')), z * z', _⟩,
+      rw [smul_add, ← is_scalar_tower.algebra_map_smul S (z : R),
+          ← is_scalar_tower.algebra_map_smul S (z' : R), smul_smul, smul_smul],
+      congr' 1,
+      { rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec,
+            _root_.map_one, mul_one, mul_one] },
+      { rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec,
+            _root_.map_one, mul_one, one_mul] },
+      all_goals { apply_instance } },
+    { rintros a _ ⟨y, hy, z, rfl⟩,
+      obtain ⟨y', z', rfl⟩ := mk'_surjective M a,
+      refine ⟨y' • y, submodule.smul_mem _ _ hy, z' * z, _⟩,
+      rw [← is_scalar_tower.algebra_map_smul S y', smul_smul, ← mk'_mul,
+          smul_smul, mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_mul],
+      all_goals { apply_instance } } },
+  { rintro ⟨y, hy, z, rfl⟩,
+    exact submodule.smul_mem _ _ (submodule.span_subset_span R S _ hy) }
+end
+
+lemma mem_span_map {x : S} {a : set R} :
+  x ∈ ideal.span (algebra_map R S '' a) ↔
+    ∃ (y ∈ ideal.span a) (z : M), x = mk' S y z :=
+begin
+  refine (mem_span_iff M).trans _,
+  split,
+  { rw ← coe_submodule_span,
+    rintros ⟨_, ⟨y, hy, rfl⟩, z, hz⟩,
+    refine ⟨y, hy, z, _⟩,
+    rw [hz, algebra.linear_map_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one] },
+  { rintros ⟨y, hy, z, hz⟩,
+    refine ⟨algebra_map R S y, submodule.map_mem_span_algebra_map_image _ _ hy, z, _⟩,
+    rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one] },
+end
+
 end is_localization
 
 namespace is_fraction_ring
