mathlib

mathlib copied to clipboard

Add a definition of (bundled) subgroupoid and prove some of their basic properties.

---

Thanks a lot! I corrected the stuff I was OK with and commented on the rest. I've also added a few definitions (mostly about how subgroupoid_le gives rise to morphisms of subgroupoid.coe and everything behaves well).

Wow, thanks for all these suggestions! I will look at everything in detail tomorrow, but in the meantime:

• Re. eq_to_hom, I was actually just a bit scared of using it, but changed it already in my dirty branch here and forgot to bring the changes here too. It's indeed way better.
• Is there a way to accept all the suggestions in one go?

Is there a way to accept all the suggestions in one go?

You should see an "add suggestion to batch" button, and you may commit them together.

OK, I've followed most of the changes you proposed, but:

• For instance (h : S.objs.nonempty) : nonempty S.coe := ⟨⟨h.some,h.some_spec⟩⟩ , the linter is also unhappy with this because it says:

  Error: category_theory.groupoid.subgroupoid.coe.nonempty - Impossible to infer argument 4: (h : S.objs.nonempty)
  

• ~~For the is_subgroupoid business, are you strongly in favour of the set_like route? It looks like a viable way but since the code is already here and works, I'm a bit skeptical of the need to change that part.~~ OK, I changed to using set_like: what do you think of that, @alreadydone ?

Thanks!

For instance (h : S.objs.nonempty) : nonempty S.coe := ⟨⟨h.some,h.some_spec⟩⟩ , the linter is also unhappy with this because it says:

Indeed it shouldn't be an instance. You may add @[nolint has_nonempty_instance] or be satisfied with the instance for the subgroupoid (⊤) given [nonempty C].

I went with using [nonempty …] rather than [….nonempty] and that seems to work.

@alreadydone: OK, corrected following your requests/proposals! I was reluctant to drop the .coe because it's the "canonical" name as far as I'm aware, but anyway.

Well, after some more thought, I want to push back against removing .objs : Now, if S is a subgroupoid, and say I want to say that S is disconnected as a groupoid, it's going to look like S.objs.is_disconnected which just looks like it shouldn't even typecheck. What's the point of getting rid of .coe ?

Hi @bottine I've simplified some proofs over in my fork and pointed out most notable changes as comments here. Notice that I haven't merged your latest commit. Mostly I golf the proofs by simplifying just enough for defeq to work. I'm unable to prove map is a subgroupoid without using map.mem_arrows_iff, but I only need to use it once.

@alreadydone: OK, corrected following your requests/proposals! I was reluctant to drop the .coe because it's the "canonical" name as far as I'm aware, but anyway.

Well, after some more thought, I want to push back against removing .objs : Now, if S is a subgroupoid, and say I want to say that S is disconnected as a groupoid, it's going to look like S.objs.is_disconnected which just looks like it shouldn't even typecheck. What's the point of getting rid of .coe ?

By analogy with simple_graph.subgraph.coe, it's coe_subgroupoid that should be called coe. If you have groupoid.is_disconnected you should be able to write S.coe_subgroupoid.is_disconnected without problem.

OK, applied your suggestions. Thanks a lot!

Thanks!

maintainer merge

(or delegate and wait for CI, but note that queue is empty now)

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

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests