transitioning between various subobjects

Stream: mathlib4

[Jireh Loreaux]

Currently, transitioning between various subobjects can be quite painful at times. I would like to lessen this burden. To give just a small flavor of what I mean, consider the following goal:

import Mathlib

variable {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]

open Submodule in
lemma AddSubmonoid.closure_subset_span (s : Set M) :
    (AddSubmonoid.closure s : Set M) ⊆ span R s := by
  sorry

While this is relatively easy to prove, it's not absolutely immediate, as one would hope. Moreover, there would be a similar lemma for subalgebras, etc., which leads you to want to prove the following lemma:

import Mathlib

variable {S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M]

@[to_additive (attr := simp)]
lemma Submonoid.closure_subset {t : Set M} {s : S} :
    (Submonoid.closure t : Set M) ⊆ s ↔ t ⊆ s := by
  sorry

This is totally natural, but it's actually surprisingly annoying to prove with the current state of Mathlib (unless someone proves me wrong aside from what follows below). One "natural" way to prove it is to construct a Submonoid with carrier (↑s : Set M), and then apply Submonoid.closure_le, but it's annoying to need to do this. We could, as we do with morphisms, create coercions from subobject classes to the relevant subobjects, but I can already hear Eric Wieser's cries of anguish (not to mention the cries of Lean's elaborator) at the idea.

[Jireh Loreaux]

Instead, I propose to do something different. I want to add the following CanLift instances for subobjects across Mathlib. In this way, we can always lift the coercion to Set of an element in a subobject class to whichever subobject kind we want. Moreover, the using portion should always be provable by aesop. In this way, it should be relatively painless to pass between various "copies" of a subobject of different kinds within a single proof, all of them united by the fact that they have the same coercion to set. As this example shows, the ability to use lift makes the proof trivial.

import Mathlib

variable {S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M]

@[to_additive]
instance : CanLift (Set M) (Submonoid M) (↑)
    (fun s ↦ 1 ∈ s ∧ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) where
  prf s h := ⟨{ carrier := s, one_mem' := h.1, mul_mem' := h.2 }, rfl⟩

@[to_additive (attr := simp)]
lemma Submonoid.closure_subset {t : Set M} {s : S} :
    (Submonoid.closure t : Set M) ⊆ s ↔ t ⊆ s := by
  lift (s : Set M) to Submonoid M using (by aesop) with s
  simp

@[to_additive]
lemma Submonoid.mem_of_mem_closure {t : Set M} {s : S} (h : t ⊆ s) {x : M}
    (hx : x ∈ Submonoid.closure t) : x ∈ s :=
  Submonoid.closure_subset.mpr h hx

Thoughts?

[Andrew Yang]

Not against the idea in general, but I don't think that this is that annoying to prove?

variable {S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M]

@[to_additive (attr := simp)]
lemma Submonoid.closure_subset {t : Set M} {s : S} :
    (Submonoid.closure t : Set M) ⊆ s ↔ t ⊆ s :=
  Submonoid.closure_le (s := t) (S := ⟨⟨s, mul_mem⟩, one_mem s⟩)

[Andrew Yang]

Also for HomClasss, we have things like docs#RingHomClass.toRingHom. Maybe we can copy it here?

[Edward van de Meent]

either that or generalize the api to using SubMonoidClass rather than Submonoid?

[Jireh Loreaux]

Andrew Yang said:

but I don't think that this is that annoying to prove?

For submonoids, you can just fill all the stuff manually, sure, but it gets annoying when you're working with say, docs#Subalgebra or docs#StarSubalgebra. And it would be nice to not to be forced to fill the arguments.

[Jireh Loreaux]

Andrew Yang said:

Also for HomClasss, we have things like docs#RingHomClass.toRingHom. Maybe we can copy it here?

I mentioned this in my post. These are the coercions which, while we could have them, I think we may want to avoid.

[Jireh Loreaux]

