Commit 2026-03-04 10:41 3a31ced7

feat(InfinitePlace/Completion): embeddings of w.Completion factor through 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