feat(ring_theory/ideal/norm): relative ideal norm (#18303)

This PR contains the definition of `ideal.rel_norm`, the relative ideal norm as a bundled monoid-with-zero homomorphism sending `I : ideal S` to the ideal in `R` spanned by the norms of the elements in `I`; here `R` and `S` are Dedekind domains and `S` is an extension of `R` which is finite free as an `R`-module.

Co-Authored-By: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

src/algebra/char_p/quotient.lean

@@ -37,3 +37,15 @@ lemma quotient' {R : Type*} [comm_ring R] (p : ℕ) [char_p R p] (I : ideal R)
 end⟩
 
 end char_p
+
+lemma ideal.quotient.index_eq_zero {R : Type*} [comm_ring R] (I : ideal R) :
+  (I.to_add_subgroup.index : R ⧸ I) = 0 :=
+begin
+  rw [add_subgroup.index, nat.card_eq],
+  split_ifs with hq, swap, simp,
+  by_contra h,
+  -- TODO: can we avoid rewriting the `I.to_add_subgroup` here?
+  letI : fintype (R ⧸ I) := @fintype.of_finite _ hq,
+  have h : (fintype.card (R ⧸ I) : R ⧸ I) ≠ 0 := h,
+  simpa using h
+end

src/ring_theory/ideal/norm.lean

@@ -4,16 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Alex J. Best
 -/
 
+import algebra.char_p.quotient
 import data.finsupp.fintype
 import data.int.absolute_value
 import data.int.associated
-import data.matrix.notation
-import data.zmod.quotient
+import number_theory.ramification_inertia
 import linear_algebra.free_module.determinant
 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.dedekind_domain.pid
+import ring_theory.local_properties
 import ring_theory.localization.norm
 
 /-!
@@ -31,8 +30,10 @@ the norms of elements in `I`.
    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`.
+ * `ideal.span_norm R (I : ideal S)`: the ideal spanned by the norms of elements in `I`.
+    This is used to define `ideal.rel_norm`.
+ * `ideal.rel_norm R (I : ideal S)`: the relative ideal norm as a bundled monoid-with-zero morphism,
+   defined as the ideal spanned by the norms of elements in `I`.
 
 ## Main results
 
@@ -42,6 +43,7 @@ the norms of elements in `I`.
    of the basis change matrix
  * `ideal.abs_norm_span_singleton`: the ideal norm of a principal ideal is the
    norm of its generator
+ * `map_mul ideal.rel_norm`: multiplicativity of the relative ideal norm
 -/
 
 open_locale big_operators
@@ -82,6 +84,8 @@ end
 
 end submodule
 
+section ring_of_integers
+
 variables {S : Type*} [comm_ring S] [is_domain S]
 
 open submodule
@@ -383,6 +387,12 @@ end
 lemma abs_norm_dvd_abs_norm_of_le {I J : ideal S} (h : J ≤ I) : I.abs_norm ∣ J.abs_norm :=
 map_dvd abs_norm (dvd_iff_le.mpr h)
 
+lemma abs_norm_dvd_norm_of_mem {I : ideal S} {x : S} (h : x ∈ I) : ↑I.abs_norm ∣ algebra.norm ℤ x :=
+begin
+  rw [← int.dvd_nat_abs, ← abs_norm_span_singleton x, int.coe_nat_dvd],
+  exact abs_norm_dvd_abs_norm_of_le ((span_singleton_le_iff_mem _).mpr h)
+end
+
 @[simp]
 lemma abs_norm_span_insert (r : S) (s : set S) :
   abs_norm (span (insert r s)) ∣ gcd (abs_norm (span s)) (algebra.norm ℤ r).nat_abs :=
@@ -410,8 +420,14 @@ lemma prime_of_irreducible_abs_norm_span {a : S} (ha : a ≠ 0)
   prime a :=
 (ideal.span_singleton_prime ha).mp (is_prime_of_irreducible_abs_norm hI)
 
+lemma abs_norm_mem (I : ideal S) : ↑I.abs_norm ∈ I :=
+by rw [abs_norm_apply, card_quot, ← ideal.quotient.eq_zero_iff_mem, map_nat_cast,
+       quotient.index_eq_zero]
+
 end ideal
 
+end ring_of_integers
+
 end abs_norm
 
 section span_norm
@@ -423,6 +439,8 @@ 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`.
+
+See also `ideal.rel_norm`.
 -/
 def span_norm (I : ideal S) : ideal R :=
 ideal.span (algebra.norm R '' (I : set S))
@@ -432,6 +450,21 @@ ideal.span (algebra.norm R '' (I : set S))
   span_norm R (⊥ : ideal S) = ⊥ :=
 span_eq_bot.mpr (λ x hx, by simpa using hx)
 
+variables {R}
+
+@[simp] lemma span_norm_eq_bot_iff [is_domain R] [is_domain S]
+  [module.free R S] [module.finite R S] {I : ideal S} :
+  span_norm R I = ⊥ ↔ I = ⊥ :=
+begin
+  simp only [span_norm, ideal.span_eq_bot, set.mem_image, set_like.mem_coe, forall_exists_index,
+    and_imp, forall_apply_eq_imp_iff₂,
+    algebra.norm_eq_zero_iff_of_basis (module.free.choose_basis R S), @eq_bot_iff _ _ _ I,
+    set_like.le_def],
+  refl
+end
+
+variables (R)
+
 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)
 
