feat(ring_theory): definition and properties of relative ideal norm (#…

…18299)

This PR provides a definition of the relative ideal norm `ideal.span_norm R I` as the ideal spanned by the norms of elements in `I`. We also give some basic results on this definition. A follow-up PR will bundle this into a homomorphism `ideal.rel_norm`.

src/ring_theory/ideal/norm.lean

@@ -14,21 +14,25 @@ import linear_algebra.free_module.ideal_quotient
 import linear_algebra.free_module.pid
 import linear_algebra.isomorphisms
 import ring_theory.dedekind_domain.ideal
-import ring_theory.norm
+import ring_theory.localization.norm
 
 /-!
 
 # Ideal norms
 
 This file defines the absolute ideal norm `ideal.abs_norm (I : ideal R) : ℕ` as the cardinality of
-the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite).
+the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite),
+and the relative ideal norm `ideal.span_norm R (I : ideal S) : ideal S` as the ideal spanned by
+the norms of elements in `I`.
 
 ## Main definitions
 
  * `submodule.card_quot (S : submodule R M)`: the cardinality of the quotient `M ⧸ S`, in `ℕ`.
    This maps `⊥` to `0` and `⊤` to `1`.
  * `ideal.abs_norm (I : ideal R)`: the absolute ideal norm, defined as
    the cardinality of the quotient `R ⧸ I`, as a bundled monoid-with-zero homomorphism.
+ * `ideal.span_norm R (I : ideal S)`: the relative ideal norm, defined as
+   the ideal spanned by the norms of elements in `I`.
 
 ## Main results
 
@@ -38,13 +42,12 @@ the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite).
    of the basis change matrix
  * `ideal.abs_norm_span_singleton`: the ideal norm of a principal ideal is the
    norm of its generator
-
-## TODO
-
-Define the relative norm.
 -/
 
 open_locale big_operators
+open_locale non_zero_divisors
+
+section abs_norm
 
 namespace submodule
 
@@ -408,3 +411,86 @@ lemma prime_of_irreducible_abs_norm_span {a : S} (ha : a ≠ 0)
 (ideal.span_singleton_prime ha).mp (is_prime_of_irreducible_abs_norm hI)
 
 end ideal
+
+end abs_norm
+
+section span_norm
+
+namespace ideal
+
+open submodule
+
+variables (R : Type*) [comm_ring R] {S : Type*} [comm_ring S] [algebra R S]
+
+/-- `ideal.span_norm R (I : ideal S)` is the ideal generated by mapping `algebra.norm R` over `I`.
+-/
+def span_norm (I : ideal S) : ideal R :=
+ideal.span (algebra.norm R '' (I : set S))
+
+@[simp] lemma span_norm_bot
+  [nontrivial S] [module.free R S] [module.finite R S] :
+  span_norm R (⊥ : ideal S) = ⊥ :=
+span_eq_bot.mpr (λ x hx, by simpa using hx)
+
+lemma norm_mem_span_norm {I : ideal S} (x : S) (hx : x ∈ I) : algebra.norm R x ∈ I.span_norm R :=
+subset_span (set.mem_image_of_mem _ hx)
+
+@[simp] lemma span_norm_singleton {r : S} :
+  span_norm R (span ({r} : set S)) = span {algebra.norm R r} :=
+le_antisymm
+  (span_le.mpr (λ x hx, mem_span_singleton.mpr begin
+    obtain ⟨x, hx', rfl⟩ := (set.mem_image _ _ _).mp hx,
+    exact map_dvd _ (mem_span_singleton.mp hx')
+  end))
+  ((span_singleton_le_iff_mem _).mpr (norm_mem_span_norm _ _ (mem_span_singleton_self _)))
+
+@[simp] lemma span_norm_top : span_norm R (⊤ : ideal S) = 1 :=
+by simp [← ideal.span_singleton_one]
+
+lemma map_span_norm (I : ideal S) {T : Type*} [comm_ring T] (f : R →+* T) :
+  map f (span_norm R I) = span ((f ∘ algebra.norm R) '' (I : set S)) :=
+by rw [span_norm, map_span, set.image_image]
+
+@[mono]
+lemma span_norm_mono {I J : ideal S} (h : I ≤ J) : span_norm R I ≤ span_norm R J :=
+ideal.span_mono (set.monotone_image h)
+
+lemma span_norm_localization (I : ideal S) [module.finite R S] [module.free R S]
+  {M : submonoid R} {Rₘ Sₘ : Type*}
+  [comm_ring Rₘ] [algebra R Rₘ] [comm_ring Sₘ] [algebra S Sₘ]
+  [algebra Rₘ Sₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ]
+  [is_localization M Rₘ] [is_localization (algebra.algebra_map_submonoid S M) Sₘ]
+  (hM : algebra.algebra_map_submonoid S M ≤ S⁰) :
+  span_norm Rₘ (I.map (algebra_map S Sₘ)) = (span_norm R I).map (algebra_map R Rₘ) :=
+begin
+  casesI h : subsingleton_or_nontrivial R,
+  { haveI := is_localization.unique R Rₘ M,
+    simp },
+  let b := module.free.choose_basis R S,
+  rw map_span_norm,
+  refine span_eq_span (set.image_subset_iff.mpr _) (set.image_subset_iff.mpr _),
+  { rintros a' ha',
+    simp only [set.mem_preimage, submodule_span_eq, ← map_span_norm, set_like.mem_coe,
+        is_localization.mem_map_algebra_map_iff (algebra.algebra_map_submonoid S M) Sₘ,
+        is_localization.mem_map_algebra_map_iff M Rₘ, prod.exists]
+      at ⊢ ha',
+    obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha',
+    refine ⟨⟨algebra.norm R a, norm_mem_span_norm _ _ ha⟩,
+            ⟨s ^ fintype.card (module.free.choose_basis_index R S), pow_mem hs _⟩, _⟩,
+    swap,
+    simp only [submodule.coe_mk, subtype.coe_mk, map_pow] at ⊢ has,
+    apply_fun algebra.norm Rₘ at has,
+    rwa [_root_.map_mul, ← is_scalar_tower.algebra_map_apply,
+        is_scalar_tower.algebra_map_apply R Rₘ,
+        algebra.norm_algebra_map_of_basis (b.localization_localization Rₘ M Sₘ hM),
+        algebra.norm_localization R a hM] at has,
+    all_goals { apply_instance} },
+  { intros a ha,
+    rw [set.mem_preimage, function.comp_app, ← algebra.norm_localization R a hM],
+    exact subset_span (set.mem_image_of_mem _ (mem_map_of_mem _ ha)),
+    all_goals { apply_instance} },
+end
+
+end ideal
+
+end span_norm