Skip to content

[Merged by Bors] - feat: pushouts of monoids#8061

Closed
ChrisHughes24 wants to merge 150 commits intomasterfrom
PushoutMonoidChris
Closed

[Merged by Bors] - feat: pushouts of monoids#8061
ChrisHughes24 wants to merge 150 commits intomasterfrom
PushoutMonoidChris

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Oct 31, 2023

Open in Gitpod

ChrisHughes24 and others added 30 commits August 23, 2023 14:53
@ChrisHughes24
just the universal property
29e7c4c
@ChrisHughes24
move the file somewhere sensible
177d477
@ChrisHughes24
define smulWord
b8277df
@ChrisHughes24
some stuff
c93d0af
@ChrisHughes24
define rcons
00c436b
@ChrisHughes24
almost defining the action
6fbbfb5
@ChrisHughes24
finally define rcons
94c30fb
@ChrisHughes24
a little more work
e87ba53
@ChrisHughes24
decidability stuff
5310a6a
@ChrisHughes24
Everything is wrong
9c2b430
@ChrisHughes24
back to using default
8010f61
@ChrisHughes24
define the actual action
e759d05
@ChrisHughes24
small progress
e938cdc
@ChrisHughes24
a bit more progress
4e12816
@ChrisHughes24
chore(Group): protected things like Semigroup.mul_assoc
62abd66
@ChrisHughes24
feat: List.head_mem
6ef9c96
@ChrisHughes24
Merge branch 'headMemch' into AmalgamatedProductChris
38bf215
@ChrisHughes24
more progress
ecd15d5
@ChrisHughes24
Merge branch 'protectStuffInGroup' into AmalgamatedProductChris
ffdab01
@ChrisHughes24
mul_def
0ba17d6
@ChrisHughes24
stuff
b603b00
@ChrisHughes24
prove that of is injective
8a0c8b5
@ChrisHughes24
small golf
27ee2e4
@ChrisHughes24
more renaming and tidying
0c568aa
@ChrisHughes24
slight simplification
bbc3b81
@ChrisHughes24
remove newline
6ea5a60
@ChrisHughes24
Merge branch 'master' into AmalgamatedProductChris
4656f45
@ChrisHughes24
feat: Binary coproducts of Monoids
2178227
@ChrisHughes24
update Mathlib.lean
d6d7e7c
@ChrisHughes24
Merge branch 'BinaryFreeProdChris' into AmalgamatedProductChris
eedc2fa
@ChrisHughes24 ChrisHughes24 changed the title feat: Pushouts of monoid feat: pushouts of monoids Oct 31, 2023
@ChrisHughes24 ChrisHughes24 mentioned this pull request Oct 31, 2023
Closed
9 tasks
riccardobrasca
riccardobrasca approved these changes Oct 31, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add the universal property in some form? It is essentially already there with lift and hom_ext_nonempty, but it would be nice to have bijection from maps from the pushout and maps such that...

Mathlib/GroupTheory/PushoutI.lean Outdated
- `Monoid.PushoutI.of`: the map from each Monoid in the family to the pushout
- `Monoid.PushoutI.lift`: the universal property used to define homomorphisms out of the pushout.

- `Monoid.PushoutI.NormalWord`: a normal form for words in the pushout
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca Oct 31, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is in the second part.

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 31, 2023

Can you add the universal property in some form? It is essentially already there with lift and hom_ext_nonempty, but it would be nice to have bijection from maps from the pushout and maps such that...

I added it, but I never end up using these things. The full universal property is given by of, base, of_comp_eq_base, liftandhom_ext`.

@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Oct 31, 2023

Can you add the universal property in some form? It is essentially already there with lift and hom_ext_nonempty, but it would be nice to have bijection from maps from the pushout and maps such that...

I added it, but I never end up using these things. The full universal property is given by of, base, of_comp_eq_base, liftandhom_ext`.

I agree that in practice one uses the explicit results, but I think it's nice to have it, since it really packages the universal property. Can you just add a TODO that says we want to add HasPushout (or whatever it is called) to the relevant categories? Thanks!

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 31, 2023

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Oct 31, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Oct 31, 2023

Can you add the universal property in some form? It is essentially already there with lift and hom_ext_nonempty, but it would be nice to have bijection from maps from the pushout and maps such that...

I added it, but I never end up using these things. The full universal property is given by of, base, of_comp_eq_base, liftandhom_ext`.

I agree that in practice one uses the explicit results, but I think it's nice to have it, since it really packages the universal property. Can you just add a TODO that says we want to add HasPushout (or whatever it is called) to the relevant categories? Thanks!

bors d+

We already know that both Monoids and Groups have all colimits
bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 31, 2023
bors bot pushed a commit that referenced this pull request Oct 31, 2023
@ChrisHughes24
feat: pushouts of monoids (#8061)
0c484a5 
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
@bors
Copy link
Copy Markdown

bors bot commented Oct 31, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: pushouts of monoids [Merged by Bors] - feat: pushouts of monoids Oct 31, 2023
@bors bors bot closed this Oct 31, 2023
@bors bors bot deleted the PushoutMonoidChris branch October 31, 2023 15:03
fgdorais pushed a commit that referenced this pull request Nov 1, 2023
@ChrisHughes24 @fgdorais
feat: pushouts of monoids (#8061)
e71a0e9 
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees

@riccardobrasca riccardobrasca

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ChrisHughes24 @riccardobrasca