[Merged by Bors] - feat(Algebra/Module/Submodule): Symmetric submodules are modular elements in the lattice of submodules over a semiring

[martinwintermath]

Add two lemmas that are replacements for modularity on the lattice of submodules that are not necessarily over a ring, but a semiring:

• sup_inf_assoc_of_le_of_neg_le: if s ≤ p and -s ≤ p then (s ⊔ t) ⊓ p = s ⊔ (t ⊓ p)
• inf_sup_assoc_of_le_of_neg_le: if p ≤ s and -p ≤ s then (s ⊓ t) ⊔ p = s ⊓ (t ⊔ p)

This allows to shorten the proof that the lattice of submodules over a ring is modular.

I also add specialized versions for cones.

---

[github-actions]

PR summary fa6418a815

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ inf_sup_assoc_of_le_of_neg_le
+ inf_sup_assoc_of_le_of_submodule_le
+ instance : IsModularLattice (Submodule R M) := ⟨fun x _ hxy _ _ => by
+ sup_inf_assoc_of_le_of_neg_le
+ sup_inf_assoc_of_le_submodule
- instance : IsModularLattice (Submodule R M)

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[ocfnash]

I made two inline comments below but I now realise there is a bigger issue here: I think the restriction of scalars is a red herring. The thing that makes p behave in the modular fashion is that it is closed under negation.

So I think the following is a better statement:

variable (S : Type*) {M : Type*} [AddCommGroup M] [Semiring S] [Module S M]

lemma sup_inf_assoc_of_forall_neg_mem {s : Submodule S M} (t : Submodule S M)
    {p : Submodule S M} (hp : ∀ x, x ∈ p ↔ -x ∈ p) (hsp : s ≤ p) :
    (s ⊔ t) ⊓ p = s ⊔ (t ⊓ p) := by

This in turn raises a bigger question: should we have a dedicated subobject for such submodules? Probably not but it might be worth a little thought.

[martinwintermath]

I think the restriction of scalars is a red herring.

It is precisely the version that we need for convex cones, which are implemented as Submodule R≥0 M. There it is important that "closed under negation" can be inferred automatically from [Ring R].
I could implement yours as a second version. Or I could specialize the restrictScalars version to cones-only and move it to the convex cone files (which is what I had initially anyway, but then I generalized).

Regarding dedicated subobject: I played with the idea of a "generalized submodule", something like Submodule R M but in a Module S M, where S is a restriction of R. Currently cones are positive-scalar submodules of an ambient space Module R M. But one could think if them as their own spaces as well. And then it would be neat to still have "R-submodules" for them, like PointedCone.lineal.

There also is AddSubmonoid.support. Maybe relevant.

[ocfnash]

Even though in your application there are two sets of scalars, I'm not convinced that this is the API we should be building here. Instead I propose that we add the following lemmas:

section Semiring

variable {S : Type*} [Semiring S] [Module S M]

lemma sup_inf_assoc_of_le_of_neg_mem_iff
    {s p : Submodule S M} (t : Submodule S M) (hp : ∀ x, -x ∈ s ↔ x ∈ s) (hsp : s ≤ p) :
    (s ⊔ t) ⊓ p = s ⊔ (t ⊓ p) := by
  sorry

lemma inf_sup_assoc_of_le_of_neg_mem_iff
    {s p : Submodule S M} (t : Submodule S M) (hp : ∀ x, -x ∈ p ↔ x ∈ p) (hsp : p ≤ s) :
    (s ⊓ t) ⊔ p = s ⊓ (t ⊔ p) := by
  rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_mem_iff t hp hsp, inf_comm, sup_comm]

end Semiring

exactly here and while we're at it use this to golf the proof of modularity just below as follows

