[Merged by Bors] - feat(RingTheory/LaurentSeries): add algebraEquiv by AntoineChambert-Loir · Pull Request #21004 · leanprover-community/mathlib4

AntoineChambert-Loir · 2025-01-23T21:57:44Z

Define an Algebra K RatFuncAdicCompl K instance on RatFuncAdicCompl K
and promote the already defined ring equivalences to algebra equivalences LaurentSeriesAlgEquiv : K⸨X⸩ ≃ₐ[K] RatFuncAdicCompl K and K⟦X⟧ ≃ₐ[K] (idealX K).adicCompletionIntegers (RatFunc K).

TODO : update docstring (on top of file)

github-actions · 2025-01-23T21:58:36Z

PR summary abb04b9cf5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ LaurentSeriesAlgEquiv
+ LaurentSeriesRingEquiv_def
+ LaurentSeriesRingEquiv_mem_valuationSubring
+ algebraMap_C_mem_adicCompletionIntegers
+ algebraMap_apply
+ instance : Algebra K ((idealX K).adicCompletionIntegers (RatFunc K))
+ instance : Algebra K (RatFuncAdicCompl K)
+ instance : Algebra K (v.adicCompletion K)
+ instance : IsScalarTower K ((idealX K).adicCompletionIntegers (RatFunc K))
+ powerSeriesAlgEquiv
+ powerSeriesEquivSubring_apply
+ powerSeriesEquivSubring_coe_apply
+ powerSeriesRingEquiv_coe_apply
- on

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

AntoineChambert-Loir · 2025-01-25T16:56:57Z

The algebra isom is created at the cost of a slight change in the definition of powerSeries_as_subring.

faenuccio

Thanks!

Mathlib/RingTheory/LaurentSeries.lean

faenuccio · 2025-01-27T09:07:17Z

maintainer delegate

github-actions · 2025-01-27T09:07:35Z

🚀 Pull request has been placed on the maintainer queue by faenuccio.

riccardobrasca · 2025-01-27T09:36:54Z

Thanks!

bors d+

mathlib-bors · 2025-01-27T09:36:57Z

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

AntoineChambert-Loir · 2025-01-27T10:06:05Z

bors r+

Define an `Algebra K RatFuncAdicCompl K` instance on `RatFuncAdicCompl K` and promote the already defined ring equivalences to algebra equivalences `LaurentSeriesAlgEquiv : K⸨X⸩ ≃ₐ[K] RatFuncAdicCompl K` and `K⟦X⟧ ≃ₐ[K] (idealX K).adicCompletionIntegers (RatFunc K)`. TODO : update docstring (on top of file)

mathlib-bors · 2025-01-27T10:16:33Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...

* polynomial-sequences: (308 commits) Use the lemma we already added. Minor reordering. This is true even for the trivial ring. Also add the lt versions and the other inj lemma. Also add the basis ne versions. This seems also like it should be simp. Back to sorry free. And the natDegree version. feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) ...

feat(RingTheory/LaurentSeries): add algebraEquiv

e0e7cce

AntoineChambert-Loir requested a review from faenuccio January 23, 2025 21:58

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 23, 2025

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 23, 2025

AntoineChambert-Loir added the WIP Work in progress label Jan 23, 2025

AntoineChambert-Loir added 2 commits January 24, 2025 00:45

progress on powerSeries

9c294d5

create algebra isoms

b9deef4

AntoineChambert-Loir added 2 commits January 25, 2025 20:48

update docstring

8030146

remove import

0b62433

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 25, 2025

AntoineChambert-Loir removed the WIP Work in progress label Jan 25, 2025

faenuccio reviewed Jan 27, 2025

View reviewed changes

Mathlib/RingTheory/LaurentSeries.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/LaurentSeries.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/LaurentSeries.lean Outdated Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 27, 2025

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 27, 2025

update after comments

abb04b9

mathlib-bors bot changed the title ~~feat(RingTheory/LaurentSeries): add algebraEquiv~~ [Merged by Bors] - feat(RingTheory/LaurentSeries): add algebraEquiv Jan 27, 2025

mathlib-bors bot closed this Jan 27, 2025

mathlib-bors bot deleted the ACL/LaurentAlgEquiv branch January 27, 2025 10:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory/LaurentSeries): add algebraEquiv#21004

[Merged by Bors] - feat(RingTheory/LaurentSeries): add algebraEquiv#21004
AntoineChambert-Loir wants to merge 6 commits intomasterfrom
ACL/LaurentAlgEquiv

AntoineChambert-Loir commented Jan 23, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 23, 2025 •

edited

Loading

Declarations diff

Uh oh!

AntoineChambert-Loir commented Jan 25, 2025

Uh oh!

faenuccio left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio commented Jan 27, 2025

Uh oh!

github-actions bot commented Jan 27, 2025

Uh oh!

riccardobrasca commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

AntoineChambert-Loir commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

AntoineChambert-Loir commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

TODO : update docstring (on top of file)

Uh oh!

github-actions bot commented Jan 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary abb04b9cf5

Import changes for modified files

Declarations diff

Uh oh!

AntoineChambert-Loir commented Jan 25, 2025

Uh oh!

faenuccio left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

faenuccio commented Jan 27, 2025

Uh oh!

github-actions bot commented Jan 27, 2025

Uh oh!

riccardobrasca commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

AntoineChambert-Loir commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

AntoineChambert-Loir commented Jan 23, 2025 •

edited

Loading

github-actions bot commented Jan 23, 2025 •

edited

Loading