Weakening docs#submodule.mul_induction_on

Stream: maths

[Eric Wieser]

Is it possible to eliminate the hs : ∀ (r : R) x, C x → C (r • x) hypothesis from docs#submodule.mul_induction_on? My hand-wavey argument is that:

1. any element of M * N must be of the form∑ᵢ mᵢ*nᵢ where mᵢ ∈ M and nᵢ ∈ M
2. ha : ∀ x y, C x → C y → C (x + y) already tells us that it's sufficient to prove C (mᵢnᵢ) to show C (∑ᵢ mᵢnᵢ)
3. hm : ∀ (m ∈ M) (n ∈ N), C (m * n) can prove C (mᵢnᵢ)

Is my claim 1) correct? Can I get there without going through docs#submodule.mem_bsupr_iff_exists_dfinsupp?

[Alex J. Best]

Are you talking about docs#submodule.mul_induction_on ?

[Yaël Dillies]

I'm pretty 1 is false when A is noncommutative.

[Yaël Dillies]

Or is it the commutativity of R that matters?

[Eric Wieser]

I think only the commutativity of R matters

[Yaël Dillies]

Then it must be true.

[Eric Wieser]

I think my difficulty amounts to:

-- is this true?
lemma to_add_submonoid_mul (M N : submodule R A) :
  (M * N).to_add_submonoid = M.to_add_submonoid * N.to_add_submonoid := sorry

(which needs #11522 for the * on the LHS)

[Eric Wieser]

Which in turn I think needs:

lemma supr_to_add_submonoid {ι} (M : ι → submodule R A) :
  (⨆ i, M i).to_add_submonoid = ⨆ i, (M i).to_add_submonoid :=
sorry

[Yaël Dillies]

That looks wrong. Surely (M * N).to_add_submonoid = M.to_add_submonoid + N.to_add_submonoid is true instead.

[Yaël Dillies]

Also, you surely meant "the * on the RHS"

[Yaël Dillies]

Oh wait, I was reading docs#submonoid.to_add_submonoid. Your thing is probably true.

[Eric Wieser]

#11525 proves the above supr lemma for sup

[Eric Wieser]

Proof was pretty ugly, but I guess not difficult:

lemma supr_to_add_submonoid {ι : Sort*} (p : ι → submodule R M) :
  (⨆ i, p i).to_add_submonoid = ⨆ i, (p i).to_add_submonoid :=
begin
  apply le_antisymm,
  { intros x hx,
    rw [mem_to_add_submonoid, supr_eq_span] at hx,
    simp_rw [add_submonoid.supr_eq_closure, coe_to_add_submonoid],
    refine submodule.span_induction hx (λ x hx, _) _ (λ x y hx hy, _) (λ r x hx, _),
    { exact add_submonoid.subset_closure hx },
    { exact add_submonoid.zero_mem _ },
    { exact add_submonoid.add_mem _ hx hy },
    { apply add_submonoid.closure_induction hx,
      { rintros x ⟨_, ⟨i, rfl⟩, hix : x ∈ p i⟩,
        apply add_submonoid.subset_closure (set.mem_Union.mpr ⟨i, _⟩),
        exact smul_mem _ r hix },
      { rw smul_zero,
        exact add_submonoid.zero_mem _ },
      { intros x y hx hy,
        rw smul_add,
        exact add_submonoid.add_mem _ hx hy, } } },
  { refine supr_le (λ i, _),
    refine to_add_submonoid_mono _,
    exact le_supr _ i, }
end

Presumably there's a slightly easier way to get there...