Comments from Original PR #24877

This section contains 2 comment(s) from the original PR, excluding bot comments.

@xroblot (2025-05-20 11:10 UTC):
I think something like that it's definitely a good idea, but I'd like to have a better understanding of how this is going to combine with what's already there for infinite places. In particular, I have the feeling there is a risk for code duplication. Maybe ramification of complex embeddings should follow from ramification of infinite places or the other way around, but I don't think that having two definitions of ramifications and then prove that there are consistent is the way to go. I could be wrong though so I am ready to hear counterargument.

@smmercuri (2025-05-20 16:43 UTC):
One of the main results of these series of PRs is ∑ (v | w), w.ramificationIdx K = Module.finrank K L, whose proof basically goes #UnramifiedExtension + 2*#RamifiedExtension = #ComplexExtensions = #(L →ₐ[K] ℂ) = Module.finrank K L. So I need some way of talking about extensions of complex embeddings. I think these differ somewhat from ramification of infinite places, since if v | w then we are not guaranteed that w.embedding extends v.embedding. Indeed in the ramified case there is a two-to-one map from infinite place extensions to complex extensions (see one of the dependent PRs). Because of this difference, I feel the content of this PR does not quite risk duplication, and I think it's just a question of whether these predicates are worth giving explicit names to or not, which I think they are.

Your point about duplication is valid though, particularly to the dependent PR #24882 where, for example, I define UnramifiedExtension as

{ w : InfinitePlace L // w.comap (algebraMap K L) = v ∧ w.IsUnramified K }

but it could be replaced with

{ w : InfinitePlace L // ∃ ψ, w = mk ψ ∧ IsUnmixedExtension v.embedding ψ }

or possibly removed altogether.

Overall, I still feel these are different enough to have as separate defs, but if we do want to reduce them then I think we should do it via the ComplexEmbedding -> InfinitePlace way around, which would affect #24882 rather than this PR.

PR summary 7fe074626b

Import changes for modified files

No significant changes to the import graph

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

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

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

@smmercuri is this still WIP?

@smmercuri is this still WIP?

Ah yes it is, I still need to incorporate feedback from the old PR. Planning to work through my WIP PRs over the next week!

@smmercuri is this still WIP?

Ah yes it is, I still need to incorporate feedback from the old PR. Planning to work through my WIP PRs over the next week!

Please let me know when this is not WIP anymore so I take another look.

@smmercuri is this still WIP?

Ah yes it is, I still need to incorporate feedback from the old PR. Planning to work through my WIP PRs over the next week!

Please let me know when this is not WIP anymore so I take another look.

Thanks! This is now ready to review.

LGTM. I was gonna complain about the use of the term mixed by then I remembered that I was the one that named the NumberField.mixedEmbedding.mixedSpace so I should probably not 😅

Yes this is one reason I went for that terminology. I'm also unsure about whether it's the right term in this case so I would be open to other suggestions. Perhaps IsSplit is more appropriate?

On the other hand, I think I would drop the Complex in ComplexExtension but that might require to protect the definition since there seems to be quite a lot of things called Extension already in Mathlib. So it's up to you

I did have this as ComplexEmbedding.Extension previously, but I also define InfinitePlace.Extension further up so was trying to avoid confusion. I'll just protect them and make sure to use dot notation instead!

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• CI Success