Remove redundancy in inductive definition

Stream: lean4

[Junyan Xu]

Is there a way to shorten this inductive definition?

import Mathlib.RingTheory.Artinian

universe u

variable (R : Type*) [Ring R]

inductive IsFiniteLength : ∀ (M : Type u) [AddCommGroup M] [Module R M], Prop
  | of_subsingleton M [AddCommGroup M] [Module R M] : Subsingleton M → IsFiniteLength M
  | of_simple_quotient M [AddCommGroup M] [Module R M] (N : Submodule R M) :
    IsFiniteLength N → IsSimpleModule R (M ⧸ N) → IsFiniteLength M

If I do

inductive IsFiniteLength (M : Type u) [AddCommGroup M] [Module R M] : Prop
  | of_subsingleton : Subsingleton M → IsFiniteLength M
  | of_simple_quotient (N : Submodule R M) :
    IsFiniteLength N → IsSimpleModule R (M ⧸ N) → IsFiniteLength M

I get

inductive datatype parameter mismatch
  ↥N
expected
  M

[Kevin Buzzard]

(off-topic : Wouldn't it just be easier to demand a finite saturated filtration rather than going down this route?)

[Junyan Xu]

I think the induction principle (IsFiniteLength.rec) generated by this is quite nice and allows you to quickly prove properties (e.g. Noetherian/Artinian) of finite length modules from properties of simple modules.

[Kevin Buzzard]

I guess inductive IsFiniteLength (M : Type u) [AddCommGroup M] [Module R M] : Prop doesn't work because this is only giving you ways to prove that M is finite length (hence the error). This is how inductive props work I guess. What's wrong with the first version?

[Junyan Xu]

Just want to know if there's a way to avoid writing M [AddCommGroup M] [Module R M] three times ...

[Junyan Xu]

Now this is probably a Lean bug:

import Mathlib.RingTheory.Artinian
universe u

variable (R : Type*) [Ring R]

/-- A module of finite length is either a subsingleton or a simple extension of a module known
to be of finite length. -/
inductive IsFiniteLength : ∀ (M : Type u) [AddCommGroup M] [Module R M], Prop
  | of_subsingleton {M} [AddCommGroup M] [Module R M] [Subsingleton M] : IsFiniteLength M
  | of_simple_quotient {M} [AddCommGroup M] [Module R M] {N : Submodule R M}
      [IsSimpleModule R (M ⧸ N)] : IsFiniteLength N → IsFiniteLength M

variable {R} {M : Type*} [AddCommGroup M] [Module R M]

theorem LinearEquiv.isFiniteLength (h : IsFiniteLength R M) :
    ∀ {N : Type u} [AddCommGroup N] [Module R N], (M ≃ₗ[R] N) → IsFiniteLength R N :=
  h.rec _ _

The infoview at the two placeholders are
image.png
image.png

[Junyan Xu]

with a phantom variable N✝ and associated instances, and I don't think the second goal is solvable. If I manually specify the motive

h.rec (motive := fun M _ _ _ ↦ ∀ {N} [AddCommGroup N] [Module R N], (M ≃ₗ[R] N) → IsFiniteLength R N) _ _

then the infoview becomes sane and the goal solvable, even though N✝ is still in the context.

[Yury G. Kudryashov]

Lean autointroduces implicit vars in term mode.

[Yury G. Kudryashov]

I think that you should move {N} etc before : and use induction h.

[Junyan Xu]

You're right, my bad. If I replace {} by ⦃⦄ then N✝ disappears and I no longer need to specify the motive:

theorem LinearEquiv.isFiniteLength (h : IsFiniteLength R M) :
    ∀ ⦃N : Type u⦄ [AddCommGroup N] [Module R N], (M ≃ₗ[R] N) → IsFiniteLength R N :=
  h.rec (fun _M _ _ _ {_N} _ _ e ↦ have := e.symm.toEquiv.subsingleton; .of_subsingleton)
    fun _M _ _ S _ _ ih {_N} _ _ e ↦
      have := IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
      .of_simple_quotient (ih <| e.submoduleMap S)

Yury G. Kudryashov said:

I think that you should move {N} etc before : and use induction h.

I'll check whether this shortens the proof.

[Junyan Xu]

I tested and this works nicely:

variable {R} {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

theorem LinearEquiv.isFiniteLength (e : M ≃ₗ[R] N)
    (h : IsFiniteLength R M) : IsFiniteLength R N := by
  induction' h with M _ _ _ M _ _ S _ _ ih generalizing N
  · have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
  · have := IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
    exact .of_simple_quotient (ih <| e.submoduleMap S)

Thanks!

[Junyan Xu]

Off topic: #17478 contains the definition IsFiniteLength and #17557 shows a semisimple ring is Artinian.

[Johan Commelin]

I kicked the deps on the bors queue