feat: predicates for extensions of complex embeddings#24877
feat: predicates for extensions of complex embeddings#24877
Conversation
PR summary 1e5008c035Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
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. |
|
One of the main results of these series of PRs is Your point about duplication is valid though, particularly to the dependent PR #24882 where, for example, I define { 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 |
| variable (φ ψ) | ||
|
|
||
| /-- | ||
| If `L/K` and `ψ : K →+* ℂ`, `φ : L →+* ℂ`, then `φ` is a _mixed extension_ of `ψ` if the |
There was a problem hiding this comment.
I am not sure about calling it a mixed extension but since I cannot think of anything better, I can guess it's fine. We could call it ComplexEmbedding.RamifiedExtension, I guess, but it might get too confusing
There was a problem hiding this comment.
I am also unsure of the naming, so I'm open to other suggestions, but I do think we should avoid using ramified for complex embeddings as it would be a bit confusing.
|
This pull request has conflicts, please merge |
|
This PR has been migrated to a fork-based workflow: #27977 |
If `L/K` and `ψ : K →+* ℂ`, we define the subtype `ComplexExtension L ψ` of `L →+* ℂ` that extend `ψ` to `L`. Also define two predicates asserting ways that `φ` can extend `ψ`. - `φ.IsMixed` : `ψ` has real image while `φ` has complex image. - `φ.IsUnmixed`: the negation of `IsMixed` -- `ψ` has real image if and only if `φ` has real image. `ComplexExtension.IsMixed` and `ComplexExtension.IsUnmixed` are the `ComplexEmbedding` analogues to ramified and unramified infinite places, which is a two-to-one isomorphism in the former and a one-to-one isomorphism in the latter, hence the slightly different terminology. This PR continues the work from #24877. Original PR: #24877
…munity#27977) If `L/K` and `ψ : K →+* ℂ`, we define the subtype `ComplexExtension L ψ` of `L →+* ℂ` that extend `ψ` to `L`. Also define two predicates asserting ways that `φ` can extend `ψ`. - `φ.IsMixed` : `ψ` has real image while `φ` has complex image. - `φ.IsUnmixed`: the negation of `IsMixed` -- `ψ` has real image if and only if `φ` has real image. `ComplexExtension.IsMixed` and `ComplexExtension.IsUnmixed` are the `ComplexEmbedding` analogues to ramified and unramified infinite places, which is a two-to-one isomorphism in the former and a one-to-one isomorphism in the latter, hence the slightly different terminology. This PR continues the work from leanprover-community#24877. Original PR: leanprover-community#24877
…munity#27977) If `L/K` and `ψ : K →+* ℂ`, we define the subtype `ComplexExtension L ψ` of `L →+* ℂ` that extend `ψ` to `L`. Also define two predicates asserting ways that `φ` can extend `ψ`. - `φ.IsMixed` : `ψ` has real image while `φ` has complex image. - `φ.IsUnmixed`: the negation of `IsMixed` -- `ψ` has real image if and only if `φ` has real image. `ComplexExtension.IsMixed` and `ComplexExtension.IsUnmixed` are the `ComplexEmbedding` analogues to ramified and unramified infinite places, which is a two-to-one isomorphism in the former and a one-to-one isomorphism in the latter, hence the slightly different terminology. This PR continues the work from leanprover-community#24877. Original PR: leanprover-community#24877
If
L/K,ψ : K →+* ℂ,φ : L →+* ℂwe define three predicates asserting ways thatφcan extendψ.IsExtension ψ φ: the restriction ofφtoKisψ.IsMixedExtension ψ φ: the restriction ofφtoKisψ,ψhas real image whileφhas complex image.IsUnmixedExtension ψ φ: the restriction ofφtoKisψ,ψhas real image if and only ifφhas real image.IsMixedExtensionandIsUnmixedExtensionare theComplexEmbeddinganalogues to ramified and unramified infinite places.