!4#3434

Stream: mathlib4

[Xavier Roblot]

I am having some troubles with Submodule.inductionOnRank in this file. To prove Submodule.nonempty_basis_of_pid

theorem Submodule.nonempty_basis_of_pid {ι : Type _} [Finite ι] (b : Basis ι R M)
    (N : Submodule R M) : ∃ n : ℕ, Nonempty (Basis (Fin n) R N

where the goal is

∃ n, Nonempty (Basis (Fin n) R { x // x ∈ N })

I need to write explicitly the induction hypothesis:

refine inductionOnRank b (fun N ↦ ∃ n : ℕ, Nonempty (Basis (Fin n) R N)) ?_ N

to be able to use inductionOnRank. (It was simply refine N.induction_on_rank b _ _ with Lean 3). Still, this works and the proof completes.

But, for the proof of Submodule.exists_smith_normal_form_of_le

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.castLE hno i)

the goal is

∀ (N : Submodule R M),  N ≤ O → ∃ n o hno bO bN a, ∀ (i : Fin n), ↑(↑bN i) = ↑(a i • ↑bO (↑(Fin.castLE hno).toEmbedding i))

and I cannot make Submodule.inductionOnRank work. Even if I do something like

let P : Submodule R M → Prop := fun O => ∀ N : Submodule R M, 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.castLE hno i)
refine inductionOnRank b P ?_ O

to specify the induction hypothesis, it does not work and gives me the new goal:

 ∀ (N : Submodule R M),
  (∀ (N' : Submodule R M), N' ≤ N → ∀ (x : M), x ∈ N → (∀ (c : R) (y : M), y ∈ N' → c • x + y = 0 → c = 0) → P N') → P N

[Eric Wieser]

Does induction N using Submodule.inductionOnRank work?

[Xavier Roblot]

It does work but I need also to specify the basis b somehow and I don't know how to do that. How can I provide the arguments to Submodule.inductionOnRank?

[Eric Wieser]

docs4#Submodule.inductionOnRank / docs#submodule.induction_on_rank

[Eric Wieser]

The lemma is stupid, it should take module.free instead

[Eric Wieser]

Ah, it's a def not a lemma!