@@ -444,7 +477,7 @@ le_antisymm
   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 :=
+@[simp] lemma span_norm_top : span_norm R (⊤ : ideal S) = ⊤ :=
 by simp [← ideal.span_singleton_one]
 
 lemma map_span_norm (I : ideal S) {T : Type*} [comm_ring T] (f : R →+* T) :
@@ -456,7 +489,7 @@ lemma span_norm_mono {I J : ideal S} (h : I ≤ J) : span_norm R I ≤ span_norm
 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*}
+  (M : submonoid R) {Rₘ : Type*} (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ₘ] :
@@ -490,6 +523,124 @@ begin
     all_goals { apply_instance } },
 end
 
+lemma span_norm_mul_span_norm_le (I J : ideal S) :
+  span_norm R I * span_norm R J ≤ span_norm R (I * J) :=
+begin
+  rw [span_norm, span_norm, span_norm, ideal.span_mul_span', ← set.image_mul],
+  refine ideal.span_mono (set.monotone_image _),
+  rintros _ ⟨x, y, hxI, hyJ, rfl⟩,
+  exact ideal.mul_mem_mul hxI hyJ
+end
+
+/-- This condition `eq_bot_or_top` is equivalent to being a field.
+However, `span_norm_mul_of_field` is harder to apply since we'd need to upgrade a `comm_ring R`
+instance to a `field R` instance. -/
+lemma span_norm_mul_of_bot_or_top [is_domain R] [is_domain S]
+  [module.free R S] [module.finite R S]
+  (eq_bot_or_top : ∀ I : ideal R, I = ⊥ ∨ I = ⊤)
+  (I J : ideal S) :
+  span_norm R (I * J) = span_norm R I * span_norm R J :=
+begin
+  refine le_antisymm _ (span_norm_mul_span_norm_le _ _ _),
+  cases eq_bot_or_top (span_norm R I) with hI hI,
+  { rw [hI, span_norm_eq_bot_iff.mp hI, bot_mul, span_norm_bot],
+    exact bot_le },
+  rw [hI, ideal.top_mul],
+  cases eq_bot_or_top (span_norm R J) with hJ hJ,
+  { rw [hJ, span_norm_eq_bot_iff.mp hJ, mul_bot, span_norm_bot],
+    exact bot_le },
+  rw hJ,
+  exact le_top
+end
+
+@[simp] lemma span_norm_mul_of_field {K : Type*} [field K] [algebra K S] [is_domain S]
+  [module.finite K S] (I J : ideal S) :
+  span_norm K (I * J) = span_norm K I * span_norm K J :=
+span_norm_mul_of_bot_or_top K eq_bot_or_top I J
+
+variables [is_domain R] [is_domain S] [is_dedekind_domain R] [is_dedekind_domain S]
+variables [module.finite R S] [module.free R S]
+
+/-- Multiplicativity of `ideal.span_norm`. simp-normal form is `map_mul (ideal.rel_norm R)`. -/
+lemma span_norm_mul (I J : ideal S) : span_norm R (I * J) = span_norm R I * span_norm R J :=
+begin
+  nontriviality R,
+  casesI subsingleton_or_nontrivial S,
+  { have : ∀ I : ideal S, I = ⊤ := λ I, subsingleton.elim I ⊤,
+    simp [this I, this J, this (I * J)] },
+  refine eq_of_localization_maximal _,
+  unfreezingI { intros P hP },
+  by_cases hP0 : P = ⊥,
+  { unfreezingI { subst hP0 },
+    rw span_norm_mul_of_bot_or_top,
+    intros I,
+    refine or_iff_not_imp_right.mpr (λ hI, _),
+    exact (hP.eq_of_le hI bot_le).symm },
+  let P' := algebra.algebra_map_submonoid S P.prime_compl,
+  letI : algebra (localization.at_prime P) (localization P') :=
+    localization_algebra P.prime_compl S,
+  haveI : is_scalar_tower R (localization.at_prime P) (localization P') :=
+    is_scalar_tower.of_algebra_map_eq (λ x, (is_localization.map_eq _ _).symm),
+  have h : P' ≤ S⁰ :=
+    map_le_non_zero_divisors_of_injective _ (no_zero_smul_divisors.algebra_map_injective _ _)
+      P.prime_compl_le_non_zero_divisors,
+  haveI : is_domain (localization P') := is_localization.is_domain_localization h,
+  haveI : is_dedekind_domain (localization P') := is_localization.is_dedekind_domain S h _,
+  letI := classical.dec_eq (ideal (localization P')),
+  haveI : is_principal_ideal_ring (localization P') :=
+    is_dedekind_domain.is_principal_ideal_ring_localization_over_prime S P hP0,
+  rw [ideal.map_mul, ← span_norm_localization R I P.prime_compl (localization P'),
+    ← span_norm_localization R J P.prime_compl (localization P'),
+    ← span_norm_localization R (I * J) P.prime_compl (localization P'), ideal.map_mul,
+    ← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
+    span_singleton_mul_span_singleton, span_norm_singleton, span_norm_singleton,
+    span_norm_singleton, span_singleton_mul_span_singleton, _root_.map_mul],
+  repeat { apply_instance },
+  repeat { assumption },
+end
+
+/-- The relative norm `ideal.rel_norm R (I : ideal S)`, where `R` and `S` are Dedekind domains,
+and `S` is an extension of `R` that is finite and free as a module. -/
+def rel_norm : ideal S →*₀ ideal R :=
+{ to_fun := span_norm R,
+  map_zero' := span_norm_bot R,
+  map_one' := by rw [one_eq_top, span_norm_top R, one_eq_top],
+  map_mul' := span_norm_mul R }
+
+lemma rel_norm_apply (I : ideal S) :
+  rel_norm R I = span (algebra.norm R '' (I : set S) : set R) :=
+rfl
+
+@[simp] lemma span_norm_eq (I : ideal S) : span_norm R I = rel_norm R I := rfl
+
+@[simp] lemma rel_norm_bot : rel_norm R (⊥ : ideal S) = ⊥ :=
+by simpa only [zero_eq_bot] using map_zero (rel_norm R : ideal S →*₀ _)
+
+@[simp] lemma rel_norm_top : rel_norm R (⊤ : ideal S) = ⊤ :=
+by simpa only [one_eq_top] using map_one (rel_norm R : ideal S →*₀ _)
+
+variables {R}
+
+@[simp] lemma rel_norm_eq_bot_iff {I : ideal S} : rel_norm R I = ⊥ ↔ I = ⊥ :=
+span_norm_eq_bot_iff
+
+variables (R)
+
+lemma norm_mem_rel_norm (I : ideal S) {x : S} (hx : x ∈ I) : algebra.norm R x ∈ rel_norm R I :=
+norm_mem_span_norm R x hx
+
+@[simp] lemma rel_norm_singleton (r : S) :
+  rel_norm R (span ({r} : set S)) = span {algebra.norm R r} :=
+span_norm_singleton R
+
+lemma map_rel_norm (I : ideal S) {T : Type*} [comm_ring T] (f : R →+* T) :
+  map f (rel_norm R I) = span ((f ∘ algebra.norm R) '' (I : set S)) :=
+map_span_norm R I f
+
+@[mono]
+lemma rel_norm_mono {I J : ideal S} (h : I ≤ J) : rel_norm R I ≤ rel_norm R J :=
+span_norm_mono R h
+
 end ideal
 
 end span_norm