[Merged by Bors] - feat(InfinitePlace/Ramification): `LiesOver` class for absolute values and derived results on infinite places by smmercuri · Pull Request #27978 · leanprover-community/mathlib4

smmercuri · 2025-08-05T10:56:11Z

If w is an absolute value on L/K and v is an absolute value of K then w.LiesOver v is the class defining the property that v is the restriction of w to K.

This PR continues the work from #24881.

Original PR: #24881

depends on: [Merged by Bors] - feat: predicates for extensions of complex embeddings #27977

…initePlaceExtension

…mmercuri/InfinitePlaceExtension

github-actions · 2025-08-05T10:57:23Z

PR summary 3a0b00eed1

Import changes exceeding 2%

%	File
+2.04%	`Mathlib.Analysis.Normed.Ring.WithAbs`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Ring.WithAbs	1227	1252	+25 (+2.04%)
Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification	2626	2627	+1 (+0.04%)

Import changes for all files

Files	Import difference
12 files `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal` `Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification` `Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex`	1
`Mathlib.Analysis.Normed.Ring.WithAbs`	25

Declarations diff

+ LiesOver
+ LiesOver.comp_eq
+ comap_eq
+ embedding_comp_eq_or_conjugate_embedding_comp_eq
+ isComplex_of_isComplex_under
+ isReal_of_isReal_over
+ mk_embedding_comp

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).

mathlib4-dependent-issues-bot · 2025-09-19T09:36:09Z

This PR/issue depends on:

~~[Merged by Bors] - feat: predicates for extensions of complex embeddings #27977~~
By Dependent Issues (🤖). Happy coding!

mathlib4-merge-conflict-bot · 2025-09-19T10:08:12Z

This pull request has conflicts, please merge master and resolve them.

…mmercuri/InfinitePlaceExtension

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

smmercuri · 2025-10-15T09:33:08Z

I've replaced the subtype of places above v : InfinitePlace K (previously InfinitePlace.Extension) with a class LiesOver defining the same property, which makes things a lot easier than working with subtypes!

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

MichaelStollBayreuth · 2025-10-16T18:57:09Z

I've replaced the subtype of places above v : InfinitePlace K (previously InfinitePlace.Extension) with a class LiesOver defining the same property, which makes things a lot easier than working with subtypes!

I think it would make sense to have this more generally for absolute values.

smmercuri · 2025-10-17T09:57:50Z

I've replaced the subtype of places above v : InfinitePlace K (previously InfinitePlace.Extension) with a class LiesOver defining the same property, which makes things a lot easier than working with subtypes!

I think it would make sense to have this more generally for absolute values.

Yes good idea! However it was not easy to find a good place for the definition, because of the current location of AbsoluteValue.comp. I placed it in Ring/WithAbs.lean since ultimately LiesOver leads to connections between respective topologies. But probably that has led to a large import

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

MichaelStollBayreuth · 2025-10-28T13:05:29Z

CI fails with some cache problem. I'd suggest to merge master (I also noticed that it seemed to build all of Mathlib) and try again.

…mmercuri/InfinitePlaceExtension

MichaelStollBayreuth · 2025-10-28T20:51:25Z

LGTM now.
maintainer merge

github-actions · 2025-10-28T20:51:41Z

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

riccardobrasca · 2025-10-29T11:45:15Z

Thanks!

bors merge

