[Merged by Bors] - feat: In a ring, sets act on submodules

[jjaassoonn]

If $M$ is an $R$-module, $N$ a submodule and $S$ a subset of $R$. Then we can define $S \cdot N$ to be the smallest submodule containing all $s \cdot n$ where $s \in S$ and $n \in N$

---

[alreadydone]

I think in locale Pointwise this is even a MulAction.

[jjaassoonn]

I think in locale Pointwise this is even a MulAction.

It is a distributive multicative action! Thanks for pointing this out.

[alreadydone]

It is a distributive multicative action! Thanks for pointing this out.

Thanks for confirming! If Set R were a Semiring I think we can also show it's a Module, but it's not (distributivity doesn't hold). So we have to wait until we generalize the typeclass assumptions of Module for that.

[eric-wieser]

! If Set R were a Semiring

It is when using the SetSemiring alias

[eric-wieser]

I think we might already have a Module (Ideal R) (Submodule R M) instance; is this new instance the same a that one composed with Ideal.span?

[alreadydone]

It is when using the SetSemiring alias

That's using union as addition, not pointwise addition inherited from addition on R.

I think we might already have a Module (Ideal R) (Submodule R M) instance; is this new instance the same a that one composed with Ideal.span?

I think yes (and loogle found Submodule.moduleSubmodule). (Should we restrict to CommSemiring?)

[jjaassoonn]

It is when using the SetSemiring alias

That's using union as addition, not pointwise addition inherited from addition on R.

I think we might already have a Module (Ideal R) (Submodule R M) instance; is this new instance the same a that one composed with Ideal.span?

I think yes (and loogle found Submodule.moduleSubmodule). (Should we restrict to CommSemiring?)

Should I re-implement this in terms of span composing with soul then?

[eric-wieser]

I suspect this has the same problem as you remarked about for the case of non-commutative rings R

[eric-wieser]

Do you actually care about the non-commutative case?

[jjaassoonn]

Do you actually care about the non-commutative case?

No,not really. But we should have it work for noncomm cases in case other people care about them right?

[jjaassoonn]

If these lemmas are already in the Submodule namespace, maybe we don't need to repeat submodule in the lemma name?

submodule has been removed from all names

[eric-wieser]

This generalizes to

Suggested change

	protected def pointwiseSetSMul : SMul (Set R) (Submodule R M) where
	protected def pointwiseSetSMul : SMul (Set S) (Submodule R M) where

right? How may of the other results also generalize for free?

[jjaassoonn]

What is S here? Is it another ring of which M is a module?

[eric-wieser]

Yes; or more generally, a monoid for which it is a distribMulAction.

[jjaassoonn]

Everything upto induction principal should work mutatis mutandis. My hunch is that if we further assume [SMulCommClass R S M] then everything should work?

[jjaassoonn]

So the generalized principal is this

variable {s N} in
@[elab_as_elim]
lemma set_smul_inductionOn {motive : (x : M) → (_ : x ∈ s • N) → Prop}
    (x : M)
    (hx : x ∈ s • N)
    (smul₀ : ∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N),
      motive (r • n) (mem_set_smul_of_mem_mem mem₁ mem₂))
    (smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N) ,
      motive m mem → motive (r • m) (Submodule.smul_mem _ r mem)) --
    (add : ∀ ⦃m₁ m₂ : M⦄ (mem₁: m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N),
      motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) (Submodule.add_mem _ mem₁ mem₂))
    (zero : motive 0 (Submodule.zero_mem _)) :
    motive x hx :=
  let ⟨_, h⟩ := set_smul_le s N
    { carrier := { m | ∃ (mem : m ∈ s • N), motive m mem },
      zero_mem' := ⟨Submodule.zero_mem _, zero⟩
      add_mem' := fun ⟨mem, h⟩ ⟨mem', h'⟩ ↦ ⟨_, add mem mem' h h'⟩
      smul_mem' := fun r x ⟨mem, h⟩ ↦ ⟨_, smul₁ r mem h⟩ }
    (fun _ _ mem mem' ↦ ⟨mem_set_smul_of_mem_mem mem mem', smul₀ mem mem'⟩) hx
  h

But to change the next lemma

lemma set_smul_eq_map [SMulCommClass R R N] [Module S N]  [SMulCommClass S R N] :
    s • N =
    Submodule.map
      (N.subtype.comp (Finsupp.lsum R <| DistribMulAction.toLinearMap _ _))
      (Finsupp.supported N R s) := by

I need N to be both a R-submodule and S-submodule, so I included [Module S N], can I somehow say this module structure is restricted from [Module S M], or should I just I added some assumption like \forall s \in S, n \in N, s \bu n \in N

[jjaassoonn]

Is perhaps Subbimodule relevant?

[eric-wieser]

I think I would just leave this one ungeneralized

[jjaassoonn]

In 7d37123 and eecb383, the generalization has been done. Things that are not generalized were left some comments explaining why they can't or won't be generalized

[jjaassoonn]

If we generalize so that r • N makes sense for all r : S, then Submodule.singleton_set_smul
and Submodule.singleton_set_smul can be generalized as well. We can prove x ∈ ({r} : Set S) • N ↔ ∃ (m : M), m ∈ N ∧ x = r • m but we can't say ({r} : Set R) • N = r • N

[erdOne]

LGTM modulo the minor comment above
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style