Lean4
/-- The induction hypothesis of `Submodule.basisOfPid` and `Submodule.smithNormalForm`.
Basically, it says: let `N ≤ M` be a pair of submodules, then we can find a pair of
submodules `N' ≤ M'` of strictly smaller rank, whose basis we can extend to get a basis
of `N` and `M`. Moreover, if the basis for `M'` is up to scalars a basis for `N'`,
then the basis we find for `M` is up to scalars a basis for `N`.
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.
-/
theorem basis_of_pid_aux [Finite ι] {O : Type*} [AddCommGroup 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,
a • y ∈ N ∧
∃ M' ≤ M,
∃ N' ≤ N,
N' ≤ M' ∧
(∀ (c : R) (z : O), z ∈ M' → c • y + z = 0 → c = 0) ∧
(∀ (c : R) (z : O), z ∈ N' → c • a • y + z = 0 → c = 0) ∧
∀ (n') (bN' : Basis (Fin n') R N'),
∃ bN : Basis (Fin (n' + 1)) R N,
∀ (m') (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R M'),
∃ (hnm : n' + 1 ≤ m' + 1) (bM : Basis (Fin (m' + 1)) R M),
∀ as : Fin n' → R,
(∀ i : Fin n', (bN' i : O) = as i • (bM' (Fin.castLE hn'm' i) : O)) →
∃ as' : Fin (n' + 1) → R,
∀ i : Fin (n' + 1), (bN i : O) = as' i • (bM (Fin.castLE hnm i) : O) :=
by
-- Let `ϕ` be a maximal projection of `M` onto `R`, in the sense that there is
-- no `ψ` whose image of `N` is larger than `ϕ`'s image of `N`.
have : ∃ ϕ : M →ₗ[R] R, ∀ ψ : M →ₗ[R] R, ¬ϕ.submoduleImage N < ψ.submoduleImage N :=
by
obtain ⟨P, P_eq, P_max⟩ :=
set_has_maximal_iff_noetherian.mpr (inferInstance : IsNoetherian R R) _
(show (Set.range fun ψ : M →ₗ[R] R ↦ ψ.submoduleImage N).Nonempty from ⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩)
obtain ⟨ϕ, rfl⟩ := Set.mem_range.mp P_eq
exact ⟨ϕ, fun ψ hψ ↦ P_max _ ⟨_, rfl⟩ hψ⟩
let ϕ := this.choose
have ϕ_max := this.choose_spec
let a := generator (ϕ.submoduleImage N)
have a_mem : a ∈ ϕ.submoduleImage N :=
generator_mem
_
-- If `a` is zero, then the submodule is trivial. So let's assume `a ≠ 0`, `N ≠ ⊥`.
by_cases a_zero : a = 0
· have := eq_bot_of_generator_maximal_submoduleImage_eq_zero b'M N_le_M ϕ_max a_zero
contradiction
-- We claim that `ϕ⁻¹ a = y` can be taken as basis element of `N`.
obtain ⟨y, yN, ϕy_eq⟩ := (LinearMap.mem_submoduleImage_of_le N_le_M).mp a_mem
have hdvd : ∀ i, a ∣ b'M.coord i ⟨y, N_le_M yN⟩ := fun i ↦
generator_maximal_submoduleImage_dvd N_le_M ϕ_max y yN ϕy_eq (b'M.coord i)
choose c hc using hdvd
cases nonempty_fintype ι
let y' : O := ∑ i, c i • b'M i
have y'M : y' ∈ M := M.sum_mem fun i _ ↦ M.smul_mem (c i) (b'M i).2
have mk_y' : (⟨y', y'M⟩ : M) = ∑ i, c i • b'M i :=
Subtype.ext
(show y' = M.subtype _ by
simp only [map_sum, map_smul]
rfl)
have a_smul_y' : a • y' = y :=
by
refine Subtype.mk_eq_mk.mp (show (a • ⟨y', y'M⟩ : M) = ⟨y, N_le_M yN⟩ from ?_)
rw [← b'M.sum_repr ⟨y, N_le_M yN⟩, mk_y', Finset.smul_sum]
refine Finset.sum_congr rfl fun i _ ↦ ?_
rw [← mul_smul, ← hc]
rfl
-- We found a `y` and an `a`!
refine ⟨y', y'M, a, a_smul_y'.symm ▸ yN, ?_⟩
have ϕy'_eq : ϕ ⟨y', y'M⟩ = 1 :=
mul_left_cancel₀ a_zero
(calc
a • ϕ ⟨y', y'M⟩ = ϕ ⟨a • y', _⟩ := (ϕ.map_smul a ⟨y', y'M⟩).symm
_ = ϕ ⟨y, N_le_M yN⟩ := by simp only [a_smul_y']
_ = a := ϕy_eq
_ = a * 1 := (mul_one a).symm)
have ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0 := by simpa only [ϕy'_eq] using one_ne_zero
let M' : Submodule R O := (LinearMap.ker ϕ).map M.subtype
let N' : Submodule R O := (LinearMap.ker (ϕ.comp (inclusion N_le_M))).map N.subtype
have M'_le_M : M' ≤ M := M.map_subtype_le (LinearMap.ker ϕ)
have N'_le_M' : N' ≤ M' := by
intro x hx
simp only [N', mem_map, LinearMap.mem_ker] at hx ⊢
obtain ⟨⟨x, xN⟩, hx, rfl⟩ := hx
exact ⟨⟨x, N_le_M xN⟩, hx, rfl⟩
have N'_le_N : N' ≤ N :=
N.map_subtype_le
(LinearMap.ker (ϕ.comp (inclusion N_le_M)))
-- So fill in those results as well.
refine
⟨M', M'_le_M, N', N'_le_N, N'_le_M', ?_⟩
-- Note that `y'` is orthogonal to `M'`.
have y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0 :=
by
intro c x xM' hc
obtain ⟨⟨x, xM⟩, hx', rfl⟩ := Submodule.mem_map.mp xM'
rw [LinearMap.mem_ker] at hx'
have hc' : (c • ⟨y', y'M⟩ + ⟨x, xM⟩ : M) = 0 := by exact @Subtype.coe_injective O (· ∈ M) _ _ hc
simpa only [LinearMap.map_add, LinearMap.map_zero, LinearMap.map_smul, smul_eq_mul, add_zero, mul_eq_zero,
ϕy'_ne_zero, hx', or_false] using congr_arg ϕ hc'
have ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0 :=
by
intro c z zN' hc
refine (mul_eq_zero.mp (y'_ortho_M' (a * c) z (N'_le_M' zN') ?_)).resolve_left a_zero
rw [mul_comm, mul_smul, hc]
-- So we can extend a basis for `N'` with `y`
refine ⟨y'_ortho_M', ay'_ortho_N', fun n' bN' ↦ ⟨?_, ?_⟩⟩
· refine Basis.mkFinConsOfLE y yN bN' N'_le_N ?_ ?_
· intro c z zN' hc
refine ay'_ortho_N' c z zN' ?_
rwa [← a_smul_y'] at hc
· intro z zN
obtain ⟨b, hb⟩ : _ ∣ ϕ ⟨z, N_le_M zN⟩ := generator_submoduleImage_dvd_of_mem N_le_M ϕ zN
refine ⟨-b, Submodule.mem_map.mpr ⟨⟨_, N.sub_mem zN (N.smul_mem b yN)⟩, ?_, ?_⟩⟩
· refine LinearMap.mem_ker.mpr (show ϕ (⟨z, N_le_M zN⟩ - b • ⟨y, N_le_M yN⟩) = 0 from ?_)
rw [LinearMap.map_sub, LinearMap.map_smul, hb, ϕy_eq, smul_eq_mul, mul_comm, sub_self]
·
simp only [sub_eq_add_neg, neg_smul, coe_subtype]
-- And extend a basis for `M'` with `y'`
intro m' hn'm' bM'
refine ⟨Nat.succ_le_succ hn'm', ?_, ?_⟩
· refine Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ?_
intro z zM
refine ⟨-ϕ ⟨z, zM⟩, ⟨⟨z, zM⟩ - ϕ ⟨z, zM⟩ • ⟨y', y'M⟩, LinearMap.mem_ker.mpr ?_, ?_⟩⟩
· rw [LinearMap.map_sub, LinearMap.map_smul, ϕy'_eq, smul_eq_mul, mul_one, sub_self]
· rw [LinearMap.map_sub, LinearMap.map_smul, sub_eq_add_neg, neg_smul]
rfl
-- It remains to show the extended bases are compatible with each other.
intro as h
refine ⟨Fin.cons a as, ?_⟩
intro i
rw [Basis.coe_mkFinConsOfLE, Basis.coe_mkFinConsOfLE]
refine Fin.cases ?_ (fun i ↦ ?_) i
· simp only [Fin.cons_zero, Fin.castLE_zero]
exact a_smul_y'.symm
· rw [Fin.castLE_succ]
simp only [Fin.cons_succ, Function.comp_apply, coe_inclusion, h i]