…s and derived results on infinite places (#27978) If `w` is an absolute value on `L/K` and `v` is an absolute value of `K` then `w.LiesOver v` is the class defining the property that `v` is the restriction of `w` to `K`. This PR continues the work from #24881. Original PR: #24881

mathlib-bors · 2025-10-29T12:31:56Z

Pull request successfully merged into master.

Build succeeded:

…s and derived results on infinite places (leanprover-community#27978) If `w` is an absolute value on `L/K` and `v` is an absolute value of `K` then `w.LiesOver v` is the class defining the property that `v` is the restriction of `w` to `K`. This PR continues the work from leanprover-community#24881. Original PR: leanprover-community#24881

Salvatore Mercuri added 4 commits May 14, 2025 07:40

predicates for extensions of complex embeddings

1e5008c

InfinitePlace.Extension API

8cd5e33

Merge branch 'smmercuri/ComplexEmbeddingExtension' into smmercuri/Inf…

5e4705b

…initePlaceExtension

Merge branch 'master' of https://github.com/smmercuri/mathlib4 into s…

dbe4145

…mmercuri/InfinitePlaceExtension

smmercuri mentioned this pull request Aug 5, 2025

feat: InfinitePlace.Extension API for extensions of infinite places. #24881

Closed

1 task

github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Aug 5, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 5, 2025

smmercuri mentioned this pull request Aug 5, 2025

feat: dimensions of completions at infinite place extensions #27980

Open

7 tasks

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 19, 2025

mathlib4-merge-conflict-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 Sep 19, 2025

Merge branch 'master' of https://github.com/smmercuri/mathlib4 into s…

2395098

…mmercuri/InfinitePlaceExtension

github-actions 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 Sep 24, 2025

smmercuri added 2 commits September 24, 2025 10:23

Update infinite place extension API

3e6b674

golf

fa1feae

smmercuri mentioned this pull request Sep 24, 2025

[Merged by Bors] - feat(InfinitePlace/Completion): embeddings of w.Completion factor through embeddings of v.Completion when w lies over v #29942

Closed

4 tasks

smmercuri added 2 commits September 24, 2025 15:25

Extension.abs

98c5ed0

Add docstring for Extension.abs

36bdcdf

smmercuri added the FLT part of the ongoing formalization of Fermat's Last Theorem label Sep 24, 2025

leanprover-community-bot-assistant assigned MichaelStollBayreuth Oct 2, 2025

MichaelStollBayreuth reviewed Oct 11, 2025

View reviewed changes

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 11, 2025

smmercuri mentioned this pull request Oct 15, 2025

feat: NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank #30551

Open

9 tasks

Replace Extension type with LiesOver class

f0ba7d6

smmercuri changed the title ~~feat: InfinitePlace.Extension API for extensions of infinite places.~~ feat(InfinitePlace/Ramification): LiesOver class for infinite places Oct 15, 2025

MichaelStollBayreuth reviewed Oct 16, 2025

View reviewed changes

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean Show resolved Hide resolved

MichaelStollBayreuth reviewed Oct 16, 2025

View reviewed changes

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean Outdated Show resolved Hide resolved

Abstract LiesOver to AbsoluteValue

47fad31

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

smmercuri changed the title ~~feat(InfinitePlace/Ramification): LiesOver class for infinite places~~ feat(InfinitePlace/Ramification): LiesOver class for absolute values and derived results on infinite places Oct 17, 2025

smmercuri removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 20, 2025

MichaelStollBayreuth reviewed Oct 28, 2025

View reviewed changes

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth reviewed Oct 28, 2025

View reviewed changes

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 28, 2025

smmercuri and others added 2 commits October 28, 2025 11:33

Apply suggestion from @MichaelStollBayreuth

402a458

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Update Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

7d84461

Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

smmercuri removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 28, 2025

Merge branch 'master' of https://github.com/smmercuri/mathlib4 into s…

9725781

…mmercuri/InfinitePlaceExtension

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 28, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Oct 29, 2025

mathlib-bors bot changed the title ~~feat(InfinitePlace/Ramification): LiesOver class for absolute values and derived results on infinite places~~ [Merged by Bors] - feat(InfinitePlace/Ramification): LiesOver class for absolute values and derived results on infinite places Oct 29, 2025

mathlib-bors bot closed this Oct 29, 2025

Conversation

smmercuri commented Aug 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 3a0b00eed1

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Sep 19, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Sep 19, 2025

Uh oh!

Uh oh!

smmercuri commented Oct 15, 2025

Uh oh!

Uh oh!

Uh oh!

MichaelStollBayreuth commented Oct 16, 2025

Uh oh!

smmercuri commented Oct 17, 2025

Uh oh!

Uh oh!

Uh oh!

MichaelStollBayreuth commented Oct 28, 2025

Uh oh!

MichaelStollBayreuth commented Oct 28, 2025

Uh oh!

github-actions bot commented Oct 28, 2025

Uh oh!

riccardobrasca commented Oct 29, 2025

Uh oh!

mathlib-bors bot commented Oct 29, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

smmercuri commented Aug 5, 2025 •

edited

Loading

github-actions bot commented Aug 5, 2025 •

edited

Loading