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(ring_theory/power_series): order #1292

Merged
merged 65 commits into from Sep 30, 2019
Merged

feat(ring_theory/power_series): order #1292

merged 65 commits into from Sep 30, 2019

Conversation

jcommelin
Copy link
Member

No description provided.

@jcommelin
First start on power_series
12acd3c
@jcommelin
Innocent changes
8b7eb31
@jcommelin
Almost a comm_semiring
146405a
@jcommelin
Defined hom from mv_polynomial to mv_power_series; sorrys remain
0f01f4a
@jcommelin
Attempt that seem to go nowhere
eaa538a
@jcommelin
Working on coeff_mul for polynomials
2bc7b64
@jcommelin
Small progress
d26b939
@jcommelin
Finish mv_polynomial.coeff_mul
bfde6d7
@jcommelin
Cleaner proof of mv_polynomial.coeff_mul
907584d
@jcommelin
Fix build
be0b909
@jcommelin
WIP
d4b3672
@jcommelin
Finish proof of mul_assoc
0afb898
@jcommelin
WIP
9f3160a
@jcommelin
Merge branch 'lean-3.4.2' into power-series
99dd853
@jcommelin
Golfing coeff_mul
4ee9f0c
@jcommelin
WIP
dac1470
@jcommelin
Crazy wf is crazy
81195b1
@jcommelin
mv_power_series over local ring is local
faf92d8
@jcommelin
WIP
7a18a28
@jcommelin
Add empty line
3bba2bf
@jcommelin
wip
10169aa
@jcommelin
wip
f30a689
@jcommelin
WIP
aeae8ae
@jcommelin
WIP
a1c7cb5
@jcommelin
WIP
be25bd8
@jcommelin
Add header comments
a3d7690
@jcommelin
WIP
70744fb
@jcommelin
WIP
332840d
@jcommelin
Merge branch 'lean-3.4.2' into power-series
095a688
@jcommelin
Fix finsupp build
21b465b
@PatrickMassot
Copy link
Member

I see many lemmas whose name contain "coe" but are not marked for norm_cast use. Could you fix that? Also, is it normal that this PR doesn't update the header documentation? In this documentation, you describe the role of alpha, could you describe the role of sigma?

@jcommelin
Copy link
Member Author

I will do it when I return from holidays (two weeks).

@jcommelin
Copy link
Member Author

@PatrickMassot I have added elim_cast attributes. I have updated the documentation.

@ChrisHughes24 I think that moving to bundled homs is already going to be quite a refactor. Because the algebraic structure on mv_power_series is defined in terms of coeff and C. So at the time of definition of coeff and C, it is impossible to show that they are add_homs etc.

So I would have to refactor the file in order to define coeff and C after the algebraic structure has been set up.

The example you give is also interesting. coeff 0 is a (semi)ring hom. But coeff n for general n is only a linear map. I'm not sure how to handle this in a bundled setting...

@ChrisHughes24
Copy link
Member

@PatrickMassot I have added elim_cast attributes. I have updated the documentation.

@ChrisHughes24 I think that moving to bundled homs is already going to be quite a refactor. Because the algebraic structure on mv_power_series is defined in terms of coeff and C. So at the time of definition of coeff and C, it is impossible to show that they are add_homs etc.

So I would have to refactor the file in order to define coeff and C after the algebraic structure has been set up.

The example you give is also interesting. coeff 0 is a (semi)ring hom. But coeff n for general n is only a linear map. I'm not sure how to handle this in a bundled setting...

I didn't really pay attention to that. I think we do want an is_ring_hom predicate as well for situations like this. Doing algebraic closure, I actually used the is_ring_hom predicate to define a preorder.

@semorrison
Copy link
Collaborator

Shall we merge this after fixing the conflict? It looks good to me.

@ChrisHughes24
Copy link
Member

I made a Zulip post about how to do the bundled hom refactor, and whether or not to merge PRs that use is_ring_hom. I'd rather here the community's views on this before merging this PR.

@jcommelin
Copy link
Member Author

I've bundled the homs.

@jcommelin
Copy link
Member Author

Travis was a bit unhappy, but the build should now be fixed.

@jcommelin jcommelin added the awaiting-review The author would like community review of the PR label Sep 25, 2019
@ChrisHughes24 ChrisHughes24 added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Sep 26, 2019
jcommelin
jcommelin commented Sep 26, 2019
View reviewed changes
src/ring_theory/power_series.lean Show resolved Hide resolved
src/ring_theory/power_series.lean Outdated Show resolved Hide resolved
src/ring_theory/power_series.lean Outdated Show resolved Hide resolved
@mergify mergify bot merged commit c6fab42 into master Sep 30, 2019
@mergify mergify bot deleted the power-series-order branch September 30, 2019 08:56
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@jcommelin @anrddh
feat(ring_theory/power_series): order (leanprover-community#1292)
b72f232 
* First start on power_series

* Innocent changes

* Almost a comm_semiring

* Defined hom from mv_polynomial to mv_power_series; sorrys remain

* Attempt that seem to go nowhere

* Working on coeff_mul for polynomials

* Small progress

* Finish mv_polynomial.coeff_mul

* Cleaner proof of mv_polynomial.coeff_mul

* Fix build

* WIP

* Finish proof of mul_assoc

* WIP

* Golfing coeff_mul

* WIP

* Crazy wf is crazy

* mv_power_series over local ring is local

* WIP

* Add empty line

* wip

* wip

* WIP

* WIP

* WIP

* Add header comments

* WIP

* WIP

* Fix finsupp build

* Fix build, hopefully

* Fix build: ideals

* More docs

* Update src/data/power_series.lean

Fix typo.

* Fix build -- bump instance search depth

* Make changes according to some of the review comments

* Use 'formal' in the names

* Use 'protected' in more places, remove '@simp's

* Make 'inv_eq_zero' an iff

* Generalize to non-commutative scalars

* Order of a power series

* Start on formal Laurent series

* WIP

* Remove file. It's for another PR.

* Add stuff about order

* Remove old file

* Basics on order of power series

* Lots of stuff

* Move stuff on kernels

* Move stuff on ker to the right place

* Fix build

* Add elim_cast attributes, update documentation

* Bundle homs

* Fix build

* Remove duplicate trunc_C

* Fix build
@YaelDillies YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 9, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ChrisHughes24 ChrisHughes24 ChrisHughes24 approved these changes

Assignees

@ChrisHughes24 ChrisHughes24

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@jcommelin @PatrickMassot @ChrisHughes24 @semorrison @YaelDillies