LiesOver instances for completions of number fields

If L and K are number fields such that Algebra K L then this algebra extends naturally to the completions of K and L at places, whenever the place of L lies over the place of K. This file contains the relevant instances and properties of this extension as scoped instances. These are scoped because they create non-defeq instance diamonds when K = L.

@[implicit_reducible]

noncomputable def NumberField.LiesOver.instAlgebraCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [(↑w).LiesOver ↑v] : Algebra v.Completion w.Completion

If w lies over v, then w.Completion is a v.Completion-algebra.

Equations

• NumberField.LiesOver.instAlgebraCompletion = ⋯.mapRingHom.toAlgebra

theorem NumberField.LiesOver.instIsScalarTowerCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [(↑w).LiesOver ↑v] : IsScalarTower K v.Completion w.Completion

theorem NumberField.LiesOver.instContinuousSMulCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [(↑w).LiesOver ↑v] : ContinuousSMul v.Completion w.Completion