feat: Generalize absNorm to fractional ideals (#9613)

This PR defines the absolute ideal norm of a fractional ideal `I : FractionalIdeal R⁰ K` where
`K` is a fraction field of `R` as a zero-preserving group homomorphism with values in `ℚ` and proves that it generalises the norm on (integral) ideals  (and some other classical result). 

Also in this PR:
- Add the directory `Mathlib/RingTheory/FractionalIdeal` and move the file `Mathlib/RingTheory/FractionalIdeal.lean` to `Mathlib/RingTheory/FractionalIdeal/Basic.lean`. The new results are in `Mathlib/RingTheory/FractionalIdeal/Norm.lean`
- Define the `numerator` and `denominator` of a fractional ideal. These are used to define the norm. Also define a linear equiv between a fractional ideal and its `numerator`.
- Several technical lemmas.

Mathlib.lean

@@ -3109,7 +3109,8 @@ import Mathlib.RingTheory.FiniteType
 import Mathlib.RingTheory.Finiteness
 import Mathlib.RingTheory.Fintype
 import Mathlib.RingTheory.Flat
-import Mathlib.RingTheory.FractionalIdeal
+import Mathlib.RingTheory.FractionalIdeal.Basic
+import Mathlib.RingTheory.FractionalIdeal.Norm
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.FreeRing
 import Mathlib.RingTheory.GradedAlgebra.Basic

Mathlib/Algebra/Algebra/Operations.lean

@@ -405,6 +405,21 @@ lemma mul_mem_smul_iff {S} [CommRing S] [Algebra R S] {x : S} {p : Submodule R S
     x * y ∈ x • p ↔ y ∈ p :=
   show Exists _ ↔ _ by simp [mul_cancel_left_mem_nonZeroDivisors hx]
 
+variable (M N) in
+theorem mul_smul_mul_eq_smul_mul_smul (x y : R) : (x * y) • (M * N) = (x • M) * (y • N) := by
+  ext
+  refine ⟨?_, fun hx ↦ Submodule.mul_induction_on hx ?_ fun _ _ hx hy ↦ Submodule.add_mem _ hx hy⟩
+  · rintro ⟨_, hx, rfl⟩
+    rw [DistribMulAction.toLinearMap_apply]
+    refine Submodule.mul_induction_on hx (fun m hm n hn ↦ ?_) (fun _ _ hn hm ↦ ?_)
+    · rw [← smul_mul_smul x y m n]
+      exact mul_mem_mul (smul_mem_pointwise_smul m x M hm) (smul_mem_pointwise_smul n y N hn)
+    · rw [smul_add]
+      exact Submodule.add_mem _ hn hm
+  · rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩
+    erw [smul_mul_smul x y m n]
+    exact smul_mem_pointwise_smul _ _ _ (mul_mem_mul hm hn)
+
 /-- Sub-R-modules of an R-algebra form an idempotent semiring. -/
 instance idemSemiring : IdemSemiring (Submodule R A) :=
   { toAddSubmonoid_injective.semigroup _ fun m n : Submodule R A => mul_toAddSubmonoid m n,

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -155,8 +155,11 @@ theorem dvd_cancel_left_mem_nonZeroDivisors {x y r : R'} (hr : r ∈ R'⁰) : r
 theorem dvd_cancel_left_coe_nonZeroDivisors {x y : R'} {c : R'⁰} : c * x ∣ c * y ↔ x ∣ y :=
   dvd_cancel_left_mem_nonZeroDivisors c.prop
 
-theorem nonZeroDivisors.ne_zero [Nontrivial M] {x} (hx : x ∈ M⁰) : x ≠ 0 := fun h ↦
-  one_ne_zero (hx _ <| (one_mul _).trans h)
+theorem zero_not_mem_nonZeroDivisors [Nontrivial M] : 0 ∉ M⁰ :=
+  fun h ↦ one_ne_zero <| h 1 <| mul_zero _
+
+theorem nonZeroDivisors.ne_zero [Nontrivial M] {x} (hx : x ∈ M⁰) : x ≠ 0 :=
+  ne_of_mem_of_not_mem hx zero_not_mem_nonZeroDivisors
 #align non_zero_divisors.ne_zero nonZeroDivisors.ne_zero
 
 theorem nonZeroDivisors.coe_ne_zero [Nontrivial M] (x : M⁰) : (x : M) ≠ 0 :=

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -166,6 +166,12 @@ theorem coe_equivMapOfInjective_apply (f : F) (i : Injective f) (p : Submodule R
   rfl
 #align submodule.coe_equiv_map_of_injective_apply Submodule.coe_equivMapOfInjective_apply
 
+@[simp]
+theorem map_equivMapOfInjective_symm_apply (f : F) (i : Injective f) (p : Submodule R M)
+    (x : p.map f) : f ((equivMapOfInjective f i p).symm x) = x := by
+  rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
+    i.eq_iff, LinearEquiv.apply_symm_apply]
+
 /-- The pullback of a submodule `p ⊆ M₂` along `f : M → M₂` -/
 def comap (f : F) (p : Submodule R₂ M₂) : Submodule R M :=
   { p.toAddSubmonoid.comap f with

Mathlib/LinearAlgebra/Matrix/Basis.lean

@@ -118,6 +118,13 @@ theorem sum_toMatrix_smul_self [Fintype ι] : ∑ i : ι, e.toMatrix v i j • e
   simp_rw [e.toMatrix_apply, e.sum_repr]
 #align basis.sum_to_matrix_smul_self Basis.sum_toMatrix_smul_self
 
+theorem toMatrix_smul {R₁ S : Type*} [CommRing R₁] [Ring S] [Algebra R₁ S] [Fintype ι]
+    [DecidableEq ι] (x : S) (b : Basis ι R₁ S) (w : ι → S) :
+    (b.toMatrix (x • w)) = (Algebra.leftMulMatrix b x) * (b.toMatrix w) := by
+  ext
+  rw [Basis.toMatrix_apply, Pi.smul_apply, smul_eq_mul, ← Algebra.leftMulMatrix_mulVec_repr]
+  rfl
+
 theorem toMatrix_map_vecMul {S : Type*} [Ring S] [Algebra R S] [Fintype ι] (b : Basis ι R S)
     (v : ι' → S) : ((b.toMatrix v).map <| algebraMap R S).vecMul b = v := by
   ext i

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -8,7 +8,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian
 import Mathlib.Order.Hom.Basic
 import Mathlib.RingTheory.DedekindDomain.Basic
-import Mathlib.RingTheory.FractionalIdeal
+import Mathlib.RingTheory.FractionalIdeal.Basic
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.ChainOfDivisors
 

Mathlib/RingTheory/FractionalIdeal.lean → Mathlib/RingTheory/FractionalIdeal/Basic.lean

@@ -134,6 +134,40 @@ protected theorem isFractional (I : FractionalIdeal S P) : IsFractional S (I : S
   I.prop
 #align fractional_ideal.is_fractional FractionalIdeal.isFractional
 
+/-- An element of `S` such that `I.den • I = I.num`, see `FractionalIdeal.num` and
+`FractionalIdeal.den_mul_eq_num`. -/
+noncomputable def den (I : FractionalIdeal S P) : S :=
+  ⟨I.2.choose, I.2.choose_spec.1⟩
+
+/-- An ideal of `R` such that `I.den • I = I.num`, see `FractionalIdeal.den` and
+`FractionalIdeal.den_mul_eq_num`. -/
+noncomputable def num (I : FractionalIdeal S P) : Ideal R :=
+  (I.den • (I : Submodule R P)).comap (Algebra.linearMap R P)
+
+theorem den_mul_self_eq_num (I : FractionalIdeal S P) :
+    I.den • (I : Submodule R P) = Submodule.map (Algebra.linearMap R P) I.num := by
+  rw [den, num, Submodule.map_comap_eq]
+  refine (inf_of_le_right ?_).symm
+  rintro _ ⟨a, ha, rfl⟩
+  exact I.2.choose_spec.2 a ha
+
+/-- The linear equivalence between the fractional ideal `I` and the integral ideal `I.num`
+defined by mapping `x` to `den I • x`. -/
+noncomputable def equivNum [Nontrivial P] [NoZeroSMulDivisors R P]
+    {I : FractionalIdeal S P} (h_nz : (I.den : R) ≠ 0) : I ≃ₗ[R] I.num := by
+  refine LinearEquiv.trans
+    (LinearEquiv.ofBijective ((DistribMulAction.toLinearMap R P I.den).restrict fun _ hx ↦ ?_)
+      ⟨fun _ _ hxy ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩)
+    (Submodule.equivMapOfInjective (Algebra.linearMap R P)
+      (NoZeroSMulDivisors.algebraMap_injective R P) (num I)).symm
+  · rw [← den_mul_self_eq_num]
+    exact Submodule.smul_mem_pointwise_smul _ _ _ hx
+  · simp_rw [LinearMap.restrict_apply, DistribMulAction.toLinearMap_apply, Subtype.mk.injEq] at hxy
+    rwa [Submonoid.smul_def, Submonoid.smul_def, smul_right_inj h_nz, SetCoe.ext_iff] at hxy
+  · rw [← den_mul_self_eq_num] at hy
+    obtain ⟨x, hx, hxy⟩ := hy
+    exact ⟨⟨x, hx⟩, by simp_rw [LinearMap.restrict_apply, Subtype.ext_iff, ← hxy]; rfl⟩
+
 section SetLike
 
 instance : SetLike (FractionalIdeal S P) P where
@@ -150,6 +184,15 @@ theorem ext {I J : FractionalIdeal S P} : (∀ x, x ∈ I ↔ x ∈ J) → I = J
   SetLike.ext
 #align fractional_ideal.ext FractionalIdeal.ext
 
+@[simp]
+ theorem equivNum_apply [Nontrivial P] [NoZeroSMulDivisors R P] {I : FractionalIdeal S P}
+    (h_nz : (I.den : R) ≠ 0) (x : I) :
+    algebraMap R P (equivNum h_nz x) = I.den • x := by
+  change Algebra.linearMap R P _ = _
+  rw [equivNum, LinearEquiv.trans_apply, LinearEquiv.ofBijective_apply, LinearMap.restrict_apply,
+    Submodule.map_equivMapOfInjective_symm_apply, Subtype.coe_mk,
+    DistribMulAction.toLinearMap_apply]
+
 /-- Copy of a `FractionalIdeal` with a new underlying set equal to the old one.
 Useful to fix definitional equalities. -/
 protected def copy (p : FractionalIdeal S P) (s : Set P) (hs : s = ↑p) : FractionalIdeal S P :=
@@ -337,6 +380,19 @@ instance : Inhabited (FractionalIdeal S P) :=
 instance : One (FractionalIdeal S P) :=
   ⟨(⊤ : Ideal R)⟩
 
+theorem zero_of_num_eq_bot [NoZeroSMulDivisors R P] (hS : 0 ∉ S) {I : FractionalIdeal S P}
+    (hI : I.num = ⊥) : I = 0 := by
+  rw [← coeToSubmodule_eq_bot, eq_bot_iff]
+  intro x hx
+  suffices (den I : R) • x = 0 from
+    (smul_eq_zero.mp this).resolve_left (ne_of_mem_of_not_mem (SetLike.coe_mem _) hS)
+  have h_eq : I.den • (I : Submodule R P) = ⊥ := by rw [den_mul_self_eq_num, hI, Submodule.map_bot]
+  exact (Submodule.eq_bot_iff _).mp h_eq (den I • x) ⟨x, hx, rfl⟩
+
+theorem num_zero_eq (h_inj : Function.Injective (algebraMap R P)) :
+    num (0 : FractionalIdeal S P) = 0 := by
+  simpa [num, LinearMap.ker_eq_bot] using h_inj
+
 variable (S)
 
 @[simp, norm_cast]
@@ -1305,6 +1361,17 @@ theorem mem_spanSingleton_self (x : P) : x ∈ spanSingleton S x :=
   (mem_spanSingleton S).mpr ⟨1, one_smul _ _⟩
 #align fractional_ideal.mem_span_singleton_self FractionalIdeal.mem_spanSingleton_self
 
+/-- A version of `FractionalIdeal.den_mul_self_eq_num` in terms of fractional ideals. -/
+theorem den_mul_self_eq_num' (I : FractionalIdeal S P) :
+    spanSingleton S (algebraMap R P I.den) * I = I.num := by
+  apply coeToSubmodule_injective
+  dsimp only
+  rw [coe_mul, ← smul_eq_mul, coe_spanSingleton, smul_eq_mul, Submodule.span_singleton_mul]
+  convert I.den_mul_self_eq_num using 1
+  ext
+  erw [Set.mem_smul_set, Set.mem_smul_set]
+  simp [Algebra.smul_def]
+
 variable {S}
 
 @[simp]

Mathlib/RingTheory/FractionalIdeal/Norm.lean

@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2024 Xavier Roblot. All rights reserved.
+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
+
+/-!
+
+# Fractional ideal norms
+
+This file defines the absolute ideal norm of a fractional ideal `I : FractionalIdeal R⁰ K` where
+`K` is a fraction field of `R`. The norm is defined by
+`FractionalIdeal.absNorm I = Ideal.absNorm I.num / |Algebra.norm ℤ I.den|` where `I.num` is an
+ideal of `R` and `I.den` an element of `R⁰` such that `I.den • I = I.num`.
+
+## Main definitions and results
+
+ * `FractionalIdeal.absNorm`: the norm as a zero preserving morphism with values in `ℚ`.
+ * `FractionalIdeal.absNorm_eq'`: the value of the norm does not depend on the choice of
+   `I.num` and `I.den`.
+ * `FractionalIdeal.abs_det_basis_change`: the norm is given by the determinant
+    of the basis change matrix.
+ * `FractionalIdeal.absNorm_span_singleton`: the norm of a principal fractional ideal is the
+   norm of its generator
+-/
+
+namespace FractionalIdeal
+
+open scoped Pointwise nonZeroDivisors
+
+variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R]
+
+variable {K : Type*} [CommRing K] [Algebra R K] [IsFractionRing R K]
+
+theorem absNorm_div_norm_eq_absNorm_div_norm {I : FractionalIdeal R⁰ K} (a : R⁰) (I₀ : Ideal R)
+    (h : a • (I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀) :
+    (Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den:R)| =
+      (Ideal.absNorm I₀ : ℚ) / |Algebra.norm ℤ (a:R)| := by
+  rw [div_eq_div_iff]
+  · replace h := congr_arg (I.den • ·) h
+    have h' := congr_arg (a • ·) (den_mul_self_eq_num I)
+    dsimp only at h h'
+    rw [smul_comm] at h
+    rw [h, Submonoid.smul_def, Submonoid.smul_def, ← Submodule.ideal_span_singleton_smul,
+      ← Submodule.ideal_span_singleton_smul, ← Submodule.map_smul'', ← Submodule.map_smul'',
+      (LinearMap.map_injective ?_).eq_iff, smul_eq_mul, smul_eq_mul] at h'
+    · simp_rw [← Int.cast_natAbs, ← Nat.cast_mul, ← Ideal.absNorm_span_singleton]
+      rw [← _root_.map_mul, ← _root_.map_mul, mul_comm, ← h', mul_comm]
+    · exact LinearMap.ker_eq_bot.mpr (IsFractionRing.injective R K)
+  all_goals simpa [Algebra.norm_eq_zero_iff] using nonZeroDivisors.coe_ne_zero _
+
+/-- The absolute norm of the fractional ideal `I` extending by multiplicativity the absolute norm
+on (integral) ideals. -/
+noncomputable def absNorm : FractionalIdeal R⁰ K →*₀ ℚ where
+  toFun I := (Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den : R)|
+  map_zero' := by
+    dsimp only
+    rw [num_zero_eq, Submodule.zero_eq_bot, Ideal.absNorm_bot, Nat.cast_zero, zero_div]
+    exact IsFractionRing.injective R K
+  map_one' := by
+    dsimp only
+    rw [absNorm_div_norm_eq_absNorm_div_norm 1 ⊤ (by simp [Submodule.one_eq_range]),
+      Ideal.absNorm_top, Nat.cast_one, OneMemClass.coe_one, _root_.map_one,  abs_one, Int.cast_one,
+      one_div_one]
+  map_mul' I J := by
+    dsimp only
+    rw [absNorm_div_norm_eq_absNorm_div_norm (I.den * J.den) (I.num * J.num) (by
+        have : Algebra.linearMap R K = (IsScalarTower.toAlgHom R R K).toLinearMap := rfl
+        rw [coe_mul, this, Submodule.map_mul, ← this, ← den_mul_self_eq_num, ← den_mul_self_eq_num]
+        exact Submodule.mul_smul_mul_eq_smul_mul_smul _ _ _ _),
+      Submonoid.coe_mul, _root_.map_mul, _root_.map_mul, Nat.cast_mul, div_mul_div_comm,
+      Int.cast_abs, Int.cast_abs, Int.cast_abs, ← abs_mul, Int.cast_mul]
+
+theorem absNorm_eq (I : FractionalIdeal R⁰ K) :
+    absNorm I = (Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den : R)| := rfl
+
+theorem absNorm_eq' {I : FractionalIdeal R⁰ K} (a : R⁰) (I₀ : Ideal R)
+    (h : a • (I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀) :
+    absNorm I = (Ideal.absNorm I₀ : ℚ) / |Algebra.norm ℤ (a:R)| := by
+  rw [absNorm, ← absNorm_div_norm_eq_absNorm_div_norm a I₀ h, MonoidWithZeroHom.coe_mk,
+    ZeroHom.coe_mk]
+
+theorem absNorm_nonneg (I : FractionalIdeal R⁰ K) : 0 ≤ absNorm I := by dsimp [absNorm]; positivity
+
+theorem absNorm_bot : absNorm (⊥ : FractionalIdeal R⁰ K) = 0 := absNorm.map_zero'
+
+theorem absNorm_one : absNorm (1 : FractionalIdeal R⁰ K) = 1 := by convert absNorm.map_one'
+
+theorem absNorm_eq_zero_iff [NoZeroDivisors K] {I : FractionalIdeal R⁰ K} :
+    absNorm I = 0 ↔ I = 0 := by
+  refine ⟨fun h ↦ zero_of_num_eq_bot zero_not_mem_nonZeroDivisors ?_, fun h ↦ h ▸ absNorm_bot⟩
+  rw [absNorm_eq, div_eq_zero_iff] at h
+  refine Ideal.absNorm_eq_zero_iff.mp <| Nat.cast_eq_zero.mp <| h.resolve_right ?_
+  simpa [Algebra.norm_eq_zero_iff] using nonZeroDivisors.coe_ne_zero _
+
+theorem coeIdeal_absNorm (I₀ : Ideal R) :
+    absNorm (I₀ : FractionalIdeal R⁰ K) = Ideal.absNorm I₀ := by
+  rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, _root_.map_one, abs_one,
+    Int.cast_one, _root_.div_one]
+
+section IsLocalization
+
+variable [IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K] [Algebra ℚ K]
+
+theorem abs_det_basis_change [NoZeroDivisors K] {ι : Type*} [Fintype ι]
+    [DecidableEq ι] (b : Basis ι ℤ R) (I : FractionalIdeal R⁰ K) (bI : Basis ι ℤ I) :
+    |(b.localizationLocalization ℚ ℤ⁰ K).det ((↑) ∘ bI)| = absNorm I := by
+  have := IsFractionRing.nontrivial R K
+  let b₀ : Basis ι ℚ K := b.localizationLocalization ℚ ℤ⁰ K
+  let bI.num : Basis ι ℤ I.num := bI.map
+      ((equivNum (nonZeroDivisors.coe_ne_zero _)).restrictScalars ℤ)
+  rw [absNorm_eq, ← Ideal.natAbs_det_basis_change b I.num bI.num, Int.cast_natAbs, Int.cast_abs,
+    Int.cast_abs, Basis.det_apply, Basis.det_apply]
+  change _ = |algebraMap ℤ ℚ _| / _
+  rw [RingHom.map_det, show RingHom.mapMatrix (algebraMap ℤ ℚ) (b.toMatrix ((↑) ∘ bI.num)) =
+      b₀.toMatrix ((algebraMap R K (den I : R)) • ((↑) ∘ bI)) by
+    ext : 2
+    simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
+      ← Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply,
+      Basis.map_apply, LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def,
+      Algebra.smul_def]
+    rfl]
+  rw [Basis.toMatrix_smul, Matrix.det_mul, abs_mul, ← Algebra.norm_eq_matrix_det,
+    Algebra.norm_localization ℤ ℤ⁰, show (Algebra.norm ℤ (den I: R) : ℚ) =
+    algebraMap ℤ ℚ (Algebra.norm ℤ (den I: R)) by rfl, mul_div_assoc, mul_div_cancel' _ (by
+    rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
+    exact nonZeroDivisors.coe_ne_zero _)]
+
+variable (R) in
+@[simp]
+theorem absNorm_span_singleton [Module.Finite ℚ K] (x : K) :
+    absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ x)| := by
+  have : IsDomain K := IsFractionRing.isDomain R
+  obtain ⟨d, ⟨r, hr⟩⟩ := IsLocalization.exists_integer_multiple R⁰ x
+  rw [absNorm_eq' d (Ideal.span {r})]
+  · rw [Ideal.absNorm_span_singleton]
+    simp_rw [Int.cast_natAbs, Int.cast_abs, show ((Algebra.norm ℤ _) : ℚ) = algebraMap ℤ ℚ
+      (Algebra.norm ℤ _) by rfl, ← Algebra.norm_localization ℤ ℤ⁰ (Sₘ := K) _]
+    rw [hr, Algebra.smul_def, _root_.map_mul, abs_mul, mul_div_assoc, mul_div_cancel' _ (by
+      rw [ne_eq, abs_eq_zero, Algebra.norm_eq_zero_iff, IsFractionRing.to_map_eq_zero_iff]
+      exact nonZeroDivisors.coe_ne_zero _)]
+  · ext
+    simp_rw [← SetLike.mem_coe, Submodule.coe_pointwise_smul, Set.mem_smul_set, SetLike.mem_coe,
+      mem_coe, mem_spanSingleton, Submodule.mem_map, Algebra.linearMap_apply, Submonoid.smul_def,
+      Ideal.mem_span_singleton', exists_exists_eq_and, _root_.map_mul, hr, ← Algebra.smul_def,
+      smul_comm (d : R)]
+
+end IsLocalization