[Merged by Bors] - feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` lies over `v` by smmercuri · Pull Request #29942 · leanprover-community/mathlib4

smmercuri · 2025-09-24T13:05:08Z

The class ComplexEmbedding.LiesOver ψ φ formalises the property that the complex field embedding φ : L →+* ℂ restricted to K gives ψ : K →+* ℂ, whenever Algebra K L.

If w : InfinitePlace L and v : InfinitePlace K are such that we have Algebra v.Completion w.Completion, then extensionEmbedding w : L →+* ℂ restricted to K gives extensionEmbedding v : K →+* ℂ.

To avoid diamonds arising from propeq instances when K = L we do not construct the global instance Algebra v.Completion w.Completion from Algebra K L, but assume it instead. It is then required to assume the following compatibility assumptions for the main result of this PR to be true:

IsScalarTower (WithAbs v.1) v.Completion w.Completion
ContinuousSMul v.Completion w.Completion

…initePlaceExtension

…mmercuri/InfinitePlaceExtension

…aming-WithAbs

github-actions · 2025-09-24T13:06:15Z

PR summary 7c0aa26a8b

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.NumberField.InfinitePlace.Completion	2695	2696	+1 (+0.04%)

Import changes for all files

Files	Import difference
3 files `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.InfiniteAdeleRing` `Mathlib.NumberTheory.NumberField.InfinitePlace.Completion`	1

Declarations diff

+ LiesOver
+ algebraMap_coe
+ embedding_liesOver_of_isReal
+ extensionEmbeddingOfIsReal_apply
+ extensionEmbedding_liesOver_of_isReal
+ isometry_algebraMap
+ liesOver_conjugate_extensionEmbedding
+ liesOver_extensionEmbedding

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

Increase in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
10051	2	backward.isDefEq

Current commit fb6b0f5bbb
Reference commit 7c0aa26a8b

You can run this locally as

./scripts/reporting/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).

…xtensionEmbeddingAlgebraMap

mathlib-dependent-issues · 2026-03-02T18:05:17Z

This PR/issue depends on:

~~[Merged by Bors] - feat(InfinitePlace/Ramification): LiesOver class for absolute values and derived results on infinite places #27978~~
~~[Merged by Bors] - refactor: use isometry extensions for completions at infinite places of number fields #29969~~
~~[Merged by Bors] - feat(Normed/Ring/WithAbs): apply results relating algebraMaps on WithAbs #29944~~
~~[Merged by Bors] - refactor: use 1-field structure to define the WithAbs type synonym #34230~~
By Dependent Issues (🤖). Happy coding!

…xtensionEmbeddingAlgebraMap

riccardobrasca

Thanks!

bors d+

Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean

mathlib-bors · 2026-03-04T09:19:51Z

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

smmercuri · 2026-03-04T09:49:33Z

bors r+

…hrough embeddings of `v.Completion` when `w` lies over `v` (#29942) The class `ComplexEmbedding.LiesOver ψ φ` formalises the property that the complex field embedding `φ : L →+* ℂ` restricted to `K` gives `ψ : K →+* ℂ`, whenever `Algebra K L`. If `w : InfinitePlace L` and `v : InfinitePlace K` are such that we have `Algebra v.Completion w.Completion`, then `extensionEmbedding w : L →+* ℂ` restricted to `K` gives `extensionEmbedding v : K →+* ℂ`. To avoid diamonds arising from propeq instances when `K = L` we do not construct the global instance `Algebra v.Completion w.Completion` from `Algebra K L`, but assume it instead. It is then required to assume the following compatibility assumptions for the main result of this PR to be true: - `IsScalarTower (WithAbs v.1) v.Completion w.Completion` - `ContinuousSMul v.Completion w.Completion`

mathlib-bors · 2026-03-04T09:53:28Z

Build failed:

ci (staging) / Build

…xtensionEmbeddingAlgebraMap

kbuzzard · 2026-03-04T09:57:28Z

This is failing in bors; the error is

Error: error: Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean:237:10: failed to synthesize instance of type class
  Algebra (WithAbs ↑v) w.Completion

Can you merge master and try again?

kbuzzard · 2026-03-04T09:57:36Z

bors r-

kbuzzard · 2026-03-04T09:59:54Z

bors d+

mathlib-bors · 2026-03-04T09:59:56Z

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

smmercuri · 2026-03-04T10:41:26Z

bors r+

…hrough embeddings of `v.Completion` when `w` lies over `v` (#29942) The class `ComplexEmbedding.LiesOver ψ φ` formalises the property that the complex field embedding `φ : L →+* ℂ` restricted to `K` gives `ψ : K →+* ℂ`, whenever `Algebra K L`. If `w : InfinitePlace L` and `v : InfinitePlace K` are such that we have `Algebra v.Completion w.Completion`, then `extensionEmbedding w : L →+* ℂ` restricted to `K` gives `extensionEmbedding v : K →+* ℂ`. To avoid diamonds arising from propeq instances when `K = L` we do not construct the global instance `Algebra v.Completion w.Completion` from `Algebra K L`, but assume it instead. It is then required to assume the following compatibility assumptions for the main result of this PR to be true: - `IsScalarTower (WithAbs v.1) v.Completion w.Completion` - `ContinuousSMul v.Completion w.Completion`

mathlib-bors · 2026-03-04T10:55:03Z

Pull request successfully merged into master.

Build succeeded:

…hrough embeddings of `v.Completion` when `w` lies over `v` (leanprover-community#29942) The class `ComplexEmbedding.LiesOver ψ φ` formalises the property that the complex field embedding `φ : L →+* ℂ` restricted to `K` gives `ψ : K →+* ℂ`, whenever `Algebra K L`. If `w : InfinitePlace L` and `v : InfinitePlace K` are such that we have `Algebra v.Completion w.Completion`, then `extensionEmbedding w : L →+* ℂ` restricted to `K` gives `extensionEmbedding v : K →+* ℂ`. To avoid diamonds arising from propeq instances when `K = L` we do not construct the global instance `Algebra v.Completion w.Completion` from `Algebra K L`, but assume it instead. It is then required to assume the following compatibility assumptions for the main result of this PR to be true: - `IsScalarTower (WithAbs v.1) v.Completion w.Completion` - `ContinuousSMul v.Completion w.Completion`

Salvatore Mercuri and others added 18 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

Move Completion.lean

27837f9

Update Mathlib.lean

21ff23f

Fix naming in Field.WithAbs

da1b191

Define lifts of ring homs to AbsoluteValue.Completion

c3e0c43

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

2395098

…mmercuri/InfinitePlaceExtension

Update infinite place extension API

3e6b674

golf

fa1feae

Merge branch 'WithAbs-mapOfComp' into extensionEmbeddingAlgebraMap

94fab61

Add algebraMap lemmas for extensionEmbeddings

563d882

Fix direction of WithAbs.equiv

82efbfd

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

6c02074

…aming-WithAbs

Merge branch 'naming-withAbs' into WithAbs-mapOfComp

bba1e46

Fix direction of WithAbs.equiv

a559958

Merge branch 'WithAbs-mapOfComp' into extensionEmbeddingAlgebraMap

be63c07

smmercuri changed the title ~~Extension embedding algebra map~~ feat(InfinitePlace/Completion): embeddings of w.Completion factor through embeddings of v.Completion when w extends v. Sep 24, 2025

smmercuri changed the title ~~feat(InfinitePlace/Completion): embeddings of w.Completion factor through embeddings of v.Completion when w extends v.~~ feat(InfinitePlace/Completion): embeddings of w.Completion factor through embeddings of v.Completion when w extends v Sep 24, 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 Sep 24, 2025

smmercuri mentioned this pull request Sep 24, 2025

feat: dimensions of completions at infinite place extensions #27980

Open

7 tasks

smmercuri added 5 commits September 24, 2025 14:52

golf

cef1bc0

Remove .1.1

7945770

Extension.abs

98c5ed0

Add docstring for Extension.abs

36bdcdf

Fix proof in AdeleRing

d7e9a8c

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

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

db693f4

…xtensionEmbeddingAlgebraMap

smmercuri added 2 commits March 2, 2026 18:15

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

28add37

…xtensionEmbeddingAlgebraMap

fix

5411e20

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 2, 2026

rename to LiesOver

8ed4391

smmercuri changed the title ~~feat(InfinitePlace/Completion): embeddings of w.Completion factor through embeddings of v.Completion when w extends v~~ feat(InfinitePlace/Completion): embeddings of w.Completion factor through embeddings of v.Completion when w lies over v Mar 2, 2026

update IsScalarTower

0ba3e4c

smmercuri requested a review from riccardobrasca March 4, 2026 09:03

riccardobrasca self-assigned this Mar 4, 2026

riccardobrasca reviewed Mar 4, 2026

View reviewed changes

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

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

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 4, 2026

fixes

833768b

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

0fd1b1d

…xtensionEmbeddingAlgebraMap

mathlib-triage bot removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 4, 2026

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 4, 2026

switch off transparency

fb6b0f5

mathlib-bors bot closed this Mar 4, 2026

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 7c0aa26a8b

Import changes for modified files

Declarations diff

Uh oh!

mathlib-dependent-issues bot commented Mar 2, 2026

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Mar 4, 2026

Uh oh!

smmercuri commented Mar 4, 2026

Uh oh!

mathlib-bors bot commented Mar 4, 2026

Uh oh!

kbuzzard commented Mar 4, 2026

Uh oh!

kbuzzard commented Mar 4, 2026

Uh oh!

kbuzzard commented Mar 4, 2026

Uh oh!

mathlib-bors bot commented Mar 4, 2026

Uh oh!

smmercuri commented Mar 4, 2026

Uh oh!

mathlib-bors bot commented Mar 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

smmercuri commented Sep 24, 2025 •

edited

Loading

github-actions bot commented Sep 24, 2025 •

edited

Loading