Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Basic group theory #427

Merged
merged 9 commits into from
Sep 4, 2024
Merged

Basic group theory #427

merged 9 commits into from
Sep 4, 2024

Conversation

ncfavier
Copy link
Member

Description

  • (amalgamated) free products of groups, making them finitely cocomplete
  • semidirect products of abstract and concrete groups, some fundamental group actions
  • cyclic groups, $\mathbb{Z}/n\mathbb{Z}$
  • (generalised) dihedral groups
  • explicit construction of finite products of concrete groups
  • order of an element, torsion groups, torsion-free groups

Checklist

Before submitting a merge request, please check the items below:

  • I've read the contributing guidelines.
  • The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
  • All new code blocks have "agda" as their language.

@Lavenza
Copy link
Member

Lavenza commented Aug 27, 2024

Pull request preview

@ncfavier
def: semidirect product of groups
755d602
@ncfavier
def: cyclic groups
e0e9730
@ncfavier
def: dihedral groups
59e14d5
@ncfavier
def: finite limits of concrete groups
2d49ac7
@ncfavier
chore: flip ∘Iso and ∘ni
131224b 
We try to stick to the convention that `∘` means the classical
composition order while `∙` means diagrammatic order.
@ncfavier
def: order and torsion
ee0a8b2
@ncfavier
chore: only lift ℤ and ℤ/n as needed
2108816 
Having ℤ unlifted means that we can use the category reasoning
combinators to prove identities of the integers without having to
sprinkle lifts and lowers everywhere.
@ncfavier ncfavier mentioned this pull request Aug 27, 2024
Open
@ncfavier ncfavier merged commit a122947 into main Sep 4, 2024
5 checks passed
@ncfavier ncfavier deleted the ncf/groups branch September 4, 2024 13:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@plt-amy plt-amy plt-amy approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@ncfavier @Lavenza @plt-amy