[Merged by Bors] - fix: Fix FundamentalGroupoid being reducible.
#8257
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
| @@ -205,7 +206,7 @@ | |||
| inv_hom_id := by | |||
| change (projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B = 𝟭 _ | |||
| apply CategoryTheory.Functor.hext | |||
| · intros; apply Prod.ext <;> simp <;> rfl | |||
| · intros; apply FundamentalGroupoid.ext ; apply Prod.ext <;> simp <;> rfl | |||
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
| · intros; apply FundamentalGroupoid.ext ; apply Prod.ext <;> simp <;> rfl | |
| · intros; apply FundamentalGroupoid.ext; apply Prod.ext <;> simp <;> rfl |
…ommunity/mathlib4 into AT-fundamental-groupoid-fix
| rw [simply_connected_def, equiv_punit_iff_unique] | ||
| refine ⟨fun ⟨⟨x⟩,h⟩ => ⟨⟨x.as⟩, fun x y => h _ _⟩, | ||
| fun ⟨⟨x⟩,h⟩ => ⟨⟨⟨x⟩⟩, fun x y => h _ _⟩ ⟩ |
There was a problem hiding this comment.
Is there a missing lemma here? Maybe Nonempty (FundamentalGroupoid X) \iff Nonempty X (and similarly for Subsingleton and Nontrivial)
There was a problem hiding this comment.
(the trick is to build the equiv and then all these results are there by dot notation)
There was a problem hiding this comment.
Probably. I didn't think too much when I made these changes :) I'll fix this soon.
There was a problem hiding this comment.
I added equiv and some related lemmas and instances. I don't want this PR to expand too far beyond the original fix, so I would prefer to leave anything further which is not directly related to a future PR.
|
I noticed this a while ago and have another design to fix the problem without changing FundamentalGroupoid to a one-field structure, but I haven't fixed all errors. The ideas is that Lean can't quite identify the coeSort of Did you find this because you want to do something with fundamental groupoids, or by |
adamtopaz
added
the
awaiting-review
|
bors d=@alreadydone |
|
✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
Instead it is now the opposite -- a structure with a single field. [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Groupoid.2EtoCategory/near/400820106) Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
|
Build failed (retrying...): |
Instead it is now the opposite -- a structure with a single field. [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Groupoid.2EtoCategory/near/400820106) Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
FundamentalGroupoid being reducible.FundamentalGroupoid being reducible.
Instead it is now the opposite -- a structure with a single field. [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Groupoid.2EtoCategory/near/400820106) Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
Instead it is now the opposite -- a structure with a single field.
zulip discussion