[Merged by Bors] - feat(linear_algebra/free_module): lemmas on ideal quotient of a free module over a PID

src/linear_algebra/free_module/ideal_quotient.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2022 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import data.zmod.quotient
+import linear_algebra.free_module.finite.basic
+import linear_algebra.free_module.pid
+import linear_algebra.quotient_pi
+
+/-! # Ideals in free modules over PIDs
+
+## Main results
+
+ - `ideal.quotient_equiv_pi_span`: `S ⧸ I`, if `S` is finite free as a module over a PID `R`,
+   can be written as a product of quotients of `R` by principal ideals.
+
+-/
+
+open_locale big_operators
+
+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 ι]
+
+/-- 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
+  (I : ideal S) (b : basis ι R S) (hI : I ≠ ⊥) :
+  (S ⧸ I) ≃ₗ[R] Π i, (R ⧸ ideal.span ({I.smith_coeffs b hI i} : set R)) :=
+begin
+  -- 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`.
+  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 ≃ₗ[R] I := b'.equiv ab (equiv.refl _),
+  let f : S →ₗ[R] S := (I.subtype.restrict_scalars R).comp (e : S →ₗ[R] I),
+  let f_apply : ∀ x, f x = b'.equiv ab (equiv.refl _) x := λ x, rfl,
+  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 : ι → R) 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)⟩ } },
+
+  -- 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)),
+  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,
+               submodule.restrict_scalars_mem, mem_I_iff, smul_eq_mul, forall_true_left,
+               linear_equiv.coe_coe, basis.equiv_fun_apply],
+    split,
+    { rintros ⟨y, hy, rfl⟩ i, exact hy i },
+    { rintros hdvd,
+      refine ⟨∑ i, x i • b' i, λ i, _, _⟩; rwa b'.repr_sum_self,
+      { exact hdvd i } } },
+  refine ((submodule.quotient.restrict_scalars_equiv R I).restrict_scalars R).symm.trans _,
+  any_goals { apply ring_hom.id }, any_goals { apply_instance },
+  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)),
+  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
+  (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 :=
+  add_equiv.Pi_congr_right (λ i, ↑(int.quotient_span_equiv_zmod (a i)))
+in (↑(e : (S ⧸ I) ≃ₗ[ℤ] _) : (S ⧸ I ≃+ _)).trans e'
+
+/-- A nonzero ideal over a free finite extension of `ℤ` has a finite quotient.
+
+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]
+  (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)⟩);
+  exact fintype.of_equiv (Π i, zmod (a i).nat_abs) e.symm

src/linear_algebra/free_module/pid.lean

@@ -160,7 +160,7 @@ For `basis_of_pid` we only need the first half and can fix `M = ⊤`,
 for `smith_normal_form` we need the full statement,
 but must also feed in a basis for `M` using `basis_of_pid` to keep the induction going.
 -/
-lemma submodule.basis_of_pid_aux [fintype ι] {O : Type*} [add_comm_group O] [module R O]
+lemma submodule.basis_of_pid_aux [finite ι] {O : Type*} [add_comm_group O] [module R O]
   (M N : submodule R O) (b'M : basis ι R M) (N_bot : N ≠ ⊥) (N_le_M : N ≤ M) :
   ∃ (y ∈ M) (a : R) (hay : a • y ∈ N) (M' ≤ M) (N' ≤ N) (N'_le_M' : N' ≤ M')
     (y_ortho_M' : ∀ (c : R) (z : O), z ∈ M' → c • y + z = 0 → c = 0)
@@ -201,6 +201,7 @@ begin
   have hdvd : ∀ i, a ∣ b'M.coord i ⟨y, N_le_M yN⟩ :=
     λ i, generator_maximal_submodule_image_dvd N_le_M ϕ_max y yN ϕy_eq (b'M.coord i),
   choose c hc using hdvd,
+  casesI nonempty_fintype ι,
   let y' : O := ∑ i, c i • b'M i,
   have y'M : y' ∈ M := M.sum_mem (λ i _, M.smul_mem (c i) (b'M i).2),
   have mk_y' : (⟨y', y'M⟩ : M) = ∑ i, c i • b'M i :=
@@ -289,11 +290,12 @@ see `submodule.basis_of_pid`.
 
 See also the stronger version `submodule.smith_normal_form`.
 -/
-lemma submodule.nonempty_basis_of_pid {ι : Type*} [fintype ι]
+lemma submodule.nonempty_basis_of_pid {ι : Type*} [finite ι]
   (b : basis ι R M) (N : submodule R M) :
   ∃ (n : ℕ), nonempty (basis (fin n) R N) :=
 begin
   haveI := classical.dec_eq M,
+  casesI nonempty_fintype ι,
   refine N.induction_on_rank b _ _,
   intros N ih,
   let b' := (b.reindex (fintype.equiv_fin ι)).map (linear_equiv.of_top _ rfl).symm,
@@ -311,12 +313,12 @@ if `R` is a principal ideal domain.
 
 See also the stronger version `submodule.smith_normal_form`.
 -/
-noncomputable def submodule.basis_of_pid {ι : Type*} [fintype ι]
+noncomputable def submodule.basis_of_pid {ι : Type*} [finite ι]
   (b : basis ι R M) (N : submodule R M) :
   Σ (n : ℕ), (basis (fin n) R N) :=
 ⟨_, (N.nonempty_basis_of_pid b).some_spec.some⟩
 
-lemma submodule.basis_of_pid_bot {ι : Type*} [fintype ι] (b : basis ι R M) :
+lemma submodule.basis_of_pid_bot {ι : Type*} [finite ι] (b : basis ι R M) :
   submodule.basis_of_pid b ⊥ = ⟨0, basis.empty _⟩ :=
 begin
   obtain ⟨n, b'⟩ := submodule.basis_of_pid b ⊥,
@@ -330,7 +332,7 @@ if `R` is a principal ideal domain.
 
 See also the stronger version `submodule.smith_normal_form_of_le`.
 -/
-noncomputable def submodule.basis_of_pid_of_le {ι : Type*} [fintype ι]
+noncomputable def submodule.basis_of_pid_of_le {ι : Type*} [finite ι]
   {N O : submodule R M} (hNO : N ≤ O) (b : basis ι R O) :
   Σ (n : ℕ), basis (fin n) R N :=
 let ⟨n, bN'⟩ := submodule.basis_of_pid b (N.comap O.subtype)
@@ -339,7 +341,7 @@ in ⟨n, bN'.map (submodule.comap_subtype_equiv_of_le hNO)⟩
 /-- A submodule inside the span of a linear independent family is a free `R`-module of finite rank,
 if `R` is a principal ideal domain. -/
 noncomputable def submodule.basis_of_pid_of_le_span
-  {ι : Type*} [fintype ι] {b : ι → M} (hb : linear_independent R b)
+  {ι : Type*} [finite ι] {b : ι → M} (hb : linear_independent R b)
   {N : submodule R M} (le : N ≤ submodule.span R (set.range b)) :
   Σ (n : ℕ), basis (fin n) R N :=
 submodule.basis_of_pid_of_le le (basis.span hb)
@@ -422,11 +424,12 @@ a `basis.smith_normal_form`.
 
 This is a strengthening of `submodule.basis_of_pid_of_le`.
 -/
-theorem submodule.exists_smith_normal_form_of_le [fintype ι]
+theorem submodule.exists_smith_normal_form_of_le [finite ι]
   (b : basis ι R M) (N O : submodule R M) (N_le_O : N ≤ O) :
   ∃ (n o : ℕ) (hno : n ≤ o) (bO : basis (fin o) R O) (bN : basis (fin n) R N) (a : fin n → R),
     ∀ i, (bN i : M) = a i • bO (fin.cast_le hno i) :=
 begin
+  casesI nonempty_fintype ι,
   revert N,
   refine induction_on_rank b _ _ O,
   intros M ih N N_le_M,
@@ -453,7 +456,7 @@ need to map `N` into a submodule of `O`.
 
 This is a strengthening of `submodule.basis_of_pid_of_le`.
 -/
-noncomputable def submodule.smith_normal_form_of_le [fintype ι]
+noncomputable def submodule.smith_normal_form_of_le [finite ι]
   (b : basis ι R M) (N O : submodule R M) (N_le_O : N ≤ O) :
   Σ (o n : ℕ), basis.smith_normal_form (N.comap O.subtype) (fin o) n :=
 begin
@@ -474,7 +477,7 @@ This is a strengthening of `submodule.basis_of_pid`.
 See also `ideal.smith_normal_form`, which moreover proves that the dimension of
 an ideal is the same as the dimension of the whole ring.
 -/
-noncomputable def submodule.smith_normal_form [fintype ι] (b : basis ι R M) (N : submodule R M) :
+noncomputable def submodule.smith_normal_form [finite ι] (b : basis ι R M) (N : submodule R M) :
   Σ (n : ℕ), basis.smith_normal_form N ι n :=
 let ⟨m, n, bM, bN, f, a, snf⟩ := N.smith_normal_form_of_le b ⊤ le_top,
     bM' := bM.map (linear_equiv.of_top _ rfl),
@@ -485,6 +488,10 @@ let ⟨m, n, bM, bN, f, a, snf⟩ := N.smith_normal_form_of_le b ⊤ le_top,
                     equiv.to_embedding_apply, function.embedding.trans_apply,
                     equiv.symm_apply_apply]⟩
 
+section ideal
+
+variables {S : Type*} [comm_ring S] [is_domain S] [algebra R S]
+
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
@@ -496,25 +503,28 @@ need to map `I` into a submodule of `R`.
 This is a strengthening of `submodule.basis_of_pid`.
 -/
 noncomputable def ideal.smith_normal_form
-  [fintype ι] {S : Type*} [comm_ring S] [is_domain S] [algebra R S]
-  (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) :
+  [fintype ι] (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) :
   basis.smith_normal_form (I.restrict_scalars R) ι (fintype.card ι) :=
 let ⟨n, bS, bI, f, a, snf⟩ := (I.restrict_scalars R).smith_normal_form b in
 have eq : _ := ideal.rank_eq bS hI (bI.map ((restrict_scalars_equiv R S S I).restrict_scalars _)),
 let e : fin n ≃ fin (fintype.card ι) := fintype.equiv_of_card_eq (by rw [eq, fintype.card_fin]) in
 ⟨bS, bI.reindex e, e.symm.to_embedding.trans f, a ∘ e.symm, λ i,
   by simp only [snf, basis.coe_reindex, function.embedding.trans_apply, equiv.to_embedding_apply]⟩
 
+variables [finite ι]
+
 /-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
 then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
 find a basis for `S` and `I` such that the inclusion map is a square diagonal
 matrix.
 
 See also `ideal.smith_normal_form` for a version of this theorem that returns
 a `basis.smith_normal_form`.
+
+The definitions `ideal.ring_basis`, `ideal.self_basis`, `ideal.smith_coeffs` are (noncomputable)
+choices of values for this existential quantifier.
 -/
 theorem ideal.exists_smith_normal_form
-  [finite ι] {S : Type*} [comm_ring S] [is_domain S] [algebra R S]
   (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) :
   ∃ (b' : basis ι R S) (a : ι → R) (ab' : basis ι R I),
   ∀ i, (ab' i : S) = a i • b' i :=
@@ -526,6 +536,61 @@ have fe : ∀ i, f (e.symm i) = i := e.apply_symm_apply,
   by simp only [snf, fe, basis.map_apply, linear_equiv.restrict_scalars_apply,
     submodule.restrict_scalars_equiv_apply, basis.coe_reindex]⟩
 
+/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
+then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
+find a basis for `S` and `I` such that the inclusion map is a square diagonal
+matrix; this is the basis for `S`.
+See `ideal.self_basis` for the basis on `I`,
+see `ideal.smith_coeffs` for the entries of the diagonal matrix
+and `ideal.self_basis_def` for the proof that the inclusion map forms a square diagonal matrix.
+-/
+noncomputable def ideal.ring_basis (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) : basis ι R S :=
+(ideal.exists_smith_normal_form b I hI).some
+
+/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
+then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
+find a basis for `S` and `I` such that the inclusion map is a square diagonal
+matrix; this is the basis for `I`.
+See `ideal.ring_basis` for the basis on `S`,
+see `ideal.smith_coeffs` for the entries of the diagonal matrix
+and `ideal.self_basis_def` for the proof that the inclusion map forms a square diagonal matrix.
+-/
+noncomputable def ideal.self_basis (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) : basis ι R I :=
+(ideal.exists_smith_normal_form b I hI).some_spec.some_spec.some
+
+/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
+then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
+find a basis for `S` and `I` such that the inclusion map is a square diagonal
+matrix; these are the entries of the diagonal matrix.
+See `ideal.ring_basis` for the basis on `S`,
+see `ideal.self_basis` for the basis on `I`,
+and `ideal.self_basis_def` for the proof that the inclusion map forms a square diagonal matrix.
+-/
+noncomputable def ideal.smith_coeffs (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) : ι → R :=
+(ideal.exists_smith_normal_form b I hI).some_spec.some
+
+/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
+then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
+find a basis for `S` and `I` such that the inclusion map is a square diagonal
+matrix.
+-/
+@[simp]
+lemma ideal.self_basis_def (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) :
+  ∀ i, (ideal.self_basis b I hI i : S) = ideal.smith_coeffs b I hI i • ideal.ring_basis b I hI i :=
+(ideal.exists_smith_normal_form b I hI).some_spec.some_spec.some_spec
+
+@[simp]
+lemma ideal.smith_coeffs_ne_zero (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) (i) :
+  ideal.smith_coeffs b I hI i ≠ 0 :=
+begin
+  intro hi,
+  apply basis.ne_zero (ideal.self_basis b I hI) i,
+  refine subtype.coe_injective _,
+  simp [hi]
+end
+
+end ideal
+
 end smith_normal
 
 end principal_ideal_domain