Skip to content

Add missing proofs for FinGrp, FS, Met#217

Merged
ScriptRaccoon merged 5 commits into
mainfrom
fin-grp-cocongruences
May 29, 2026
Merged

Add missing proofs for FinGrp, FS, Met#217
ScriptRaccoon merged 5 commits into
mainfrom
fin-grp-cocongruences

Conversation

@ScriptRaccoon
Copy link
Copy Markdown
Owner

@ScriptRaccoon ScriptRaccoon commented May 28, 2026 •
edited
Loading

This PR

  • adds a proof that FinGrp has effective cocongruences (proven in https://mathoverflow.net/questions/511516)
  • adds a proof that FS is a generalized variety
  • greatly simplifies the proof that FS is finitely accessible
  • adds a proof that PMet, Met and Met∞ are not regular
  • unknown (category, property)-pairs before this PR: 114
  • unknown (category, property)-pairs after this PR: 108

@ScriptRaccoon ScriptRaccoon mentioned this pull request May 28, 2026
Open
@ScriptRaccoon ScriptRaccoon changed the title FinGrp does have effective cocongruences Add missing proofs for FinGrp and other categories (WIP) May 28, 2026
@ScriptRaccoon ScriptRaccoon force-pushed the fin-grp-cocongruences branch from ca5be00 to 8970143 Compare May 28, 2026 16:17
@ScriptRaccoon ScriptRaccoon changed the title Add missing proofs for FinGrp and other categories (WIP) Add missing proofs for FinGrp and FS May 28, 2026
@ScriptRaccoon ScriptRaccoon force-pushed the fin-grp-cocongruences branch from 8970143 to 68cef69 Compare May 28, 2026 16:25
dschepler
dschepler reviewed May 28, 2026
View reviewed changes
Comment thread content/sifted-colimits-in-groupoids.md Outdated
@dschepler
Copy link
Copy Markdown
Contributor

dschepler commented May 28, 2026

Other than the one minor reservation I have about the terminology "eventually constant", this looks good to me.

@ScriptRaccoon ScriptRaccoon changed the title Add missing proofs for FinGrp and FS Add missing proofs for FinGrp, FS, Met May 28, 2026
@ScriptRaccoon ScriptRaccoon force-pushed the fin-grp-cocongruences branch from a77bbf4 to a905a84 Compare May 29, 2026 07:01
@ScriptRaccoon ScriptRaccoon merged commit 2945954 into main May 29, 2026
1 check passed
@ScriptRaccoon ScriptRaccoon deleted the fin-grp-cocongruences branch May 29, 2026 07:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@dschepler dschepler dschepler left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

data

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ScriptRaccoon @dschepler