feat(linear_algebra/free_module/ideal_quotient): prove dimension of quotient by ideal equals degree of norm of generator (#19121)

Multramate · alreadydone · Multramate · commit 90b0d53ee6ff · 2023-06-10T18:56:02.000Z
Also refactor file into `namespace ideal`.



Co-authored-by: Junyan Xu &lt;junyanxu.math@gmail.com&gt;
diff --git a/src/linear_algebra/free_module/ideal_quotient.lean b/src/linear_algebra/free_module/ideal_quotient.lean
@@ -22,17 +22,20 @@ import linear_algebra.quotient_pi
 
 -/
 
-open_locale big_operators direct_sum
+namespace ideal
 
-variables {ι R S : Type*} [comm_ring R] [comm_ring S] [algebra R S]
-variables [is_domain R] [is_principal_ideal_ring R] [is_domain S] [fintype ι]
+open_locale big_operators direct_sum polynomial
+
+variables {R S ι : Type*} [comm_ring R] [comm_ring S] [algebra R S]
+variables [is_domain R] [is_principal_ideal_ring R] [is_domain S] [finite ι]
 
 /-- We can write the quotient of an ideal over a PID as a product of quotients by principal ideals.
 -/
-noncomputable def ideal.quotient_equiv_pi_span
+noncomputable def quotient_equiv_pi_span
   (I : ideal S) (b : basis ι R S) (hI : I ≠ ⊥) :
-  (S ⧸ I) ≃ₗ[R] Π i, (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R)) :=
+  (S ⧸ I) ≃ₗ[R] Π i, (R ⧸ span ({I.smith_coeffs b hI i} : set R)) :=
 begin
+  haveI := fintype.of_finite ι,
   -- Choose `e : S ≃ₗ I` and a basis `b'` for `S` that turns the map
   -- `f := ((submodule.subtype I).restrict_scalars R).comp e` into a diagonal matrix:
   -- there is an `a : ι → ℤ` such that `f (b' i) = a i • b' i`.
@@ -57,10 +60,10 @@ begin
 
   -- Now we map everything through the linear equiv `S ≃ₗ (ι → R)`,
   -- which maps `I` to `I' := Π i, a i ℤ`.
