Theorems · Theorem · number theory

NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding

∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [inst_3 : Algebra v.Completion w.Completion]
  [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion]
  [NumberField.ComplexEmbedding.LiesOver w.embedding v.embedding],
  NumberField.ComplexEmbedding.LiesOver (NumberField.InfinitePlace.Completion.extensionEmbedding w)
    (NumberField.InfinitePlace.Completion.extensionEmbedding v)

Assume that w.Completion forms an algebra over v.Completion with continuous scalar action, such that IsScalarTower K v.Completion w.Completion. If w.embedding : L →+* ℂ extends v.embedding : K →+* ℂ, then the corresponding embeddings to completions are also extensions.

Defined in

Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Cited by

2 results in Mathlib

Foundations

Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraAlgebraIsScalarTowerContinuousSMulNumberField.ComplexEmbedding.LiesOver