chore: Split Mathlib.RingTheory.Ideal.Norm (#19211)

We split `Mathlib.RingTheory.Ideal.Norm` into `Basic` and `RelNorm`. This is in preparation to generalize `Ideal.RelNorm` to nonfree extensions.

Mathlib.lean

@@ -4251,7 +4251,8 @@ import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.Maximal
 import Mathlib.RingTheory.Ideal.MinimalPrime
 import Mathlib.RingTheory.Ideal.Nonunits
-import Mathlib.RingTheory.Ideal.Norm
+import Mathlib.RingTheory.Ideal.Norm.AbsNorm
+import Mathlib.RingTheory.Ideal.Norm.RelNorm
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.Ideal.Over
 import Mathlib.RingTheory.Ideal.Pointwise

Mathlib/NumberTheory/Cyclotomic/Rat.lean

@@ -5,7 +5,7 @@ Authors: Riccardo Brasca
 -/
 import Mathlib.NumberTheory.Cyclotomic.Discriminant
 import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
-import Mathlib.RingTheory.Ideal.Norm
+import Mathlib.RingTheory.Ideal.Norm.AbsNorm
 
 /-!
 # Ring of integers of `p ^ n`-th cyclotomic fields

Mathlib/RingTheory/FractionalIdeal/Norm.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.RingTheory.FractionalIdeal.Basic
-import Mathlib.RingTheory.Ideal.Norm
+import Mathlib.RingTheory.Ideal.Norm.AbsNorm
+import Mathlib.RingTheory.Localization.NormTrace
 
 /-!
 

Mathlib/RingTheory/Ideal/Norm.lean → Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

@@ -8,28 +8,23 @@ import Mathlib.Data.Int.AbsoluteValue
 import Mathlib.Data.Int.Associated
 import Mathlib.LinearAlgebra.FreeModule.Determinant
 import Mathlib.LinearAlgebra.FreeModule.IdealQuotient
-import Mathlib.RingTheory.DedekindDomain.PID
-import Mathlib.RingTheory.Localization.NormTrace
+import Mathlib.RingTheory.DedekindDomain.Dvr
+import Mathlib.RingTheory.DedekindDomain.Ideal
+import Mathlib.RingTheory.Norm.Basic
 
 /-!
 
 # Ideal norms
 
 This file defines the absolute ideal norm `Ideal.absNorm (I : Ideal R) : ℕ` as the cardinality of
-the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite),
-and the relative ideal norm `Ideal.spanNorm R (I : Ideal S) : Ideal S` as the ideal spanned by
-the norms of elements in `I`.
+the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite).
 
 ## Main definitions
 
  * `Submodule.cardQuot (S : Submodule R M)`: the cardinality of the quotient `M ⧸ S`, in `ℕ`.
    This maps `⊥` to `0` and `⊤` to `1`.
  * `Ideal.absNorm (I : Ideal R)`: the absolute ideal norm, defined as
    the cardinality of the quotient `R ⧸ I`, as a bundled monoid-with-zero homomorphism.
