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

[Merged by Bors] - feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series #14418

Closed
wants to merge 31 commits into from
Closed

[Merged by Bors] - feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series #14418

wants to merge 31 commits into from

Conversation

faenuccio
Copy link
Collaborator

@faenuccio faenuccio commented Jul 4, 2024 •
edited
Loading

Add some properties conneccting the $X$-adic valuation of a Laurent series to the vanishing of its coefficients, together with explicit values of the valuation of some basic Laurent series.

Co-authored-by: María Inés de Frutos-Fernández @mariainesdff

@faenuccio faenuccio added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Jul 4, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 4, 2024 •
edited
Loading

PR summary 2712d2d6dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ coeff_zero_of_lt_intValuation
+ coeff_zero_of_lt_valuation
+ eq_coeff_of_valuation_sub_lt
+ instance : Valued (LaurentSeries K) ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation
+ intValuation_le_iff_coeff_lt_eq_zero
+ mk_eq_mk'
+ val_le_one_iff_eq_coe
+ valuation_X_pow
+ valuation_eq_LaurentSeries_valuation
+ valuation_le_iff_coeff_lt_eq_zero
+ valuation_of_mk
+ valuation_single_zpow

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

@faenuccio faenuccio changed the title feat(RingTheory/LaurentSeries): add properties about the X-adic valuation on Laurent series feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series Jul 4, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 4, 2024
@ScottCarnahan
Copy link
Collaborator

Have you considered using AddVal from Mathlib.RingTheory.HahnSeries.Summable? It looks like the order API from Hahn series can make some of your proofs shorter.

@faenuccio
Copy link
Collaborator Author

Have you considered using AddVal from Mathlib.RingTheory.HahnSeries.Summable? It looks like the order API from Hahn series can make some of your proofs shorter.

Oh no, I had briefly had a look and then decided that since I was going for a MulVal they were unrelated. I will check it and try to simply my proofs - thanks!

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 5, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2024
@faenuccio
Copy link
Collaborator Author

faenuccio commented Jul 8, 2024 •
edited
Loading

Have you considered using AddVal from Mathlib.RingTheory.HahnSeries.Summable? It looks like the order API from Hahn series can make some of your proofs shorter.

@ScottCarnahan I have had a look but it seems to me that since most of the material about AddVal concerns... additive valuations, there is not much I can gain: I would at any rate need to set-up a dictionary. Or am I missing something, do you have explicit instances in mind where this could help?

@faenuccio faenuccio added the WIP Work in progress label Jul 11, 2024
@faenuccio faenuccio requested a review from ScottCarnahan July 11, 2024 08:40
@faenuccio faenuccio added WIP Work in progress and removed WIP Work in progress labels Jul 11, 2024
@faenuccio faenuccio removed the WIP Work in progress label Jul 17, 2024
jcommelin
jcommelin reviewed Jul 18, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

Mathlib/RingTheory/LaurentSeries.lean

theorem valuation_X_pow (s : ℕ) :
Valued.v (((X : K⟦X⟧) : LaurentSeries K) ^ s) = Multiplicative.ofAdd (-(s : ℤ)) := by
erw [map_pow,/- this, -/ ← one_mul (s : ℤ), ← neg_mul (1 : ℤ) s, Int.ofAdd_mul,
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
erw [map_pow,/- this, -/ ← one_mul (s : ℤ), ← neg_mul (1 : ℤ) s, Int.ofAdd_mul,
erw [map_pow, ← one_mul (s : ℤ), ← neg_mul (1 : ℤ) s, Int.ofAdd_mul,

Copy link
Member

Choose a reason for hiding this comment

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

Also, do you understand where exactly you need the e in erw? Is this pointing at a missing API lemma?

Mathlib/RingTheory/LaurentSeries.lean
n < d → coeff K n f = 0 := by
intro hnd
apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd
erw [← span_singleton_dvd_span_singleton_iff_dvd, ← Ideal.span_singleton_pow,
Copy link
Member

Choose a reason for hiding this comment

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

Same erw question.

Mathlib/RingTheory/LaurentSeries.lean
∀ n : ℕ, n < d → coeff K n f = 0 := by
have : PowerSeries.X ^ d ∣ f ↔ ∀ n : ℕ, n < d → (PowerSeries.coeff K n) f = 0 :=
⟨PowerSeries.X_pow_dvd_iff.mp, PowerSeries.X_pow_dvd_iff.mpr⟩
erw [← this, valuation_of_algebraMap (PowerSeries.idealX K) f, ←
Copy link
Member

Choose a reason for hiding this comment

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

Idem

Mathlib/RingTheory/LaurentSeries.lean
simp only [ne_eq, WithZero.coe_ne_zero, not_false_iff]

/- Two Laurent series whose difference has small valuation have the same coefficients for
small enough indeces. -/
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
small enough indeces. -/
small enough indices. -/

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jul 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 18, 2024
@faenuccio
feat(RingTheory/LaurentSeries): add properties of the X-adic valuatio…
03c6011 
…n on Laurent series (#14418)

Add some properties conneccting the $X$-adic valuation of a Laurent series to the vanishing of its coefficients, together with explicit values of the valuation of some basic Laurent series.

Co-authored-by: María Inés de Frutos-Fernández @mariainesdff 

- [x] depends on: #13064
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series [Merged by Bors] - feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series Jul 18, 2024
@mathlib-bors mathlib-bors bot closed this Jul 18, 2024
@mathlib-bors mathlib-bors bot deleted the fae_PR_valLaurentSeries branch July 18, 2024 08:27
@faenuccio faenuccio mentioned this pull request Jul 18, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Jul 18, 2024
@faenuccio
fix(RingTheory/LaurentSeries): fix two suggestions left (#14864)
84374bf 
We fix two suggestions from #14418 that were accidentally forgotten.
mathlib-bors bot pushed a commit that referenced this pull request Jul 18, 2024
@faenuccio
fix(RingTheory/LaurentSeries): fix two suggestions left (#14864)
28267f8 
We fix two suggestions from #14418 that were accidentally forgotten.
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@ScottCarnahan ScottCarnahan Awaiting requested review from ScottCarnahan

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@faenuccio @ScottCarnahan @leanprover-community-mathlib4-bot @jcommelin @kim-em