How to write induction principle for modules

Stream: mathlib4

[Jz Pan]

Suppose I proved this result:

If A is a Noetherian ring and M is a finitely generated A-module, then there exists
a chain of submodules 0 = M₀ ≤ M₁ ≤ M₂ ≤ ... ≤ Mₙ = M of M, such that for each 0 ≤ i < n,
Mᵢ / Mᵢ₋₁ is isomorphic to A / pᵢ for some prime ideal pᵢ of A.

It gives the following induction principle: let P be a property for A-modules, such that

• it holds for zero module (it's formalized as it holds for any module which is subsingleton)
• it holds for A / p for every prime ideal p of A (to avoid universe problem, it's formalized as it holds for any module isomorphic to A / p)
• it is stable by short exact sequences

Then P holds for M if A is Noetherian and M is finitely generated.

I have the formalization of it:

import Mathlib

@[elab_as_elim]
theorem IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (M : Type v) [AddCommGroup M] [Module A M] [Module.Finite A M]
    {P : (N : Type v) → [AddCommGroup N] → [Module A N] → Prop}
    (h_subsingleton : (N : Type v) → [AddCommGroup N] → [Module A N] →
      [Subsingleton N] → P N)
    (h_quotient : (N : Type v) → [AddCommGroup N] → [Module A N] →
      (p : PrimeSpectrum A) → (N ≃ₗ[A] A ⧸ p.1) → P N)
    (h_exact : (N₁ : Type v) → [AddCommGroup N₁] → [Module A N₁] →
      (N₂ : Type v) → [AddCommGroup N₂] → [Module A N₂] →
      (N₃ : Type v) → [AddCommGroup N₃] → [Module A N₃] →
      (f : N₁ →ₗ[A] N₂) → (g : N₂ →ₗ[A] N₃) →
      Function.Injective f → Function.Surjective g → Function.Exact f g →
      P N₁ → P N₃ → P N₂) : P M := by
  sorry -- proof omitted

My question is, how to make it work with induction tactics? For example, this result implies

/-- There are only finitely many associated primes of a finitely generated module
over a Noetherian ring. -/
theorem associatedPrimes.finite
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (M : Type v) [AddCommGroup M] [Module A M] [Module.Finite A M] :
    (associatedPrimes A M).Finite := by
  induction M using IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A -- doesn't work
  · sorry
  · sorry
  · sorry

But the induction tactic doesn't work. The refine works but I need to explicitly provide P.

How do I rewrite the induction principle to make induction works?

[Edward van de Meent]

Did you forget to add the @[induction_eliminator] attribute? oh nvm, that's not what this question is about

[Edward van de Meent]

i think the issue may be that you're basically writing an induction principle for Type, and so lean has a hard time figuring out which argument is which?

[Edward van de Meent]

nope, not it either

[Edward van de Meent]

ok, I think what basically happens is that lean just doesn't really do instance arguments to induction?

[Edward van de Meent]

lean is complaining "i have no clue how to find [CommRing A]" because there is no explicit argument after it whose unification specifies it. For induction principles, as far as i can tell, lean only does unification, no instance synthesis

[Edward van de Meent]

this is a result of how Lean.Meta.addImplicitTargets is implemented

[Edward van de Meent]

in the short term, i think you can change the module A M argument to explicit and supply the instance to induction, and that should work. In the long term, i think we can make a lean issue for this?

[Jz Pan]

Edward van de Meent said:

in the short term, i think you can change the module A M argument to explicit and supply the instance to induction, and that should work. In the long term, i think we can make a lean issue for this?

Let me try if it works. But it sound extremely weird. Even if it works, I think I still prefer to instance variable version and use refine instead.

[Edward van de Meent]

well... in a sense, you really are doing induction on the module structure, so writing something like induction ‹Module A M› is not completely nonsensical

[Edward van de Meent]

to make that work, you need to make M a lazy implicit argument and the Module A M argument explicit

[Edward van de Meent]

Like So

import Mathlib

@[elab_as_elim]
theorem IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime
    (A : Type u) [ha1:CommRing A] [ha2: IsNoetherianRing A]
    ⦃M : Type v⦄ [AddCommGroup M] (_:Module A M)
    {P : (N : Type v) → [AddCommGroup N] → [Module A N] → Prop}
    (h_subsingleton : (N : Type v) → [AddCommGroup N] → [Module A N] →
      [Subsingleton N] → P N)
    (h_quotient : (N : Type v) → [AddCommGroup N] → [Module A N] →
      (p : PrimeSpectrum A) → (N ≃ₗ[A] A ⧸ p.1) → P N)
    (h_exact : (N₁ : Type v) → [AddCommGroup N₁] → [Module A N₁] →
      (N₂ : Type v) → [AddCommGroup N₂] → [Module A N₂] →
      (N₃ : Type v) → [AddCommGroup N₃] → [Module A N₃] →
      (f : N₁ →ₗ[A] N₂) → (g : N₂ →ₗ[A] N₃) →
      Function.Injective f → Function.Surjective g → Function.Exact f g →
      P N₁ → P N₃ → P N₂) : P M := by
  sorry -- proof omitted

/-- There are only finitely many associated primes of a finitely generated module
over a Noetherian ring. -/
theorem associatedPrimes.finite
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (M : Type v) [AddCommGroup M] [Module A M] [Module.Finite A M] :
    (associatedPrimes A M).Finite := by
  -- let foo := @IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A _ _
  induction ‹Module A M› using IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A
  · sorry
  · sorry
  · sorry

[Edward van de Meent]

apparently, there already is an issue for this: lean4#4246

[Edward van de Meent]

i've added a comment to the issue mentioning you ran into this today. If you think this is important, do thumbs up the issue

[Edward van de Meent]

aside from this issue, if you are planning on PRing the induction principle in mathlib, the P argument should be called motive

[Jz Pan]

Thank you! Your writing make it works! So if I understand correctly, the induction variable is the last property of M I need to use? In this case it is Module A M.

import Mathlib

@[elab_as_elim]
theorem IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    ⦃M : Type v⦄ [AddCommGroup M] (_ : Module A M) [Module.Finite A M]
    {P : (N : Type v) → [AddCommGroup N] → [Module A N] → Prop}
    (h_subsingleton : (N : Type v) → [AddCommGroup N] → [Module A N] →
      [Subsingleton N] → P N)
    (h_quotient : (N : Type v) → [AddCommGroup N] → [Module A N] →
      (p : PrimeSpectrum A) → (N ≃ₗ[A] A ⧸ p.1) → P N)
    (h_exact : (N₁ : Type v) → [AddCommGroup N₁] → [Module A N₁] →
      (N₂ : Type v) → [AddCommGroup N₂] → [Module A N₂] →
      (N₃ : Type v) → [AddCommGroup N₃] → [Module A N₃] →
      (f : N₁ →ₗ[A] N₂) → (g : N₂ →ₗ[A] N₃) →
      Function.Injective f → Function.Surjective g → Function.Exact f g →
      P N₁ → P N₃ → P N₂) : P M := by
  sorry

/-- There are only finitely many associated primes of a finitely generated module
over a Noetherian ring. -/
theorem associatedPrimes.finite
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (M : Type v) [AddCommGroup M] [Module A M] [Module.Finite A M] :
    (associatedPrimes A M).Finite := by
  induction ‹Module A M› using IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A with
  | h_subsingleton N => simp [associatedPrimes.eq_empty_of_subsingleton]
  | h_quotient N p f => sorry
  | h_exact N₁ N₂ N₃ f h hf hg hfg h₁ h₃ => sorry

[Jz Pan]

Or should I say the induction variable is the last arguments in P?
It turns out that the last property I need to use is Module.Finite A M. So I changed a little and it still works. The syntax is very counter-intuitive, though, in this case one needs to do induction on a Prop! :rolling_on_the_floor_laughing:

[Edward van de Meent]

arguments which get used as arguments to P in the result type of your induction principle are called targets. the values you pass to induction are the values of the targets which are explicit parameters in the induction principle, in the order they occur in in the principle. the other values for the targets are found via unification. In this case, the parameters ⦃M : Type v⦄, [AddCommGroup M] and (_ : Module A M) are targets. Of those, we made only _ : Module A M explicit, so that's the only value you need to supply to induction. the other values are figured out by unification, since both of those arguments are arguments to Module

[Jz Pan]

Edward van de Meent said:

aside from this issue, if you are planning on PRing the induction principle in mathlib, the P argument should be called motive

I see. I've checked docs#Nat.strong_induction_on and it's called P so I also call it P.

[Edward van de Meent]

the naming conventions say they should be called motive

[Edward van de Meent]

and i think someone is working on making sure induction principles follow this convention

[Jz Pan]

Edward van de Meent said:

arguments which get used as arguments to P in the result type of your induction principle are called targets. the values you pass to induction are the values of the targets which are explicit parameters in the induction principle, in the order they occur in in the principle. the other values for the targets are found via unification. In this case, the parameters ⦃M : Type v⦄, [AddCommGroup M] and (_ : Module A M) are targets. Of those, we made only _ : Module A M explicit, so that's the only value you need to supply to induction. the other values are figured out by unification, since both of those arguments are arguments to Module

Thank you! It's clear.

The docstring for induction does not mention the syntax for induction on several variables. So I tried it a little bit:

import Mathlib

@[elab_as_elim]
theorem test33 (m n : ℕ) {motive : ℕ → ℕ → Prop} (stupid : ∀ x y, motive x y) : motive m n :=
  stupid m n

example (m n : ℕ) : m + n = 37 := by
  induction m, n using test33 with
  | stupid x y => sorry

[Adam Topaz]

This would be much less cumbersome if you used docs#ModuleCat

[Junyan Xu]

I see you can't take N to be A ⧸ p.1 in h_quotient due to universe reason, but I don't see why you don't just take N₁ to be a submodule of N₂ and N₃ the quotient module in h_exact.
(BTW I added some analogous induction principles IsSemiprimaryRing.induction and IsFiniteLength.rec.)

[Jz Pan]

Junyan Xu said:

but I don't see why you don't just take N₁ to be a submodule of N₂ and N₃ the quotient module in h_exact

That's a good point. In my original design I'm paranoid by the typeclass inference problems. Let me try if it works.

[Jz Pan]

Ahh, because I'm cheating :joy: h_subsingleton + h_exact implies h_equiv which means that LinearEquiv transfers the property P. If I rephrase h_exact as submodule and quotient, then it cannot imply h_equiv anymore...

[Junyan Xu]

I see, the proof does require the h_equiv. Without h_equiv, we would need to construct a chain of submodule of submodule ... down to the zero module in order to use the submodule/quotient module condition.

One solution to this issue could be the following:

import Mathlib.Algebra.Module.Submodule.Map
import Mathlib.LinearAlgebra.Quotient.Defs
import Mathlib.Order.RelSeries

universe u

variable {R : Type*} [Ring R]
  (P motive : ∀ (M : Type u) [AddCommGroup M] [Module R M], Prop)
  {M : Type u} [AddCommGroup M] [Module R M]
  (r : Rel (Submodule R M) (Submodule R M))
  (hr : ∀ m m', r m m' → m ≤ m' ∧ P (m' ⧸ m.comap m'.subtype))
  (hP : ∀ {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (_ : M ≃ₗ[R] N), P M ↔ P N)
  (s : RelSeries r) (h_head : s.head = ⊥) (h_last : s.last = ⊤)
  (subsingleton : ∀ (M : Type u) [AddCommGroup M] [Module R M] [Subsingleton M], motive M)

theorem induction_left
    (left : ∀ (M : Type u) [AddCommGroup M] [Module R M] (N : Submodule R M),
      P N → motive (M ⧸ N) → motive M) :
    motive M := by
  sorry

theorem induction_right
    (right : ∀ (M : Type u) [AddCommGroup M] [Module R M] (N : Submodule R M),
      P (M ⧸ N) → motive N → motive M) :
    motive M := by
  sorry

Note that I require P (N ≃ₗ[A] A ⧸ p.1 in your case) to be stable under isomorphisms but not motive.
I think they can be proven by induction on the length of the RelSeries. If it's of length n+1, you can get a RelSeries of length n from 0 to the n-th term, and another one from the 1st term to M.

[Antoine Chambert-Loir]

Couldn't you ask to prove motive M -> motive N if there is a linear equivalence from M to N ?

[Jz Pan]

if you are planning on PRing the induction principle in mathlib, the P argument should be called motive

PR created as #24242, coauthored by @Nailin Guan

[Jz Pan]

Antoine Chambert-Loir said:

Couldn't you ask to prove motive M -> motive N if there is a linear equivalence from M to N ?

Yes, it's natural to ask the user to prove h_subsingleton, h_quotient, h_equiv and h_exact. I just mean that under current design of h_exact, the h_equiv could be derived from h_subsingleton and h_exact.

[Jz Pan]

Junyan Xu said:

One solution to this issue could be the following

Interesting. Let me see what does it mean. First we have a property P on modules which is stable under isomorphisms (P M → P N is harmless since we can use LinearEquiv.symm to get another direction).
We have 0 = M₀ ≤ M₁ ≤ M₂ ≤ ... ≤ Mₙ = M, such that for each i, Mᵢ / Mᵢ₋₁ satisfies property P.
(So in our application P is being isomorphic to A / p for some p.)
We also have a property motive which holds for zero modules... OK.