Edward van de Meent said:

either that or generalize the api to using SubMonoidClass rather than Submonoid?

You can't do that without (a) writing the coercions that have been discussed, or (b) significantly decreasing the utility of the API. This is because if s : S with SubmonoidClass S M and t : Set M, you can't make sense of Submonoid.closure t ≤ s, because you can't coerce (without adding a new coercion) ↑s : Submonoid M, so the ≤ can't make sense. That is, unless you go to sets, but that decreases the utility of the API for honest-to-god Submonoids.

[Jireh Loreaux]

If you want a more real-world example of where the lack of this API can really bite you, please witness the contortions necessary in #12889 and #13326. There I ended up proving something related to Submonoid.closure_subset above which is in the library as docs#Submodule.coe_span_eq_self. That particular declaration is not the main pain point of the PR, only an example that this has come up before for me.

[Andrew Yang]

Jireh Loreaux said:

Andrew Yang said:

Also for HomClasss, we have things like docs#RingHomClass.toRingHom. Maybe we can copy it here?

I mentioned this in my post. These are the coercions which, while we could have them, I think we may want to avoid.

I don't like the coercions of homomorphisms at all but I could see them useful as standalone defs. (That is, writing .ofClass S manually if you have a Submonoid.ofClass)

[Jireh Loreaux]

I could see that, although I think the CanLift instances could be useful in their own right.

[Nailin Guan]

Sorry that I have something that don't unduerstand, why we don't like the coercion from AddSubgroupClass to AddSubgroup? Is there a general reason or some examples? Thanks

[Jireh Loreaux]

I think the biggest reason is this: you want to insert these manually. Otherwise you might end up with statements where your S : Subalgebra R A was coerced to a Submonoid A unintentionally. In general, I don't want to encourage using these in statements (so that we don't have a million and one ways to spell something), but only want them easily available in proofs, which is why I proposed CanLift instances.

[Nailin Guan]

Thanks, I know why now.
Another question: how should we use CanLift? I doesn't know how to trigger it, my original proof is failing everywhere :sweat_smile:

[Jireh Loreaux]

CanLift instances are used when you call the lift tactic.

[Nailin Guan]

Thanks, I'll try to give a fix.

[Nailin Guan]

One more thing, can you have a look for #22230? Is the defs and instances added correctly? Thanks

[Jireh Loreaux]

Looks good. Can you do it for all the subobject classes you can find? (Subsemigroup, Submodule, Subsemiring, Subring, NonUnitalSubsemiring, NonUnitalSubring, Subalgebra, NonUnitalSubalgebra, StarSubalgebra, NonUnitalStarSubalgebra)

[Nailin Guan]

Sorry I have another question first, is it safe to add coe S (ofClass S) for S of SubgroupClass S G, I met some problem with this so I want to add it.

[Nailin Guan]

Jireh Loreaux said:

Looks good. Can you do it for all the subobject classes you can find? (Subsemigroup, Submodule, Subsemiring, Subring, NonUnitalSubsemiring, NonUnitalSubring, Subalgebra, NonUnitalSubalgebra, StarSubalgebra, NonUnitalStarSubalgebra)

This is a bit crazy, I need the coe for Subgroup in an existing PR, I think I can open another one.

[Jireh Loreaux]

Nailin Guan said:

Sorry I have another question first, is it safe to add coe S (ofClass S) for S of SubgroupClass S G, I met some problem with this so I want to add it.

It's a bit unclear what you mean. Do you mean you want a Coe instance from terms of an element S of a subgroup class to terms of SubgroupClass S G (e.g., you want to be able to coerce, for S : Subring R, some x : S to ↑x : ofClass S)? if so, then no, definitely don't do that.

[Jireh Loreaux]

Nailin Guan said:

This is a bit crazy

It should only be around ~100 lines of mostly copy paste?

[Jireh Loreaux]

I've done the rest of this in #23708