- * `Ideal.spanNorm R (I : Ideal S)`: the ideal spanned by the norms of elements in `I`.
-    This is used to define `Ideal.relNorm`.
- * `Ideal.relNorm 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
 
@@ -39,10 +34,8 @@ the norms of elements in `I`.
    of the basis change matrix
  * `Ideal.absNorm_span_singleton`: the ideal norm of a principal ideal is the
    norm of its generator
- * `map_mul Ideal.relNorm`: multiplicativity of the relative ideal norm
 -/
 
-
 open scoped nonZeroDivisors
 
 section abs_norm
@@ -460,206 +453,3 @@ end Ideal
 end RingOfIntegers
 
 end abs_norm
-
-section SpanNorm
-
-namespace Ideal
-
-open Submodule
-
-variable (R : Type*) [CommRing R] {S : Type*} [CommRing S] [Algebra R S]
-
-/-- `Ideal.spanNorm R (I : Ideal S)` is the ideal generated by mapping `Algebra.norm R` over `I`.
-
-See also `Ideal.relNorm`.
--/
-def spanNorm (I : Ideal S) : Ideal R :=
-  Ideal.span (Algebra.norm R '' (I : Set S))
-
-@[simp]
-theorem spanNorm_bot [Nontrivial S] [Module.Free R S] [Module.Finite R S] :
-    spanNorm R (⊥ : Ideal S) = ⊥ := span_eq_bot.mpr fun x hx => by simpa using hx
-
-variable {R}
-
-@[simp]
-theorem spanNorm_eq_bot_iff [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S]
-    {I : Ideal S} : spanNorm R I = ⊥ ↔ I = ⊥ := by
-  simp only [spanNorm, Ideal.span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index,
-    and_imp, forall_apply_eq_imp_iff₂,
-    Algebra.norm_eq_zero_iff_of_basis (Module.Free.chooseBasis R S), @eq_bot_iff _ _ _ I,
-    SetLike.le_def]
-  rfl
-
-variable (R)
-
-theorem norm_mem_spanNorm {I : Ideal S} (x : S) (hx : x ∈ I) : Algebra.norm R x ∈ I.spanNorm R :=
-  subset_span (Set.mem_image_of_mem _ hx)
-
-@[simp]
-theorem spanNorm_singleton {r : S} : spanNorm R (span ({r} : Set S)) = span {Algebra.norm R r} :=
-  le_antisymm
-    (span_le.mpr fun x hx =>
-      mem_span_singleton.mpr
-        (by
-          obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
-          exact map_dvd _ (mem_span_singleton.mp hx')))
-    ((span_singleton_le_iff_mem _).mpr (norm_mem_spanNorm _ _ (mem_span_singleton_self _)))
-
-@[simp]
-theorem spanNorm_top : spanNorm R (⊤ : Ideal S) = ⊤ := by
-  -- Porting note: was
-  -- simp [← Ideal.span_singleton_one]
-  rw [← Ideal.span_singleton_one, spanNorm_singleton]
-  simp
-
-theorem map_spanNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
-    map f (spanNorm R I) = span (f ∘ Algebra.norm R '' (I : Set S)) := by
-  rw [spanNorm, map_span, Set.image_image]
-  -- Porting note: `Function.comp` reducibility
-  rfl
-
-@[mono]
-theorem spanNorm_mono {I J : Ideal S} (h : I ≤ J) : spanNorm R I ≤ spanNorm R J :=
-  Ideal.span_mono (Set.monotone_image h)
-
-theorem spanNorm_localization (I : Ideal S) [Module.Finite R S] [Module.Free R S] (M : Submonoid R)
-    {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ]
-    [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
-    [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] :
-    spanNorm Rₘ (I.map (algebraMap S Sₘ)) = (spanNorm R I).map (algebraMap R Rₘ) := by
-  cases subsingleton_or_nontrivial R
-  · haveI := IsLocalization.unique R Rₘ M
-    simp [eq_iff_true_of_subsingleton]
-  let b := Module.Free.chooseBasis R S
-  rw [map_spanNorm]
-  refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
-  · rintro a' ha'
-    simp only [Set.mem_preimage, submodule_span_eq, ← map_spanNorm, SetLike.mem_coe,
-      IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
-      IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
-    obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
-    refine ⟨⟨Algebra.norm R a, norm_mem_spanNorm _ _ ha⟩,
-      ⟨s ^ Fintype.card (Module.Free.ChooseBasisIndex R S), pow_mem hs _⟩, ?_⟩
-    simp only [Submodule.coe_mk, Subtype.coe_mk, map_pow] at has ⊢
-    apply_fun Algebra.norm Rₘ at has
-    rwa [_root_.map_mul, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ,
-      Algebra.norm_algebraMap_of_basis (b.localizationLocalization Rₘ M Sₘ),
-      Algebra.norm_localization R M a] at has
-  · intro a ha
-    rw [Set.mem_preimage, Function.comp_apply, ← Algebra.norm_localization (Sₘ := Sₘ) R M a]
-    exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))
-
-theorem spanNorm_mul_spanNorm_le (I J : Ideal S) :
-    spanNorm R I * spanNorm R J ≤ spanNorm R (I * J) := by
-  rw [spanNorm, spanNorm, spanNorm, Ideal.span_mul_span', ← Set.image_mul]
-  refine Ideal.span_mono (Set.monotone_image ?_)
-  rintro _ ⟨x, hxI, y, hyJ, rfl⟩
-  exact Ideal.mul_mem_mul hxI hyJ
-
-/-- This condition `eq_bot_or_top` is equivalent to being a field.
-However, `Ideal.spanNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
-instance to a `Field R` instance. -/
-theorem spanNorm_mul_of_bot_or_top [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S]
-    (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
-    spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
-  refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)
-  cases' eq_bot_or_top (spanNorm R I) with hI hI
-  · rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
-    exact bot_le
-  rw [hI, Ideal.top_mul]
-  cases' eq_bot_or_top (spanNorm R J) with hJ hJ
-  · rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
-  rw [hJ]
-  exact le_top
-
-@[simp]
-theorem spanNorm_mul_of_field {K : Type*} [Field K] [Algebra K S] [IsDomain S] [Module.Finite K S]
-    (I J : Ideal S) : spanNorm K (I * J) = spanNorm K I * spanNorm K J :=
-  spanNorm_mul_of_bot_or_top K eq_bot_or_top I J
-
-variable [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S]
-variable [Module.Finite R S] [Module.Free R S]
-
-/-- Multiplicativity of `Ideal.spanNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`. -/
-theorem spanNorm_mul (I J : Ideal S) : spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
-  nontriviality R
-  cases subsingleton_or_nontrivial S
-  · have : ∀ I : Ideal S, I = ⊤ := fun I => Subsingleton.elim I ⊤
-    simp [this I, this J, this (I * J)]
-  refine eq_of_localization_maximal ?_
-  intro P hP
-  by_cases hP0 : P = ⊥
-  · subst hP0
-    rw [spanNorm_mul_of_bot_or_top]
-    intro I
-    refine or_iff_not_imp_right.mpr fun hI => ?_
-    exact (hP.eq_of_le hI bot_le).symm
-  let P' := Algebra.algebraMapSubmonoid S P.primeCompl
-  letI : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S
-  haveI : IsScalarTower R (Localization.AtPrime P) (Localization P') :=
-    IsScalarTower.of_algebraMap_eq (fun x =>
-      (IsLocalization.map_eq (T := P') (Q := Localization P') P.primeCompl.le_comap_map x).symm)
-  have h : P' ≤ S⁰ :=
-    map_le_nonZeroDivisors_of_injective _ (NoZeroSMulDivisors.algebraMap_injective _ _)
-      P.primeCompl_le_nonZeroDivisors
-  haveI : IsDomain (Localization P') := IsLocalization.isDomain_localization h
-  haveI : IsDedekindDomain (Localization P') := IsLocalization.isDedekindDomain S h _
-  letI := Classical.decEq (Ideal (Localization P'))
-  haveI : IsPrincipalIdealRing (Localization P') :=
-    IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P hP0
-  rw [Ideal.map_mul, ← spanNorm_localization R I P.primeCompl (Localization P'),
-    ← spanNorm_localization R J P.primeCompl (Localization P'),
-    ← spanNorm_localization R (I * J) P.primeCompl (Localization P'), Ideal.map_mul,
-    ← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
-    span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
-    spanNorm_singleton, span_singleton_mul_span_singleton, _root_.map_mul]
-
-/-- The relative norm `Ideal.relNorm 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 relNorm : Ideal S →*₀ Ideal R where
-  toFun := spanNorm R
-  map_zero' := spanNorm_bot R
-  map_one' := by dsimp only; rw [one_eq_top, spanNorm_top R, one_eq_top]
-  map_mul' := spanNorm_mul R
-
-theorem relNorm_apply (I : Ideal S) : relNorm R I = span (Algebra.norm R '' (I : Set S) : Set R) :=
-  rfl
-
-@[simp]
-theorem spanNorm_eq (I : Ideal S) : spanNorm R I = relNorm R I := rfl
-
-@[simp]
-theorem relNorm_bot : relNorm R (⊥ : Ideal S) = ⊥ := by
-  simpa only [zero_eq_bot] using map_zero (relNorm R : Ideal S →*₀ _)
-
-@[simp]
-theorem relNorm_top : relNorm R (⊤ : Ideal S) = ⊤ := by
-  simpa only [one_eq_top] using map_one (relNorm R : Ideal S →*₀ _)
-
-variable {R}
-
-@[simp]
-theorem relNorm_eq_bot_iff {I : Ideal S} : relNorm R I = ⊥ ↔ I = ⊥ :=
-  spanNorm_eq_bot_iff
-
-variable (R)
-
-theorem norm_mem_relNorm (I : Ideal S) {x : S} (hx : x ∈ I) : Algebra.norm R x ∈ relNorm R I :=
-  norm_mem_spanNorm R x hx
-
-@[simp]
-theorem relNorm_singleton (r : S) : relNorm R (span ({r} : Set S)) = span {Algebra.norm R r} :=
-  spanNorm_singleton R
-
-theorem map_relNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) :
-    map f (relNorm R I) = span (f ∘ Algebra.norm R '' (I : Set S)) :=
-  map_spanNorm R I f
-
-@[mono]
-theorem relNorm_mono {I J : Ideal S} (h : I ≤ J) : relNorm R I ≤ relNorm R J :=
-  spanNorm_mono R h
-
-end Ideal
-
-end SpanNorm