[Merged by Bors] - feat(category_theory/groupoid/subgroupoid): subgroupoids and basic properties

[bottine]

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

---

[alreadydone]

This is for now; will continue tomorrow.

[bottine]

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).

[alreadydone]

Thanks! I think I completed the review but I'll try to golf some proofs later.

[alreadydone]

I think you automatically get (≤) and everything down to the partial order instance. Instead of intros c d p you would do rintro ⟨c, d, p⟩ (or λ ⟨c, d, p⟩) which is almost as convenient as it's now. You can't write p ∈ S but should be able to write ⟨_, _, p⟩ ∈ S, and you may def mk {c d} (p : c ⟶ d) : Σ c d, c ⟶ d := ⟨c, d, p⟩ (or declare a notation) so that you can write mk p ∈ S. (A notation is better since mk isn't a good name, and sigma_hom_mk is too long ...)

[bottine]

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?

[alreadydone]

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.

[alreadydone]

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.

[alreadydone]

Some final edits and then it's ready to go!

[alreadydone]

Actually lemmas that unfold definitions like mem_iff usually shouldn't be simp lemmas. For le_iff, it's not clear the RHS is simpler than the LHS, so I suggest removing the @[simp] as well.

[bottine]

OK, applied your suggestions. Thanks a lot!

[alreadydone]

Thanks!

maintainer merge

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

[github-actions]

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

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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