-  let I' : submodule R (ι → R) := submodule.pi set.univ (λ i, ideal.span ({a i} : set R)),
+  let I' : submodule R (ι → R) := submodule.pi set.univ (λ i, span ({a i} : set R)),
   have : submodule.map (b'.equiv_fun : S →ₗ[R] (ι → R)) (I.restrict_scalars R) = I',
   { ext x,
-    simp only [submodule.mem_map, submodule.mem_pi, ideal.mem_span_singleton, set.mem_univ,
+    simp only [submodule.mem_map, submodule.mem_pi, mem_span_singleton, set.mem_univ,
                submodule.restrict_scalars_mem, mem_I_iff, smul_eq_mul, forall_true_left,
                linear_equiv.coe_coe, basis.equiv_fun_apply],
     split,
@@ -73,18 +76,18 @@ begin
   refine (submodule.quotient.equiv (I.restrict_scalars R) I' b'.equiv_fun this).trans _,
   any_goals { apply ring_hom.id }, any_goals { apply_instance },
   classical,
-  let := submodule.quotient_pi (show Π i, submodule R R, from λ i, ideal.span ({a i} : set R)),
+  let := submodule.quotient_pi (show Π i, submodule R R, from λ i, span ({a i} : set R)),
   exact this
 end
 
 /-- Ideal quotients over a free finite extension of `ℤ` are isomorphic to a direct product of
 `zmod`. -/
-noncomputable def ideal.quotient_equiv_pi_zmod
+noncomputable def quotient_equiv_pi_zmod
   (I : ideal S) (b : basis ι ℤ S) (hI : I ≠ ⊥) :
   (S ⧸ I) ≃+ Π i, (zmod (I.smith_coeffs b hI i).nat_abs) :=
 let a := I.smith_coeffs b hI,
     e := I.quotient_equiv_pi_span b hI,
-    e' : (Π (i : ι), (ℤ ⧸ ideal.span ({a i} : set ℤ))) ≃+ Π (i : ι), zmod (a i).nat_abs :=
+    e' : (Π (i : ι), (ℤ ⧸ span ({a i} : set ℤ))) ≃+ Π (i : ι), zmod (a i).nat_abs :=
   add_equiv.Pi_congr_right (λ i, ↑(int.quotient_span_equiv_zmod (a i)))
 in (↑(e : (S ⧸ I) ≃ₗ[ℤ] _) : (S ⧸ I ≃+ _)).trans e'
 
@@ -93,38 +96,41 @@ in (↑(e : (S ⧸ I) ≃ₗ[ℤ] _) : (S ⧸ I ≃+ _)).trans e'
 Can't be an instance because of the side condition `I ≠ ⊥`, and more importantly,
 because the choice of `fintype` instance is non-canonical.
 -/
-noncomputable def ideal.fintype_quotient_of_free_of_ne_bot [module.free ℤ S] [module.finite ℤ S]
+noncomputable def fintype_quotient_of_free_of_ne_bot [module.free ℤ S] [module.finite ℤ S]
   (I : ideal S) (hI : I ≠ ⊥) :
   fintype (S ⧸ I) :=
 let b := module.free.choose_basis ℤ S,
     a := I.smith_coeffs b hI,
     e := I.quotient_equiv_pi_zmod b hI
 in by 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)⟩); classical;
+    (λ i, ⟨int.nat_abs_ne_zero_of_ne_zero (smith_coeffs_ne_zero b I hI i)⟩); classical;
   exact fintype.of_equiv (Π i, zmod (a i).nat_abs) e.symm
 
 variables (F : Type*) [comm_ring F] [algebra F R] [algebra F S] [is_scalar_tower F R S]
   (b : basis ι R S) {I : ideal S} (hI : I ≠ ⊥)
 
 /-- Decompose `S⧸I` as a direct sum of cyclic `R`-modules
   (quotients by the ideals generated by Smith coefficients of `I`). -/
-noncomputable def ideal.quotient_equiv_direct_sum :
-  (S ⧸ I) ≃ₗ[F] ⨁ i, R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R) :=
+noncomputable def quotient_equiv_direct_sum :
+  (S ⧸ I) ≃ₗ[F] ⨁ i, R ⧸ span ({I.smith_coeffs b hI i} : set R) :=
 begin
+  haveI := fintype.of_finite ι,
   apply ((I.quotient_equiv_pi_span b _).restrict_scalars F).trans
     (direct_sum.linear_equiv_fun_on_fintype _ _ _).symm,
   exact linear_map.is_scalar_tower.compatible_smul
   -- why doesn't it automatically apply?
   -- even after `change linear_map.compatible_smul _ (Π i, R ⧸ span _) F R`
 end
 
-lemma ideal.finrank_quotient_eq_sum [nontrivial F]
-  [∀ i, module.free F (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R))]
-  [∀ i, module.finite F (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R))] :
+lemma finrank_quotient_eq_sum {ι} [fintype ι] (b : basis ι R S) [nontrivial F]
+  [∀ i, module.free F (R ⧸ span ({I.smith_coeffs b hI i} : set R))]
+  [∀ i, module.finite F (R ⧸ span ({I.smith_coeffs b hI i} : set R))] :
   finite_dimensional.finrank F (S ⧸ I)
-    = ∑ i, finite_dimensional.finrank F (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R)) :=
+    = ∑ i, finite_dimensional.finrank F (R ⧸ span ({I.smith_coeffs b hI i} : set R)) :=
 begin
