inf/sup lemmas for upwards/downwards closed classes

Stream: mathlib4

[Martin Winter]

I frequently use that FG submodules are closed under intersection (over noetherian rings). The following lemmas therefore appeared useful to me:

theorem FG.inf_left {S : Submodule R M} (hS : S.FG) (T : Submodule R M) : (S ⊓ T).FG :=
  hS.of_le inf_le_left

theorem FG.inf_right (S : Submodule R M) {T : Submodule R M} (hT : T.FG) : (S ⊓ T).FG :=
  hT.of_le inf_le_right

I proposed them as part of #33993 but was asked to remove them because they can be easily proved from FG being downwards closed.

The same happened in my PR #34006 on co-finitely generated submodules. I proposed

theorem CoFG.sup_left {S : Submodule R M} (hS : S.CoFG) (T : Submodule R M) : (S ⊔ T).CoFG
  := hS.of_cofg_le le_sup_left

theorem CoFG.sup_right (S : Submodule R M) {T : Submodule R M} (hT : T.CoFG) : (S ⊔ T).CoFG
  := hT.of_cofg_le le_sup_right

but was asked to remove because these lemmas are "just a more obscure way of saying upwards closed".

I also proposed

alias FG.inf := FG.inf_right
alias CoFG.sup := CoFG.sup_left

I agree that these lemmas are, to a degree, redundant. Nevertheless, here are my main arguments for them:

• discoverability: if I am thinking of sup/inf it is easier for me to discover these lemmas rather than to remember that these classes are also upwards/downwards closed.
• I use them often enough so as to have an actual gain from writing hS.inf T or hS.sup T in place of using the of_le-lemmas all over the place.
• there will be similar lemmas in the future that mix FG and CoFG submodules and the proposed lemmas above complete this family of combinations.

I decided to not push for these in my PRs, but would pick this up again if it becomes too annoying in future PRs to not have them. I also understand that having these lemmas would set a precedent for similar situations. For this reason I would like to have this discussed now, perhaps in order to understand why we absolutely do not want to have them.

[Martin Winter]

@Andrew Yang @Violeta Hernández @Johan Commelin

[Violeta Hernández]

I feel like these lemmas set a bad precedent. Do we also want versions for sInf/sSup? Then surely we also want versions for iInf/iSup, as well as biInf/biSup and now we're writing substantial boilerplate for something that's entirely obvious.

[Violeta Hernández]

The of_le versions also have the advantage that you don't have to remember whether left or right in the theorem name refers to the FG submodule or to the submodule that you're taking an infimum with.

[Martin Winter]

Violeta Hernández said:

I feel like these lemmas set a bad precedent. Do we also want versions for sInf/sSup? Then surely we also want versions for iInf/iSup, as well as biInf/biSup and now we're writing substantial boilerplate for something that's entirely obvious.

To get around the precedent argument we say that these lemmas need to be justified by how often they get used. Then neither all the other sSup/iSup/... lemmas nor analogous lemmas in other situations would follow automatically.

Being "obvious" feels not like a good measure - many things in mathlib are obvious.

[Johan Commelin]

Martin Winter said:

I decided to not push for these in my PRs, but would pick this up again if it becomes too annoying in future PRs to not have them. I also understand that having these lemmas would set a precedent for similar situations. For this reason I would like to have this discussed now, perhaps in order to understand why we absolutely do not want to have them.

Martin Winter said:

To get around the precedent argument we say that these lemmas need to be justified by how often they get used. Then neither all the other sSup/iSup/... lemmas nor analogous lemmas in other situations would follow automatically.

I think this is a good idea. If you need these a lot, and you can golf many bits of proofs, then we should reconsider.

[Martin Winter]

Thanks for everybody's feedback. I will include them in future PRs if they turn out helpful. I will point here for the discussion.