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

feat(algebra/magma_algebra): define the magma algebra associated to a magma and a semiring of coefficients #6571

Closed
wants to merge 16 commits into from
Closed

feat(algebra/magma_algebra): define the magma algebra associated to a magma and a semiring of coefficients #6571

wants to merge 16 commits into from

Conversation

ocfnash
Copy link
Collaborator

@ocfnash ocfnash commented Mar 7, 2021 •
edited by github-actions bot

@ocfnash ocfnash added WIP Work in progress RFC Request for comment labels Mar 7, 2021
@ocfnash ocfnash mentioned this pull request Mar 7, 2021
Closed
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 8, 2021
@github-actions github-actions bot added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Mar 9, 2021
@github-actions
Copy link

github-actions bot commented Mar 9, 2021

⏳ Alright! Looks like we need to wait for some dependencies:

💡 Don't worry, I will continue watching the list above and keep this comment updated. To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@ocfnash ocfnash force-pushed the magma_algebra branch 3 times, most recently from be5e7a9 to 08440a3 Compare March 12, 2021 16:46
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 12, 2021
@ocfnash
feat(algebra/non_associative/basic): define non-associative algebras
b7a0188
@ocfnash
Add na_algebra.to_algebra
91eec2d
@ocfnash
Remove simp attributes to appease linter
649df65
@ocfnash
Factor out mul_hom.inverse
b67f296
@ocfnash
Experiment with Eric's "open the floodgates" suggestion
39cec7e 
Despite initial reluctance, I am beginning to be persuaded. The
names are not serious suggestions, especially as if this works, what
we are really defining is non-unital algebras since we can make the
existing `algebra` definition allow for non-associativity for free.

For now I just want to see whether this compiles.
@ocfnash
Fix build failure 1 / ?
43d04f5
@ocfnash
Change semiring ancestors.
3f97369 
_Probably_ a more useful set of ancestors.
@ocfnash
Revert semiring ancestors change.
185b373 
For reasons I haven't tried to understand this breaks the proof
of `multiset.prod_map_add`. Having seen this, I think it's best
to revert this since there's already plenty of surface area in
these changes to break things.
@ocfnash
Fix long line
4ce16c5
@ocfnash
Fix build failure 3 / ?
96b7430 
If this doesn't work, I think I'll give up on inserting `mul_one_class` /
`add_zero_class` into the `monoid` / `add_monoid` definitions.
@ocfnash
Fix build failure 4 / ?
970a79d
@ocfnash
Revert changes to monoid / add_monoid ancestors
383d5a0 
The most recent build failure (topology/locally_constant/algebra.lean:52:73)
has persuaded me to abandon this part of the work. It could be done but it's
too much of a diversion / time sink in what is already a tangent.
@ocfnash
Improve naming
16074da
@ocfnash
Move + rename file
accef2a
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 12, 2021
@ocfnash ocfnash removed the RFC Request for comment label Mar 12, 2021
@ocfnash ocfnash added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Mar 12, 2021
@ocfnash ocfnash mentioned this pull request Mar 17, 2021
Closed
2 tasks
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 26, 2021
@eric-wieser
Copy link
Member

Now that we have monoid_algebra.non_unital_non_assoc_semiring, is this PR needed? Perhaps it should be revived as simply an update to the docstring for monoid_algebra?

eric-wieser
eric-wieser reviewed Jun 8, 2021
View reviewed changes
src/algebra/magma_algebra.lean
Comment on lines +149 to +150
/-- The embedding of a magma into its magma algebra. -/
def of : mul_hom M (magma_algebra R M) :=
Copy link
Member

Choose a reason for hiding this comment

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

I guess this statement and lift below are currently not stated for monoid_algebra, but we could probably add them.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I think it is worth adding of and lift here to monoid_algebra. I claim this justifies the creation of:

set_option old_structure_cmd true

structure linear_mul_hom (R : Type u) (A : Type v) (B : Type w)
  [semiring R] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B]
  [module R A] [module R B] extends A →ₗ[R] B, mul_hom A B

By using module instead of algebra in this definition, we avoid the algebra issue and lose nothing really.

Thoughts?

Copy link
Member

Choose a reason for hiding this comment

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

@riccardobrasca actually could have done with an object of this type very recently, for linear_map.fst and linear_map.snd.

I think non_unital_alg_hom might be a better name for that structure, and it suggests we should probably have non_unital_ring_hom too.

Copy link
Member

Choose a reason for hiding this comment

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

Adding a new bundled hom comes with lots of boilerplate unfortunately.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I'll give it a go!

Copy link
Member

Choose a reason for hiding this comment

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

Oh, yes, I proved needed exactly this for linear_map.inl and linear_map.snd!

@ocfnash
Copy link
Collaborator Author

ocfnash commented Jun 8, 2021

Now that we have monoid_algebra.non_unital_non_assoc_semiring, is this PR needed? Perhaps it should be revived as simply an update to the docstring for monoid_algebra?

I'm going to settle its fate today or tomorrow. I had a quick look this morning and I think some of the constructions in monoid_algebra still need to be generalised a little to capture everything that is here.

@ocfnash ocfnash mentioned this pull request Jun 14, 2021
Closed
1 task
@ocfnash
Copy link
Collaborator Author

ocfnash commented Jun 14, 2021

Closing in favour of #7932

@ocfnash ocfnash closed this Jun 14, 2021
@ocfnash ocfnash deleted the magma_algebra branch June 14, 2021 13:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. merge-conflict Please `git merge origin/master` then a bot will remove this label.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@ocfnash @eric-wieser @jcommelin @riccardobrasca