-
Notifications
You must be signed in to change notification settings - Fork 331
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.
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
[Merged by Bors] - feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field #12268
Conversation
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Outdated
Show resolved
Hide resolved
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Outdated
Show resolved
Hide resolved
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Outdated
Show resolved
Hide resolved
|
…lCone.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…lCone.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors d+
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Outdated
Show resolved
Hide resolved
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Outdated
Show resolved
Hide resolved
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
Outdated
Show resolved
Hide resolved
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This and the previous one end with rfl
. Are we missing some lemmas here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, you're right. I am probably a bit sloppy with my use of Additive
. I'll see if I can fix that
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
Outdated
Show resolved
Hide resolved
✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with |
…e_def' into xfr_fundamental_cone_def
LGTM. If there is still something to be fixed we can do it later. Thanks! bors merge |
This one seems to have fallen off the queue when bors crashed (not your fault). Just in case something happens again: |
✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with |
… 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]>
Pull request successfully merged into master. Build succeeded: |
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.
mixedEmbedding.norm
#12249ZLattice
toSubmodule ℤ
#16604mixedSpace
explicit #16634