Zulip Chat Archive

Stream: maths

Topic: submodule induction


Antoine Chambert-Loir (Sep 23 2022 at 08:04):

I found that I had the need of a more general induction procedure for ideals or submodules, similar to docs#submodule.induction_on, when one already knows that the submodule will be contained in a given submodule. In this case, the hypotheses can be weakened. Here is an example:

universes u v
variables {R : Type u} {M : Type v} {F : Type*} {G : Type*}
variables [comm_semiring R] [add_comm_monoid M] [module R M]
variables {I J : ideal R} {N P Q : submodule R M}

theorem submodule.smul_induction_on' {p : M  Prop} (hQ :  x, x  I  N  x  Q) {x} (H : x  I  N)
  (Hb :  (r  I) (n  N), p (r  n))
  (H1 :  (x  Q) (y  Q), p x  p y  p (x + y)) : p x :=
begin
  suffices : x  Q  p x, exact this.2,
  exact submodule.smul_induction_on H
  (λ a ha x hx, ⟨(hQ (a  x) (submodule.smul_mem_smul ha hx)), Hb a ha x hx⟩)
  (λ x y hx hy, Q.add_mem hx.1 hy.1, H1 x hx.1 y hy.1 hx.2 hy.2⟩),
end

On the other hand one can mimick this everytime. Do you believe that the more general procedure should be added to mathlib ?

Patrick Massot (Sep 23 2022 at 08:05):

Yes, induction principles are good.

Antoine Chambert-Loir (Sep 23 2022 at 08:43):

In fact, I realize that docs#submodule.supr_induction should be generalized from

lemma supr_induction {ι : Sort*} (p : ι  submodule R M) {C : M  Prop} {x : M} (hx : x   i, p i)
  (hp :  i (x  p i), C x)
  (h0 : C 0)
  (hadd :  x y, C x  C y  C (x + y)) : C x := sorry

to

lemma supr_induction' {ι : Sort*} (p : ι  submodule R M) {C : M  Prop} {x : M} (hx : x   i, p i)
  (hp :  i (x  p i), C x)
  (h0 : C 0)
  (hadd :  (x   i, p i) (y   i, p i), C x  C y  C (x + y)) : C x := sorry

(the proof is easy, up to a similar modification of add_submonoid.supr_induction and possibly going on inductively…)

Antoine Chambert-Loir (Sep 23 2022 at 08:44):

(The present statement requires that the predicate C be additive, while it is sufficient that it is additive on ⨆ i, p i.

Eric Wieser (Sep 23 2022 at 08:59):

I think that suggestion is the same as how we extended docs#submodule.span_induction with docs#submodule.span_induction'?

Eric Wieser (Sep 23 2022 at 08:59):

In fact, submodule.span_induction' suggests a more general form where even the motive depends on (∈ ⨆ i, p i)

Eric Wieser (Sep 23 2022 at 09:00):

... Which exists already, it's docs#submodule.supr_induction' and I wrote it at the same time as the unprimed version in #11556!

Eric Wieser (Sep 23 2022 at 09:04):

Based on that, I would say that submodule.smul_induction_on' is a good idea to PR, but it should be generalized to {p : Π (x : M), x ∈ I • N → Prop}

Antoine Chambert-Loir (Sep 23 2022 at 15:27):

OK, I'll push something.
One remark : it seems to me that the order of the arguments for doc#submodule.span_induction' is a bit strange : since {x} (hx : x ∈ submodule.span R s) are the last one, the function requires four _ to be easily applied. The other induction lemmas have {x} (hx) for their first argument.

Eric Wieser (Sep 23 2022 at 16:17):

Lemmas tagged with elab_as_eliminator shouldn't be used with apply anyway, as they tend not to infer the motive correctly

Eric Wieser (Sep 23 2022 at 16:18):

They behave better with refine, but at that point the argument order is irrelevant


Last updated: Dec 20 2023 at 11:08 UTC