The completion of a number field at an infinite place

def NumberField.InfinitePlace.Completion.comapSemialgHom {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

Equations

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

theorem NumberField.InfinitePlace.Completion.comapSemialgHom_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 ⇑(comapSemialgHom h)

@[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) : v.Completion →ₛₐ[algebraMap K L] (wv : ExtensionPlace L v) → (↑wv).Completion

Equations

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

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)

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

Equations

• NumberField.InfinitePlace.Completion.piExtensionPlaceContinuousAlgHom L v = { toAlgHom := (NumberField.InfinitePlace.Completion.baseChange L v).baseChange_of_algebraMap, cont := ⋯ }