Documentation

Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

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.

source
noncomputable def NumberField.LiesOver.completionMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] :
v.Completion →+* w.Completion

The ring homomorphism v.Completion →+* w.Completion induced by algebraMap K L, when w lies over v.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NumberField.LiesOver.continuous_completionMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] :
    Continuous ⇑completionMap
    source
    theorem NumberField.LiesOver.completionMap_coe {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} [w.LiesOver v] (x : WithAbs ↑v) :
    completionMap { toCompletion := ↑x } = { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }
    source
    @[instance_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
    Instances For
      source
      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
      source
      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