feat(ring_theory/ideal): ideal norm evaluation lemmas (#17299)

This PR continues on #17203 by adding a couple lemmas on the ideal norm of some specific ideals:

 * the norm of `⊥` and `⊤`
 * the norm of an ideal `I : ideal S` given an additive isomorphism between `I` and `S`
 * the norm of the ideal generated by `a`
 * the norm of the ideal generated by `insert a s`

It also adds a selection of dependent lemmas. I couldn't find a really neat place for some of them: I think the current places are the least worst but I am very much open to suggestions.

Co-authored-by: Alex J Best <alex.j.best@gmail.com>



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/int/absolute_value.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import algebra.module.basic
-import group_theory.group_action.units
+import algebra.order.absolute_value
 import data.int.cast.lemmas
 import data.int.units
-import algebra.order.absolute_value
+import group_theory.group_action.units
 
 /-!
 # Absolute values and the integers
@@ -17,6 +17,7 @@ This file contains some results on absolute values applied to integers.
 ## Main results
 
  * `absolute_value.map_units_int`: an absolute value sends all units of `ℤ` to `1`
+ * `int.nat_abs_hom`: `int.nat_abs` bundled as a `monoid_with_zero_hom`
 -/
 
 variables {R S : Type*} [ring R] [linear_ordered_comm_ring S]
@@ -35,3 +36,11 @@ by rcases int.units_eq_one_or x with (rfl | rfl); simp
 lemma absolute_value.map_units_int_smul (abv : absolute_value R S) (x : ℤˣ) (y : R) :
   abv (x • y) = abv y :=
 by rcases int.units_eq_one_or x with (rfl | rfl); simp
+
+/-- `int.nat_abs` as a bundled monoid with zero hom. -/
+@[simps]
+def int.nat_abs_hom : ℤ →*₀ ℕ :=
+{ to_fun := int.nat_abs,
+  map_mul' := int.nat_abs_mul,
+  map_one' := int.nat_abs_one,
+  map_zero' := int.nat_abs_zero }

src/data/int/associated.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2022 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import algebra.associated
+import data.int.units
+
+/-!
+# Associated elements and the integers
+
+This file contains some results on equality up to units in the integers.
+
+## Main results
+
+ * `int.nat_abs_eq_iff_associated`: the absolute value is equal iff integers are associated
+-/
+
+lemma int.nat_abs_eq_iff_associated {a b : ℤ} :
+  a.nat_abs = b.nat_abs ↔ associated a b :=
+begin
+  refine int.nat_abs_eq_nat_abs_iff.trans _,
+  split,
+  { rintro (rfl | rfl),
+    { refl },
+    { exact ⟨-1, by simp⟩ } },
+  { rintro ⟨u, rfl⟩,
+    obtain (rfl | rfl) := int.units_eq_one_or u,
+    { exact or.inl (by simp) },
+    { exact or.inr (by simp) } }
+end

src/linear_algebra/determinant.lean

@@ -533,6 +533,16 @@ by { rw [basis.det_apply, basis.det_apply, ← f.det_to_matrix e, ← matrix.det
          e.to_matrix_eq_to_matrix_constr (f ∘ v), e.to_matrix_eq_to_matrix_constr v,
          ← to_matrix_comp, e.constr_comp] }
 
+@[simp] lemma basis.det_comp_basis [module A M']
+  (b : basis ι A M) (b' : basis ι A M') (f : M →ₗ[A] M') :
+  b'.det (f ∘ b) = linear_map.det (f ∘ₗ (b'.equiv b (equiv.refl ι) : M' →ₗ[A] M)) :=
+begin
+  rw [basis.det_apply, ← linear_map.det_to_matrix b', linear_map.to_matrix_comp _ b,
+      matrix.det_mul, linear_map.to_matrix_basis_equiv, matrix.det_one, mul_one],
+  congr' 1, ext i j,
+  rw [basis.to_matrix_apply, linear_map.to_matrix_apply]
+end
+
 lemma basis.det_reindex {ι' : Type*} [fintype ι'] [decidable_eq ι']
   (b : basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
   (b.reindex e).det v = b.det (v ∘ e) :=

src/linear_algebra/free_module/determinant.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2022 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Alex J. Best
+-/
+
+import linear_algebra.determinant
+import linear_algebra.free_module.finite.basic
+
+/-!
+# Determinants in free (finite) modules
+
+Quite a lot of our results on determinants (that you might know in vector spaces) will work for all
+free (finite) modules over any commutative ring.
+
+## Main results
+
+ * `linear_map.det_zero''`: The determinant of the constant zero map is zero, in a finite free
+   nontrivial module.
+-/
+
+@[simp] lemma linear_map.det_zero'' {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
+  [module.free R M] [module.finite R M] [nontrivial M] :
+  linear_map.det (0 : M →ₗ[R] M) = 0 :=
+begin
+  letI : nonempty (module.free.choose_basis_index R M) :=
+    (module.free.choose_basis R M).index_nonempty,
+  nontriviality R,
+  exact linear_map.det_zero' (module.free.choose_basis R M)
+end

src/linear_algebra/matrix/to_lin.lean

@@ -488,6 +488,14 @@ by { ext i,
      congr,
      exact v₁.equiv_fun.symm_apply_apply x }
 
+@[simp] lemma linear_map.to_matrix_basis_equiv [fintype l] [decidable_eq l]
+  (b : basis l R M₁) (b' : basis l R M₂) :
+  linear_map.to_matrix b' b (b'.equiv b (equiv.refl l) : M₂ →ₗ[R] M₁) = 1 :=
+begin
+  ext i j,
+  simp [linear_map.to_matrix_apply, matrix.one_apply, finsupp.single_apply, eq_comm],
+end
+
 lemma matrix.to_lin_mul [fintype l] [decidable_eq m] (A : matrix l m R) (B : matrix m n R) :
   matrix.to_lin v₁ v₃ (A ⬝ B) =
   (matrix.to_lin v₂ v₃ A).comp (matrix.to_lin v₁ v₂ B) :=

src/ring_theory/ideal/norm.lean

@@ -5,11 +5,13 @@ Authors: Anne Baanen, Alex J. Best
 -/
 
 import data.finsupp.fintype
+import data.int.absolute_value
+import data.int.associated
 import data.matrix.notation
 import data.zmod.quotient
-import linear_algebra.free_module.finite.basic
-import linear_algebra.free_module.pid
+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.norm
@@ -28,6 +30,15 @@ the quotient `R ⧸ I` (setting it to 0 if the cardinality is infinite).
  * `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.
 
+## Main results
+
+ * `map_mul ideal.abs_norm`: multiplicativity of the ideal norm is bundled in
+   the definition of `ideal.abs_norm`
+ * `ideal.nat_abs_det_basis_change`: the ideal norm is given by the determinant
+   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.
@@ -240,3 +251,160 @@ noncomputable def ideal.abs_norm [infinite S] [is_dedekind_domain S]
   map_mul' := λ I J, by rw card_quot_mul,
   map_one' := by rw [ideal.one_eq_top, card_quot_top],
   map_zero' := by rw [ideal.zero_eq_bot, card_quot_bot] }
+
+namespace ideal
+
+variables [infinite S] [is_dedekind_domain S] [module.free ℤ S] [module.finite ℤ S]
+
+lemma abs_norm_apply (I : ideal S) : abs_norm I = card_quot I := rfl
+
+@[simp] lemma abs_norm_bot : abs_norm (⊥ : ideal S) = 0 :=
+by rw [← ideal.zero_eq_bot, _root_.map_zero]
+
+@[simp] lemma abs_norm_top : abs_norm (⊤ : ideal S) = 1 :=
+by rw [← ideal.one_eq_top, _root_.map_one]
+
+@[simp] lemma abs_norm_eq_one_iff {I : ideal S} : abs_norm I = 1 ↔ I = ⊤ :=
+by rw [abs_norm_apply, card_quot_eq_one_iff]
+
+/-- Let `e : S ≃ I` be an additive isomorphism (therefore a `ℤ`-linear equiv).
+Then an alternative way to compute the norm of `I` is given by taking the determinant of `e`.
+See `nat_abs_det_basis_change` for a more familiar formulation of this result. -/
+theorem nat_abs_det_equiv (I : ideal S) {E : Type*} [add_equiv_class E S I] (e : E) :
+  int.nat_abs (linear_map.det
+      ((submodule.subtype I).restrict_scalars ℤ ∘ₗ add_monoid_hom.to_int_linear_map (e : S →+ I))) =
+  ideal.abs_norm I :=
+begin
+  -- `S ⧸ I` might be infinite if `I = ⊥`, but then `e` can't be an equiv.
+  by_cases hI : I = ⊥,
+  { unfreezingI { subst hI },
+    have : (1 : S) ≠ 0 := one_ne_zero,
+    have : (1 : S) = 0 := equiv_like.injective e (subsingleton.elim _ _),
+    contradiction },
+
+  let ι := module.free.choose_basis_index ℤ S,
+  let b := module.free.choose_basis ℤ S,
+  casesI is_empty_or_nonempty ι,
+  { nontriviality S,
+    exact (not_nontrivial_iff_subsingleton.mpr
+      (function.surjective.subsingleton b.repr.to_equiv.symm.surjective)
+      (by apply_instance)).elim },
+
+  -- Thus `(S ⧸ I)` is isomorphic to a product of `zmod`s, so it is a fintype.
+  letI := ideal.fintype_quotient_of_free_of_ne_bot I hI,
+  -- Use the Smith normal form to choose a nice basis for `I`.
+  letI := classical.dec_eq ι,
+  let a := I.smith_coeffs b hI,
+  let b' := I.ring_basis b hI,
+  let ab := I.self_basis b hI,
+  have ab_eq := I.self_basis_def b hI,
+  let e' : S ≃ₗ[ℤ] I := b'.equiv ab (equiv.refl _),
+  let f : S →ₗ[ℤ] S := (I.subtype.restrict_scalars ℤ).comp (e' : S →ₗ[ℤ] I),
+  let f_apply : ∀ x, f x = b'.equiv ab (equiv.refl _) x := λ x, rfl,
+  suffices : (linear_map.det f).nat_abs = ideal.abs_norm I,
+  { calc  (linear_map.det ((submodule.subtype I).restrict_scalars ℤ ∘ₗ _)).nat_abs
+        = (linear_map.det ((submodule.subtype I).restrict_scalars ℤ ∘ₗ
+            (↑(add_equiv.to_int_linear_equiv ↑e) : S →ₗ[ℤ] I))).nat_abs : rfl
+    ... = (linear_map.det ((submodule.subtype I).restrict_scalars ℤ ∘ₗ _)).nat_abs :
+      int.nat_abs_eq_iff_associated.mpr (linear_map.associated_det_comp_equiv _ _ _)
+    ... = abs_norm I : this },
+
+  have ha : ∀ i, f (b' i) = a i • b' i,
+  { intro i, rw [f_apply, b'.equiv_apply, equiv.refl_apply, ab_eq] },
+  have mem_I_iff : ∀ x, x ∈ I ↔ ∀ i, a i ∣ b'.repr x i,
+  { intro x, simp_rw [ab.mem_ideal_iff', ab_eq],
+    have : ∀ (c : ι → ℤ) i, b'.repr (∑ (j : ι), c j • a j • b' j) i = a i * c i,
+    { intros c i,
+      simp only [← mul_action.mul_smul, b'.repr_sum_self, mul_comm] },
+    split,
+    { rintro ⟨c, rfl⟩ i, exact ⟨c i, this c i⟩ },
+    { rintros ha,
+      choose c hc using ha, exact ⟨c, b'.ext_elem (λ i, trans (hc i) (this c i).symm)⟩ } },
+
+  -- `det f` is equal to `∏ i, a i`,
+  letI := classical.dec_eq ι,
+  calc  int.nat_abs (linear_map.det f)
+      = int.nat_abs (linear_map.to_matrix b' b' f).det : by rw linear_map.det_to_matrix
+  ... = int.nat_abs (matrix.diagonal a).det : _
+  ... = int.nat_abs (∏ i, a i) : by rw matrix.det_diagonal
+  ... = ∏ i, int.nat_abs (a i) : map_prod int.nat_abs_hom a finset.univ
+  ... = fintype.card (S ⧸ I) : _
+  ... = abs_norm I : (submodule.card_quot_apply _).symm,
+  -- since `linear_map.to_matrix b' b' f` is the diagonal matrix with `a` along the diagonal.
+  { congr, ext i j,
+    rw [linear_map.to_matrix_apply, ha, linear_equiv.map_smul, basis.repr_self, finsupp.smul_single,
+        smul_eq_mul, mul_one],
+    by_cases h : i = j,
+    { rw [h, matrix.diagonal_apply_eq, finsupp.single_eq_same] },
+    { rw [matrix.diagonal_apply_ne _ h, finsupp.single_eq_of_ne (ne.symm h)] } },
+
+  -- Now we map everything through the linear equiv `S ≃ₗ (ι → ℤ)`,
+  -- which maps `(S ⧸ I)` to `Π i, zmod (a i).nat_abs`.
+  haveI : ∀ i, ne_zero ((a i).nat_abs) := λ i,
+    ⟨int.nat_abs_ne_zero_of_ne_zero (ideal.smith_coeffs_ne_zero b I hI i)⟩,
+  simp_rw [fintype.card_eq.mpr ⟨(ideal.quotient_equiv_pi_zmod I b hI).to_equiv⟩, fintype.card_pi,
+           zmod.card] ,
+end
+
+/-- Let `b` be a basis for `S` over `ℤ` and `bI` a basis for `I` over `ℤ` of the same dimension.
+Then an alternative way to compute the norm of `I` is given by taking the determinant of `bI`
+over `b`. -/
+theorem nat_abs_det_basis_change {ι : Type*} [fintype ι] [decidable_eq ι]
+  (b : basis ι ℤ S) (I : ideal S) (bI : basis ι ℤ I) :
+  (b.det (coe ∘ bI)).nat_abs = ideal.abs_norm I :=
+begin
+  let e := b.equiv bI (equiv.refl _),
+  calc (b.det ((submodule.subtype I).restrict_scalars ℤ ∘ bI)).nat_abs
+      = (linear_map.det ((submodule.subtype I).restrict_scalars ℤ ∘ₗ (e : S →ₗ[ℤ] I))).nat_abs
+    : by rw basis.det_comp_basis
+  ... = _ : nat_abs_det_equiv I e
+end
+
+@[simp]
+lemma abs_norm_span_singleton (r : S) :
+  abs_norm (span ({r} : set S)) = (algebra.norm ℤ r).nat_abs :=
+begin
+  rw algebra.norm_apply,
+  by_cases hr : r = 0,
+  { simp only [hr, ideal.span_zero, algebra.coe_lmul_eq_mul, eq_self_iff_true, ideal.abs_norm_bot,
+      linear_map.det_zero'', set.singleton_zero, _root_.map_zero, int.nat_abs_zero] },
+  letI := ideal.fintype_quotient_of_free_of_ne_bot (span {r}) (mt span_singleton_eq_bot.mp hr),
+  let b := module.free.choose_basis ℤ S,
+  rw [← nat_abs_det_equiv _ (b.equiv (basis_span_singleton b hr) (equiv.refl _))],
+  swap, apply_instance,
+  congr,
+  refine b.ext (λ i, _),
+  simp
+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)
+
+@[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 :=
+(dvd_gcd_iff _ _ _).mpr
+  ⟨abs_norm_dvd_abs_norm_of_le (span_mono (set.subset_insert _ _)),
+  trans
+    (abs_norm_dvd_abs_norm_of_le (span_mono (set.singleton_subset_iff.mpr (set.mem_insert _ _))))
+    (by rw abs_norm_span_singleton)⟩
+
+lemma irreducible_of_irreducible_abs_norm {I : ideal S} (hI : irreducible I.abs_norm) :
+  irreducible I :=
+irreducible_iff.mpr
+  ⟨λ h, hI.not_unit (by simpa only [ideal.is_unit_iff, nat.is_unit_iff, abs_norm_eq_one_iff]
+      using h),
+   by rintro a b rfl; simpa only [ideal.is_unit_iff, nat.is_unit_iff, abs_norm_eq_one_iff]
+      using hI.is_unit_or_is_unit (_root_.map_mul abs_norm a b)⟩
+
+lemma is_prime_of_irreducible_abs_norm {I : ideal S} (hI : irreducible I.abs_norm) :
+  I.is_prime :=
+is_prime_of_prime (unique_factorization_monoid.irreducible_iff_prime.mp
+  (irreducible_of_irreducible_abs_norm hI))
+
+lemma prime_of_irreducible_abs_norm_span {a : S} (ha : a ≠ 0)
+  (hI : irreducible (ideal.span ({a} : set S)).abs_norm) :
+  prime a :=
+(ideal.span_singleton_prime ha).mp (is_prime_of_irreducible_abs_norm hI)
+
+end ideal

src/ring_theory/ideal/operations.lean

@@ -1536,6 +1536,35 @@ end
 
 end total
 
+section basis
+
+variables {ι R S : Type*} [comm_semiring R] [comm_ring S] [is_domain S] [algebra R S]
+
+/-- A basis on `S` gives a basis on `ideal.span {x}`, by multiplying everything by `x`. -/
+noncomputable def basis_span_singleton (b : basis ι R S) {x : S} (hx : x ≠ 0) :
+  basis ι R (span ({x} : set S)) :=
+b.map $ ((linear_equiv.of_injective (algebra.lmul R S x) (linear_map.mul_injective hx)) ≪≫ₗ
+  (linear_equiv.of_eq _ _ (by { ext, simp [mem_span_singleton', mul_comm] })) ≪≫ₗ
+  ((submodule.restrict_scalars_equiv R S S (ideal.span ({x} : set S))).restrict_scalars R))
+
+@[simp] lemma basis_span_singleton_apply (b : basis ι R S) {x : S} (hx : x ≠ 0) (i : ι) :
+  (basis_span_singleton b hx i : S) = x * b i :=
+begin
+  simp only [basis_span_singleton, basis.map_apply, linear_equiv.trans_apply,
+    submodule.restrict_scalars_equiv_apply, linear_equiv.of_injective_apply,
+    linear_equiv.coe_of_eq_apply, linear_equiv.restrict_scalars_apply,
+    algebra.coe_lmul_eq_mul, linear_map.mul_apply']
+end
+
+@[simp] lemma constr_basis_span_singleton
+  {N : Type*} [semiring N] [module N S] [smul_comm_class R N S]
+  (b : basis ι R S) {x : S} (hx : x ≠ 0) :
+  b.constr N (coe ∘ basis_span_singleton b hx) = algebra.lmul R S x :=
+b.ext (λ i, by erw [basis.constr_basis, function.comp_app, basis_span_singleton_apply,
+                   linear_map.mul_apply'])
+
+end basis
+
 end ideal
 
 lemma associates.mk_ne_zero' {R : Type*} [comm_semiring R] {r : R} :