[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268

xroblot · 2024-04-19T14:17:35Z

Let K be a number field of signature (r₁, r₂). This PR defines the fundamental cone: it is a cone in the mixed space that is a fundamental domain for the action of (𝓞 K)ˣ modulo torsion.

In a later PR #12333, we prove that points in the fundamental cone coming from (𝓞 K) modulo torsion are in a norm-preserving correspondence with the non-zero principal ideals of (𝓞 K).

This PR is part of the proof of the Analytic Class Number Formula.

depends on: [Merged by Bors] - feat: Add mixedEmbedding.norm #12249
depends on: [Merged by Bors] - feat(NumberField/CanonicalEmbedding): add normAtPlace #13135
depends on: [Merged by Bors] - chore: refactor ZLattice to Submodule ℤ #16604
depends on: [Merged by Bors] - feat(NumberField/CanonicalEmbedding): make the mixedSpace explicit #16634
depends on: [Merged by Bors] - feat(NumberField/CanonicalEmbedding/FundamencalCone): define the logMap #16763

…e_def

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

xroblot · 2024-04-29T16:19:46Z

~~I changed this back to WIP because I think I might need to change a bit the definition of the fundamental cone.~~

…e_def

…lCone.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

riccardobrasca

Thanks!

bors d+

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

riccardobrasca · 2024-09-17T10:41:54Z

Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

+theorem logEmbedding_fundSystem (i : Fin (rank K)) :
+    logEmbedding K (fundSystem K i) = basisUnitLattice K i := by
+   rw [basisUnitLattice, Basis.map_apply, ← fundSystem_mk, ← logEmbeddingEquiv_apply]
+   rfl


This and the previous one end with rfl. Are we missing some lemmas here?

Yes, it is a bit of a mystery to me. I think we're missing something like Additive.toMul x = Additive.toMul y → x = y and similar results (whose proofs is essentially rfl too) but I am not sure they're worth adding. The mess in fundSystem_mk comes also from the fact that there are two kinds of Additive.toMul involved...

I have the impression you are abusing defeq: logEmbedding takes a term of type Additive (𝓞 K)ˣ, but you are giving it fundSystem K i, which has type (𝓞 K)ˣ. Can we fix this somehow?

Yeah, you're right. I am probably a bit sloppy with my use of Additive. I'll see if I can fix that

All right, I think I took of all the abuses of defeq. There was a lot of Additive.ofMul missing but also the use ⟦x⟧ rather than QuotientGroup.mk x to go from (𝓞 K)ˣ to ((𝓞 K)ˣ ⧸ (torsion K)) that resulted in a wrongly typed quotient.

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

mathlib-bors · 2024-09-17T10:42:29Z

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

…e_def' into xfr_fundamental_cone_def

Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

riccardobrasca · 2024-09-17T16:44:08Z

LGTM. If there is still something to be fixed we can do it later. Thanks!

bors merge

bryangingechen · 2024-09-17T19:23:49Z

This one seems to have fallen off the queue when bors crashed (not your fault).
bors r+

Just in case something happens again:
bors d+

mathlib-bors · 2024-09-17T19:23:52Z

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

… the action of the units of a number field (#12268) Let `K` be a number field of signature `(r₁, r₂)`. This PR defines the fundamental cone: it is a cone in the mixed space that is a fundamental domain for the action of `(𝓞 K)ˣ` modulo torsion. In a later PR #12333, we prove that points in the fundamental cone coming from `(𝓞 K)` modulo torsion are in a norm-preserving correspondence with the non-zero principal ideals of `(𝓞 K)`. This PR is part of the proof of the Analytic Class Number Formula. Co-authored-by: Xavier Roblot <[email protected]>

mathlib-bors · 2024-09-17T20:27:09Z

Pull request successfully merged into master.

Build succeeded:

1st commit

1dd37b7

xroblot changed the title ~~feat: Define the fundamental cone for the action of the units of a number field~~ feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field Apr 19, 2024

xroblot added WIP Work in progress t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Apr 19, 2024

Typos

6f34395

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 Apr 19, 2024

xroblot added 3 commits April 19, 2024 16:46

Lint

01b097f

Backport changes

6b5c3d0

Merge remote-tracking branch 'origin/master' into xfr_fundamental_con…

8053571

…e_def

xroblot mentioned this pull request Apr 22, 2024

[Merged by Bors] - feat(NumberField/CanonicalEmbedding/FundamentalCone): Prove equivalence with principal ideals #12333

Closed

3 tasks

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Apr 22, 2024

Merge remote-tracking branch 'origin/master' into xfr_fundamental_con…

2ab05a8

…e_def

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 Apr 22, 2024

xroblot added 3 commits April 23, 2024 09:17

Remove instance

dee6067

Merge remote-tracking branch 'origin/master' into xfr_fundamental_con…

a054ea1

…e_def

Docs

97eb8e9

xroblot added awaiting-review awaiting-CI and removed WIP Work in progress labels Apr 29, 2024

github-actions bot removed the awaiting-CI label Apr 29, 2024

riccardobrasca reviewed Apr 29, 2024

View reviewed changes

Review

dde1762

xroblot added WIP Work in progress and removed awaiting-review labels Apr 29, 2024

xroblot added 4 commits May 11, 2024 16:41

Merge remote-tracking branch 'origin/master' into xfr_fundamental_con…

5bf273f

…e_def

update

32238a3

More lemmas

2af9cd2

Merge remote-tracking branch 'origin/master' into xfr_fundamental_con…

cf69fd5

…e_def

xroblot and others added 5 commits September 17, 2024 10:32

Update Basic.lean

f53e61a

clean up

2252cf4

Update FundamentalCone.lean

966c177

Update Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Fundamenta…

dd73259

…lCone.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Update Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Fundamenta…

df5d3c5

…lCone.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

xroblot requested a review from riccardobrasca September 17, 2024 09:36

riccardobrasca approved these changes Sep 17, 2024

View reviewed changes

leanprover-community-mathlib4-bot added the delegated label Sep 17, 2024

xroblot added 4 commits September 17, 2024 13:01

Review

1a12c46

rfl

3460cc6

Merge remote-tracking branch 'refs/remotes/origin/xfr_fundamental_con…

b4a0e68

…e_def' into xfr_fundamental_cone_def

fix defeq abuse

3467d82

riccardobrasca reviewed Sep 17, 2024

View reviewed changes

Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean Outdated Show resolved Hide resolved

xroblot added the WIP Work in progress label Sep 17, 2024

xroblot added 3 commits September 17, 2024 18:13

clean up

974b8c5

more defeq

fe7db50

whitespace

5bb55bc

xroblot added awaiting-CI and removed WIP Work in progress labels Sep 17, 2024

github-actions bot removed the awaiting-CI label Sep 17, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 17, 2024

mathlib-bors bot changed the title ~~feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field~~ [Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field Sep 17, 2024

mathlib-bors bot closed this Sep 17, 2024

mathlib-bors bot deleted the xfr_fundamental_cone_def branch September 17, 2024 20:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268

xroblot commented Apr 19, 2024 •

edited

Loading

xroblot commented Apr 29, 2024 •

edited

Loading

riccardobrasca left a comment

riccardobrasca Sep 17, 2024

xroblot Sep 17, 2024

riccardobrasca Sep 17, 2024 •

edited

Loading

xroblot Sep 17, 2024

xroblot Sep 17, 2024

mathlib-bors bot commented Sep 17, 2024

riccardobrasca commented Sep 17, 2024

bryangingechen commented Sep 17, 2024

mathlib-bors bot commented Sep 17, 2024

mathlib-bors bot commented Sep 17, 2024

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268

[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268

Conversation

xroblot commented Apr 19, 2024 • edited Loading

xroblot commented Apr 29, 2024 • edited Loading

riccardobrasca left a comment

Choose a reason for hiding this comment

riccardobrasca Sep 17, 2024

Choose a reason for hiding this comment

xroblot Sep 17, 2024

Choose a reason for hiding this comment

riccardobrasca Sep 17, 2024 • edited Loading

Choose a reason for hiding this comment

xroblot Sep 17, 2024

Choose a reason for hiding this comment

xroblot Sep 17, 2024

Choose a reason for hiding this comment

mathlib-bors bot commented Sep 17, 2024

riccardobrasca commented Sep 17, 2024

bryangingechen commented Sep 17, 2024

mathlib-bors bot commented Sep 17, 2024

mathlib-bors bot commented Sep 17, 2024

xroblot commented Apr 19, 2024 •

edited

Loading

xroblot commented Apr 29, 2024 •

edited

Loading

riccardobrasca Sep 17, 2024 •

edited

Loading