- instance : IsModularLattice (Submodule R M) :=
-   ⟨fun y z xz a ha => by
-     rw [mem_inf, mem_sup] at ha
-     rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩
-     rw [mem_sup]
-     refine ⟨b, hb, c, mem_inf.2 ⟨hc, ?_⟩, rfl⟩
-     rw [← add_sub_cancel_right c b, add_comm]
-     apply z.sub_mem haz (xz hb)⟩
+ instance : IsModularLattice (Submodule R M) :=
+   ⟨fun y z xz a ha => by rwa [← sup_inf_assoc_of_le_of_neg_mem_iff y (by simp) xz]⟩

I claim that the two lemmas should be sufficient for your needs since the following is true by simp:

example (S : Type*) {R M : Type*} [Ring R] [AddCommGroup M] [Semiring S]
    [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {x : M} {p : Submodule R M} :
    -x ∈ p.restrictScalars S ↔ x ∈ p.restrictScalars S := by
  simp

[martinwintermath]

Alright, I went with your versions for general submodules. The short proof for inf_sup_assoc_of_le_of_neg_mem_iff did not work though since there was a problem with the statement of the other lemma.

I do however really hope for the specialized versions for cones since it is a common enough use case in our local repo (which is about cone theory, and will be PR-ed bit by bit). I added these lemmas.

[ocfnash]

I do however really hope that we can have the specialized versions for cones since it is a common enough use case. I added these lemmas.

Yes, I agree the specialisations for cones deserve to exist.

[martinwintermath]

-awaiting-author

@ocfnash I don't understand why this label was added last week, I implemented all requests, no?

[ocfnash]

You can weaken the assumption here slightly:

Suggested change

	{p : Submodule R M} (hp : ∀ x, -x ∈ p ↔ x ∈ p) (hsp : s ≤ p) :
	{p : Submodule R M} (hp : ∀ x, -x ∈ s ↔ x ∈ s) (hsp : s ≤ p) :

[martinwintermath]

I don't think this is weaker: s being symmetric and p being symmetric are independent statements. I think this changes the statement in a way that we don't want (I suspect it makes it trivially equivalent to inf_sup_assoc_of_le_of_neg_mem_iff rather than dual to it). Am I missing something?

[ocfnash]

You're quite right!

(I guess the reason I had left that review pending was that I was still thinking about this, and I then yesterday I just mindlessly submitted.)

Looking now, I think the "right" suggestion is that we should prove:

lemma sup_inf_assoc_of_neg_le_of_le {s : Submodule R M} (t : Submodule R M)
    {p : Submodule R M} (hp : {-x | x ∈ s} ≤ p) (hsp : s ≤ p) :
    (s ⊔ t) ⊓ p = s ⊔ (t ⊓ p) := by

If we do this then we do get a symmetric lemma below as follows:

lemma inf_sup_assoc_of_neg_le_of_le {s : Submodule R M} (t : Submodule R M)
    {p : Submodule R M} (hp : {-x | x ∈ p} ≤ s) (hsp : p ≤ s) :
    (s ⊓ t) ⊔ p = s ⊓ (t ⊔ p) := by
  rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_mem_iff t hp hsp, inf_comm, sup_comm]

and I note that these assumptions are true weakenings in view of:

example {s p : Submodule R M} (hp : ∀ x, -x ∈ p ↔ x ∈ p) (hsp : s ≤ p) :
    {-x | x ∈ s} ≤ p := by
  rintro - ⟨x, hx, rfl⟩
  aesop

example {s p : Submodule R M} (hp : ∀ x, -x ∈ p ↔ x ∈ p) (hsp : p ≤ s) :
    {-x | x ∈ p} ≤ s := by
  rintro - ⟨x, hx, rfl⟩
  aesop

[martinwintermath]

That works. The one thing that bothers me is that {-x | x ∈ s} ≤ p should be written as -s ≤ p but we can't access Submodule.instPointwiseNeg without creating circular imports. I would need to move to another file. But then I can't use it to prove IsModuleLattice for submodules.

I can write it as ∀ x ∈ s, -x ∈ p (and the previous versions should also have been written as ∀ x ∈ p, -x ∈ p since we need only one direction of the ↔).

[martinwintermath]

