The completion of a number field at an infinite place

instance NumberField.InfinitePlace.Completion.instNontriviallyNormedField_fLT {K : Type u_1} [Field K] {v : InfinitePlace K} : NontriviallyNormedField v.Completion

Equations

• NumberField.InfinitePlace.Completion.instNontriviallyNormedField_fLT = { toNormedField := NumberField.InfinitePlace.Completion.instNormedField v, non_trivial := ⋯ }

instance NumberField.InfinitePlace.Completion.instAlgebraValEqComapAlgebraMap_fLT {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {wv : ExtensionPlace L v} : Algebra v.Completion (↑wv).Completion

Equations

• NumberField.InfinitePlace.Completion.instAlgebraValEqComapAlgebraMap_fLT = (AbsoluteValue.Completion.semiAlgHomOfComp ⋯).toRingHom.toAlgebra

instance NumberField.InfinitePlace.Completion.instNormedSpaceValEqComapAlgebraMap_fLT {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {wv : ExtensionPlace L v} : NormedSpace v.Completion (↑wv).Completion

Equations

• NumberField.InfinitePlace.Completion.instNormedSpaceValEqComapAlgebraMap_fLT = { toModule := Algebra.toModule, norm_smul_le := ⋯ }

instance NumberField.InfinitePlace.Completion.instFiniteDimensionalValEqComapAlgebraMap_fLT {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {wv : ExtensionPlace L v} : FiniteDimensional v.Completion (↑wv).Completion

def NumberField.InfinitePlace.Completion.comapHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} (h : w.comap (algebraMap K L) = v) : v.Completion →ₛₐ[algebraMap (WithAbs ↑v) (WithAbs ↑w)] w.Completion

The map from v.Completion to w.Completion whenever the infinite place w of L lies above the infinite place v of K.

Equations

• NumberField.InfinitePlace.Completion.comapHom h = UniformSpace.Completion.mapSemialgHom (algebraMap (WithAbs ↑v) (WithAbs ↑w)) ⋯

theorem NumberField.InfinitePlace.Completion.comapHom_cont {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} (h : w.comap (algebraMap K L) = v) : Continuous ⇑(comapHom h)

def NumberField.InfinitePlace.Completion.piExtensionPlace {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) : v.Completion →ₛₐ[algebraMap K L] (wv : ExtensionPlace L v) → (↑wv).Completion

The map from v.Completion to the product of all completions of L lying above v.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumberField.InfinitePlace.Completion.piExtensionPlace_apply {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (x : v.Completion) : (piExtensionPlace L v) x = fun (wv : ExtensionPlace L v) => (comapHom ⋯) x

def NumberField.InfinitePlace.Completion.instAlgebraTensorProduct_fLT {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) : Algebra v.Completion (TensorProduct K L v.Completion)

Equations

• NumberField.InfinitePlace.Completion.instAlgebraTensorProduct_fLT L v = Algebra.TensorProduct.rightAlgebra

instance NumberField.InfinitePlace.Completion.instTopologicalSpaceTensorProduct_fLT {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) : TopologicalSpace (TensorProduct K L v.Completion)

Equations

• NumberField.InfinitePlace.Completion.instTopologicalSpaceTensorProduct_fLT L v = moduleTopology v.Completion (TensorProduct K L v.Completion)

instance NumberField.InfinitePlace.Completion.instIsModuleTopologyTensorProduct_fLT {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) : IsModuleTopology v.Completion (TensorProduct K L v.Completion)

@[reducible, inline]

abbrev NumberField.InfinitePlace.Completion.baseChange {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) : TensorProduct K L v.Completion →ₐ[L] (wv : ExtensionPlace L v) → (↑wv).Completion

The L-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtensionPlace.

Equations

• NumberField.InfinitePlace.Completion.baseChange L v = (NumberField.InfinitePlace.Completion.piExtensionPlace L v).baseChange_of_algebraMap

theorem NumberField.InfinitePlace.Completion.continuous_baseChange_tmul_right {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) : Continuous fun (x : v.Completion) => (baseChange L v) (1 ⊗ₜ[K] x)

@[reducible, inline]

abbrev NumberField.InfinitePlace.Completion.baseChangeRight {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) : TensorProduct K L v.Completion →ₐ[v.Completion] (wv : ExtensionPlace L v) → (↑wv).Completion

The v.Completion-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtensionPlace.

Equations

• NumberField.InfinitePlace.Completion.baseChangeRight L v = (NumberField.InfinitePlace.Completion.piExtensionPlace L v).baseChangeRightOfAlgebraMap

theorem NumberField.InfinitePlace.Completion.finrank_pi_eq_finrank_tensorProduct {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) [NumberField L] : Module.finrank v.Completion ((w : ExtensionPlace L v) → (↑w).Completion) = Module.finrank v.Completion (TensorProduct K L v.Completion)

theorem NumberField.InfinitePlace.Completion.baseChange_surjective {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) [NumberField L] : Function.Surjective ⇑(baseChange L v)

theorem NumberField.InfinitePlace.Completion.baseChange_injective {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) [NumberField L] [NumberField K] : Function.Injective ⇑(baseChange L v)

instance NumberField.InfinitePlace.Completion.instIsModuleTopologyValEqComapAlgebraMap_fLT {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) {wv : ExtensionPlace L v} : IsModuleTopology v.Completion (↑wv).Completion

instance NumberField.InfinitePlace.Completion.instIsTopologicalSemiringTensorProduct_fLT {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) [NumberField L] [NumberField K] : IsTopologicalSemiring (TensorProduct K L v.Completion)

def NumberField.InfinitePlace.Completion.baseChangeEquiv {K : Type u_1} (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) [NumberField L] [NumberField K] : TensorProduct K L v.Completion ≃A[L] (wv : ExtensionPlace L v) → (↑wv).Completion

The L-algebra homeomorphism between L ⊗[K] v.Completion and the product of all completions of L lying above v.

Equations

• NumberField.InfinitePlace.Completion.baseChangeEquiv L v = IsModuleTopology.continuousAlgEquiv K v.Completion (AlgEquiv.ofBijective (NumberField.InfinitePlace.Completion.baseChange L v) ⋯) ⋯ ⋯