-  rw [linear_equiv.finrank_eq $ ideal.quotient_equiv_direct_sum F b hI,
+  rw [linear_equiv.finrank_eq $ quotient_equiv_direct_sum F b hI,
       finite_dimensional.finrank_direct_sum]
   -- slow, and dot notation doesn't work
 end
+
+end ideal
diff --git a/src/linear_algebra/free_module/norm.lean b/src/linear_algebra/free_module/norm.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2023 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+
+import linear_algebra.free_module.ideal_quotient
+import ring_theory.norm
+
+/-!
+# Norms on free modules over principal ideal domains
+-/
+
+open ideal polynomial
+
+open_locale big_operators polynomial
+
+variables {R S ι : Type*} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] [comm_ring S]
+  [is_domain S] [algebra R S]
+
+section comm_ring
+
+variables (F : Type*) [comm_ring F] [algebra F R] [algebra F S] [is_scalar_tower F R S]
+
+/-- For a nonzero element `f` in an algebra `S` over a principal ideal domain `R` that is finite and
+free as an `R`-module, the norm of `f` relative to `R` is associated to the product of the Smith
+coefficients of the ideal generated by `f`. -/
+lemma associated_norm_prod_smith [fintype ι] (b : basis ι R S) {f : S} (hf : f ≠ 0) :
+  associated (algebra.norm R f) (∏ i, smith_coeffs b _ (span_singleton_eq_bot.not.2 hf) i) :=
+begin
+  have hI := span_singleton_eq_bot.not.2 hf,
+  let b' := ring_basis b (span {f}) hI,
+  classical,
+  rw [← matrix.det_diagonal, ← linear_map.det_to_lin b'],
+  let e := (b'.equiv ((span {f}).self_basis b hI) $ equiv.refl _).trans
+    ((linear_equiv.coord S S f hf).restrict_scalars R),
+  refine (linear_map.associated_det_of_eq_comp e _ _ _).symm,
+  dsimp only [e, linear_equiv.trans_apply],
+  simp_rw [← linear_equiv.coe_to_linear_map, ← linear_map.comp_apply, ← linear_map.ext_iff],
+  refine b'.ext (λ i, _),
+  simp_rw [linear_map.comp_apply, linear_equiv.coe_to_linear_map, matrix.to_lin_apply,
+    basis.repr_self, finsupp.single_eq_pi_single, matrix.diagonal_mul_vec_single, pi.single_apply,
+    ite_smul, zero_smul, finset.sum_ite_eq', mul_one, if_pos (finset.mem_univ _), b'.equiv_apply],
+  change _ = f * _,
+  rw [mul_comm, ← smul_eq_mul, linear_equiv.restrict_scalars_apply, linear_equiv.coord_apply_smul,
+    ideal.self_basis_def],
+  refl
+end
+
+end comm_ring
+
+section field
+
+variables {F : Type*} [field F] [algebra F[X] S] [finite ι]
+
+instance (b : basis ι F[X] S) {I : ideal S} (hI : I ≠ ⊥) (i : ι) :
+  finite_dimensional F (F[X] ⧸ span ({I.smith_coeffs b hI i} : set F[X])) :=
+(adjoin_root.power_basis $ I.smith_coeffs_ne_zero b hI i).finite_dimensional
+
+/-- For a nonzero element `f` in a `F[X]`-module `S`, the dimension of $S/\langle f \rangle$ as an
+`F`-vector space is the degree of the norm of `f` relative to `F[X]`. -/
+lemma finrank_quotient_span_eq_nat_degree_norm [algebra F S] [is_scalar_tower F F[X] S]
+  (b : basis ι F[X] S) {f : S} (hf : f ≠ 0) :
+  finite_dimensional.finrank F (S ⧸ span ({f} : set S)) = (algebra.norm F[X] f).nat_degree :=
+begin
+  haveI := fintype.of_finite ι,
+  have h := span_singleton_eq_bot.not.2 hf,
+  rw [nat_degree_eq_of_degree_eq (degree_eq_degree_of_associated $ associated_norm_prod_smith b hf),
+      nat_degree_prod _ _ (λ i _, smith_coeffs_ne_zero b _ h i), finrank_quotient_eq_sum F h b],
+  -- finrank_quotient_eq_sum slow
+  congr' with i,
+  exact (adjoin_root.power_basis $ smith_coeffs_ne_zero b _ h i).finrank
+end
+
+end field