@ocfnash Okay I implemented it locally. I agree that your versions are more intellectually pleasing. But they are also a bit more cumbersome to use since the new hypothesis is not provable from only a simp anymore. Should we have both versions? What do you think?

[martinwintermath]

@ocfnash Regarding the Pointwise locale: I think we have an unfortunate import order. There are six lemmas in Pointwise.lean that mention the span; five of them cause problems when Span/Basic.lean is removed as an import. I think that these lemmas should be moved to Span/Basic.lean. Then the import order can be reversed, and we can write the hypothesis as -s ≤ p. This seems correct because other lemmas already make use of pointwise negation, e.g. -s when s : Set M.

[ocfnash]

I'm happy to prioritise getting this PR with your cone lemmas into master and leave a bit of clean up for a subsequent PR which either you or I could do.

I see the argument for reversing the import order (and I note your point about the shortcomings of the existing lemma span_neg) but I think sorting this all out might be a little annoying. If you really want to attempt this as part of these changes then that is great, but I don't think that has to happen.

[martinwintermath]

I agree. I implemented your weakened hypotheses (and removed the other versions) and will approve the PR once CI went through. The rest is for a future PR.

[ocfnash]

With the suggestion above, this can be just:

Suggested change

	ext x
	simp only [mem_inf, mem_sup]
	constructor
	· rintro ⟨y, ⟨hys, hyt⟩, z, hzp, hyzx⟩
	exact ⟨by simpa [← hyzx] using add_mem hys (hsp hzp), ⟨y, hyt, z, hzp, hyzx⟩⟩
	· rintro ⟨hxs, y, hyt, z, hzp, hyzx⟩
	use y
	refine ⟨⟨?_, hyt⟩, ⟨z, hzp, hyzx⟩⟩
	rw [← add_left_inj, add_neg_cancel_right] at hyzx
	simpa [hyzx] using add_mem hxs <| hsp <| (hp _).mpr hzp
	rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_mem_iff t hp hsp, inf_comm, sup_comm]

[ocfnash]

I don't understand why this label was added last week, I implemented all requests, no?

Apologies @martinwintermath I had written two more suggestions but not clicked GitHub's "Submit review" button so they were visible to me (albeit with some "Pending" text which I failed to notice) but not to you.

[ocfnash]

Thanks!

I've left one last suggestion. I think it would be nice to take this up, but I won't insist.

bors d+

[ocfnash]

You're quite right!

(I guess the reason I had left that review pending was that I was still thinking about this, and I then yesterday I just mindlessly submitted.)

Looking now, I think the "right" suggestion is that we should prove:

lemma sup_inf_assoc_of_neg_le_of_le {s : Submodule R M} (t : Submodule R M)
    {p : Submodule R M} (hp : {-x | x ∈ s} ≤ p) (hsp : s ≤ p) :
    (s ⊔ t) ⊓ p = s ⊔ (t ⊓ p) := by

If we do this then we do get a symmetric lemma below as follows:

lemma inf_sup_assoc_of_neg_le_of_le {s : Submodule R M} (t : Submodule R M)
    {p : Submodule R M} (hp : {-x | x ∈ p} ≤ s) (hsp : p ≤ s) :
    (s ⊓ t) ⊔ p = s ⊓ (t ⊔ p) := by
  rw [sup_comm, inf_comm, ← sup_inf_assoc_of_le_of_neg_mem_iff t hp hsp, inf_comm, sup_comm]

and I note that these assumptions are true weakenings in view of:

example {s p : Submodule R M} (hp : ∀ x, -x ∈ p ↔ x ∈ p) (hsp : s ≤ p) :
    {-x | x ∈ s} ≤ p := by
  rintro - ⟨x, hx, rfl⟩
  aesop

example {s p : Submodule R M} (hp : ∀ x, -x ∈ p ↔ x ∈ p) (hsp : p ≤ s) :
    {-x | x ∈ p} ≤ s := by
  rintro - ⟨x, hx, rfl⟩
  aesop

[mathlib-bors]

✌️ martinwintermath can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[martinwintermath]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job

[martinwintermath]

Follow up PR: #38013