Atlas.NumberTheoryI.code.GlobalFields

def AbsoluteValue.IsTrivial {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) :

Instances For

theorem AbsoluteValue.IsTrivial.map_ne_zero {K : Type u_1} [Field K] {v : AbsoluteValue K ℝ} (hv : v.IsTrivial) {x : K} (hx : x ≠ 0) :

v x = 1

source

theorem AbsoluteValue.IsTrivial.of_isEquiv {K : Type u_1} [Field K] {v w : AbsoluteValue K ℝ} (hv : v.IsTrivial) (h : v.IsEquiv w) :

w.IsTrivial

source

@[implicit_reducible]

instance nontrivialAbsValSetoid (K : Type u_1) [Field K] :

Setoid { v : AbsoluteValue K ℝ // ¬v.IsTrivial }

source

def Place (K : Type u_1) [Field K] :

Type u_1

Instances For

source

def restrictPlace {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (w : NumberField.InfinitePlace L) :

NumberField.InfinitePlace K

Instances For

source

def InfinitePlace.LiesAbove {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) :

Prop

Instances For

source

def FinitePlace.LiesAbove {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Prop

Instances For

source

@[implicit_reducible]

noncomputable instance instAlgebraBaseOfExtCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] (w : NumberField.InfinitePlace L) :

Algebra K w.Completion

source

@[implicit_reducible]

noncomputable instance instAlgebraBaseOfExtAdicCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) :

Algebra K (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

source

theorem theorem_13_5_dense_embedding (K : Type u_1) [Field K] [NumberField K] :

DenseRange ⇑(algebraMap K ((v : NumberField.InfinitePlace K) → WithAbs ↑v))

source

noncomputable def algebraMapLToCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] (w : NumberField.InfinitePlace L) :

L →ₐ[K] w.Completion

Instances For

source

noncomputable def completionEmbedding {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) (hw : w.comap (algebraMap K L) = v) :

v.Completion →ₐ[K] w.Completion

Instances For

source

noncomputable def canonicalMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

TensorProduct K L v.Completion →ₐ[K] (w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion

Instances For

source

@[implicit_reducible]

noncomputable instance nontriviallyNormedField_infinitePlace_completion {K : Type u_1} [Field K] [NumberField K] (v : NumberField.InfinitePlace K) :

NontriviallyNormedField v.Completion

source

theorem completionEmbedding_continuous {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) (hw : w.comap (algebraMap K L) = v) :

Continuous ⇑(completionEmbedding v w hw)

source

theorem canonicalMap_surjective_hfd_tgt {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

FiniteDimensional v.Completion ((w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)

source

theorem degree_identity_infinite_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) [Fintype { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }] :

Module.finrank K L = ∑ w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }, Module.finrank v.Completion (↑w).Completion

source

theorem canonicalMap_surjective_hdim {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Module.finrank v.Completion (TensorProduct K L v.Completion) = Module.finrank v.Completion ((w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)

source

theorem canonicalMap_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Function.Injective ⇑(canonicalMap v)

source

theorem canonicalMap_surjective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Function.Surjective ⇑(canonicalMap v)

source

theorem canonicalMap_bijective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Function.Bijective ⇑(canonicalMap v)

source

noncomputable def canonicalMapEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

TensorProduct K L v.Completion ≃+* ((w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)

Instances For

source

theorem canonicalMap_tmul_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) (l : L) (w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) :

(canonicalMap v) (l ⊗ₜ[K] 1) w = (algebraMap L (↑w).Completion) l

source

theorem theorem_13_5_tensor_product_iso {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Nonempty (TensorProduct K L v.Completion ≃ₐ[K] (w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)

source

theorem theorem_13_5_tensor_product_iso_Kv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Nonempty (TensorProduct K L v.Completion ≃ₐ[v.Completion] (ω : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑ω).Completion)

source

noncomputable def completionEmbedding_finite_ringHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) :

WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v) →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion L w

Instances For

source

theorem multiplicative_toAdd_pow (h : Multiplicative ℤ) (e : ℕ) :

Multiplicative.toAdd (h ^ e) = ↑e * Multiplicative.toAdd h

source

theorem exists_pow_lt_of_ne_zero (m : WithZero (Multiplicative ℤ)) (hm : m ≠ 0) (e : ℕ) (he : e ≠ 0) :

∃ (d : WithZero (Multiplicative ℤ)), d ≠ 0 ∧ ∀ a < d, a ^ e < m

source

theorem algebraMap_withVal_continuous {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

Continuous ⇑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation L w)).symm.toRingHom.comp ((algebraMap K L).comp (WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).toRingHom))

source

theorem completionEmbedding_finite_continuous {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

Continuous ⇑(completionEmbedding_finite_ringHom v w)

source

noncomputable def completionEmbedding_finite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

IsDedekindDomain.HeightOneSpectrum.adicCompletion K v →ₐ[K] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w

Instances For

source

noncomputable def algebraMapLToAdicCompletion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) :

L →ₐ[K] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w

Instances For

source

noncomputable def canonicalMap_finite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) →ₐ[K] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w

Instances For

source

theorem prop_4_36_tensorProduct_finite_isSemisimpleRing {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

IsSemisimpleRing (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

source

theorem finitePlacesAbove_finite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Finite { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }

source

theorem prop_10_3_10_4_finiteDimensional_completion {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

source

theorem thm_11_23_4_local_degree_ef {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)] :

Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) = v.asIdeal.ramificationIdx w.asIdeal * v.asIdeal.inertiaDeg w.asIdeal

source

theorem thm_5_35_11_23_degree_identity_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (instAlg : (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) (instST : ∀ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }), IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) :

Module.finrank K L = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

source

theorem prop_10_3_10_4_finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ((w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

source

theorem canonicalMap_finite_isKvLinear {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

∃ (f : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) →ₗ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w), ∀ (x : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), f x = (canonicalMap_finite v) x

source

theorem canonicalMap_finite_ker_eq_bot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

RingHom.ker (canonicalMap_finite v) = ⊥

source

theorem canonicalMap_finite_surjective_by_approx {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Function.Surjective ⇑(canonicalMap_finite v)

source

theorem cor_4_32_no_nonzero_idempotent_in_ker_finite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (e : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (he_idem : IsIdempotentElem e) (he_ker : (canonicalMap_finite v) e = 0) :

e = 0

source

theorem canonicalMap_finite_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Function.Injective ⇑(canonicalMap_finite v)

source

theorem canonicalMap_finite_surjective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Function.Surjective ⇑(canonicalMap_finite v)

source

theorem theorem_13_5_finite_place {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Nonempty (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[K] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

source

theorem theorem_13_5_finite_place_Kv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

∃ (e : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (ω : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑ω), ∀ (α : L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }), e (α ⊗ₜ[K] 1) w = (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α

source

theorem completion_real_ringEquiv {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) :

Nonempty (w.Completion ≃+* ℝ)

source

theorem completion_complex_ringEquiv {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) :

Nonempty (w.Completion ≃+* ℂ)

source

def factors_equiv_infinitePlace (K : Type u_1) [Field K] [NumberField K] (α : K) (hα : ℚ[α] = ⊤) (v : NumberField.InfinitePlace ℚ) (hiso : Nonempty (TensorProduct ℚ K v.Completion ≃ₐ[ℚ ] (w : { w : NumberField.InfinitePlace K // w.comap (algebraMap ℚ K) = v }) → (↑w).Completion)) :

Fin (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (algebraMap ℚ ℝ) (minpoly ℚ α))).card ≃ NumberField.InfinitePlace K

Instances For

source

def factors_equiv_places_above_real (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : NumberField.InfinitePlace K) (hv : v.IsReal) (α : L) (hα : K[α] = ⊤) (hiso : Nonempty (TensorProduct K L v.Completion ≃ₐ[K] (w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)) :

Fin (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map ((NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv).toRingHom.comp (algebraMap K v.Completion)) (minpoly K α))).card ≃ { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }

Instances For

source

def deg_equiv_places_above_complex (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : NumberField.InfinitePlace K) (hv : v.IsComplex) (α : L) (hα : K[α] = ⊤) (hiso : Nonempty (TensorProduct K L v.Completion ≃ₐ[K] (w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)) :

Fin (Module.finrank K L) ≃ { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }

Instances For

source

theorem corollary_13_6_factor_count (K : Type u_1) [Field K] [NumberField K] :

Fintype.card (NumberField.InfinitePlace K) = NumberField.InfinitePlace.nrRealPlaces K + NumberField.InfinitePlace.nrComplexPlaces K

source

theorem corollary_13_6_irred_factors (K : Type u_1) [Field K] [NumberField K] (α : K) (hα : ℚ[α] = ⊤) :

(UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (algebraMap ℚ ℝ) (minpoly ℚ α))).card = Fintype.card (NumberField.InfinitePlace K)

source

theorem corollary_13_6_places_above_real (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : NumberField.InfinitePlace K) (hv : v.IsReal) (α : L) (hα : K[α] = ⊤) :

{w : NumberField.InfinitePlace L | w.comap (algebraMap K L) = v}.card = (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map ((NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv).toRingHom.comp (algebraMap K v.Completion)) (minpoly K α))).card

source

theorem corollary_13_6_places_above_complex (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : NumberField.InfinitePlace K) (hv : v.IsComplex) (α : L) (hα : K[α] = ⊤) :

{w : NumberField.InfinitePlace L | w.comap (algebraMap K L) = v}.card = Module.finrank K L

source

theorem factors_equiv_places_above_finite (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (α : L) (hα : K[α] = ⊤) (hiso : Nonempty (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[K] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) :

source

theorem completion_ringEquiv_adjoinRoot (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (α : L) (hα : K[α] = ⊤) (e : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v } ≃ { q : Polynomial (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) // q.Monic ∧ Irreducible q ∧ q ∣ Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (minpoly K α) }) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w ≃+* AdjoinRoot ↑(e ⟨w, hw⟩))

source

theorem corollary_13_6_places_above_finite (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (α : L) (hα : K[α] = ⊤) :

source

theorem corollary_13_6_completion_iso_finite (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (α : L) (hα : K[α] = ⊤) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

∃ (q : Polynomial (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), q.Monic ∧ Irreducible q ∧ q ∣ Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (minpoly K α) ∧ Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w ≃+* AdjoinRoot q)

source

noncomputable def corollary_13_7_orbit_equiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsGalois k K] :

Quotient (MulAction.orbitRel Gal(K/k) (NumberField.InfinitePlace K)) ≃ NumberField.InfinitePlace k

Instances For

source

theorem corollary_13_7_mem_orbit_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] {w w' : NumberField.InfinitePlace K} :

w' ∈ MulAction.orbit Gal(K/k) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)

source

theorem corollary_13_7_exists_smul_eq {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] {w w' : NumberField.InfinitePlace K} (h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)) :

∃ (σ : Gal(K/k)), σ • w = w'

source

theorem corollary_13_7_comap_surjective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] :

Function.Surjective fun (x : NumberField.InfinitePlace K) => x.comap (algebraMap k K)

source

theorem corollary_13_7_mk_eq_iff {K : Type u_1} [Field K] {φ ψ : K →+* ℂ} :

NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk ψ ↔ φ = ψ ∨ NumberField.ComplexEmbedding.conjugate φ = ψ

source

theorem place_isReal_or_isComplex {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) :

w.IsReal ∨ w.IsComplex

source

def ComplexEmbedding.conjugateSetoid (L : Type u_1) [Field L] :

Setoid (L →+* ℂ)

Instances For

source

theorem ComplexEmbedding.conjugateSetoid_rel_iff {L : Type u_1} [Field L] {φ ψ : L →+* ℂ} :

(conjugateSetoid L) φ ψ ↔ φ = ψ ∨ NumberField.ComplexEmbedding.conjugate φ = ψ

source

noncomputable def corollary_13_7_embedding_orbit_equiv_Q (L : Type u_1) [Field L] :

Quotient (ComplexEmbedding.conjugateSetoid L) ≃ NumberField.InfinitePlace L

Instances For

source

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

Type u_2

Instances For

source

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

Setoid (EmbeddingsAbove K v)

Instances For

source

noncomputable def corollary_13_7_embeddings_equiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Quotient (conjugateSetoidAbove v) ≃ { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }

Instances For

source

@[reducible, inline]

abbrev IsRealEmbedding {K : Type u_1} [Field K] (φ : K →+* ℂ) :

Prop

Instances For

source

@[reducible, inline]

abbrev IsComplexEmbedding {K : Type u_1} [Field K] (φ : K →+* ℂ) :

Prop

Instances For

source

theorem isRealEmbedding_iff_isReal_place {K : Type u_1} [Field K] {φ : K →+* ℂ} :

IsRealEmbedding φ ↔ (NumberField.InfinitePlace.mk φ).IsReal

source

theorem isComplexEmbedding_iff_isComplex_place {K : Type u_1} [Field K] {φ : K →+* ℂ} :

IsComplexEmbedding φ ↔ (NumberField.InfinitePlace.mk φ).IsComplex

source

theorem corollary_13_9 (K : Type u_1) [Field K] [NumberField K] :

NumberField.InfinitePlace.nrRealPlaces K + 2 * NumberField.InfinitePlace.nrComplexPlaces K = Module.finrank ℚ K

source

theorem card_complex_embeddings_eq (K : Type u_1) [Field K] [NumberField K] :

Fintype.card { φ : K →+* ℂ // ¬NumberField.ComplexEmbedding.IsReal φ } = 2 * NumberField.InfinitePlace.nrComplexPlaces K

source

theorem card_real_embeddings_eq (K : Type u_1) [Field K] [NumberField K] :

Fintype.card { φ : K →+* ℂ // NumberField.ComplexEmbedding.IsReal φ } = NumberField.InfinitePlace.nrRealPlaces K

source

theorem proposition_13_11 (K : Type u_1) [Field K] [NumberField K] :

(NumberField.discr K).sign = (-1) ^ NumberField.InfinitePlace.nrComplexPlaces K

source

theorem discr_ne_zero' (K : Type u_1) [Field K] [NumberField K] :

NumberField.discr K ≠ 0

source

theorem tensorProductDecomp_denseRange (K : Type u_1) [Field K] [NumberField K] :

DenseRange ⇑(algebraMap K ((v : NumberField.InfinitePlace K) → WithAbs ↑v))

Alias of theorem_13_5_dense_embedding.

source

theorem tensorProductDecomp_infinitePlace {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Nonempty (TensorProduct K L v.Completion ≃ₐ[K] (w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)

Alias of theorem_13_5_tensor_product_iso.

source

theorem tensorProductDecomp_infinitePlace_Kv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Nonempty (TensorProduct K L v.Completion ≃ₐ[v.Completion] (ω : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑ω).Completion)

Alias of theorem_13_5_tensor_product_iso_Kv.

source

theorem tensorProductDecomp_finitePlace {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Nonempty (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[K] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

Alias of theorem_13_5_finite_place.

source

theorem tensorProductDecomp_finitePlace_Kv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

∃ (e : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (ω : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑ω), ∀ (α : L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }), e (α ⊗ₜ[K] 1) w = (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α

Alias of theorem_13_5_finite_place_Kv.

source

theorem infinitePlace_card_eq_real_add_complex (K : Type u_1) [Field K] [NumberField K] :

Fintype.card (NumberField.InfinitePlace K) = NumberField.InfinitePlace.nrRealPlaces K + NumberField.InfinitePlace.nrComplexPlaces K

Alias of corollary_13_6_factor_count.

source

theorem irredFactors_card_eq_infinitePlace_card (K : Type u_1) [Field K] [NumberField K] (α : K) (hα : ℚ[α] = ⊤) :

(UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (algebraMap ℚ ℝ) (minpoly ℚ α))).card = Fintype.card (NumberField.InfinitePlace K)

Alias of corollary_13_6_irred_factors.

source

theorem placesAboveReal_card_eq_irredFactors (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : NumberField.InfinitePlace K) (hv : v.IsReal) (α : L) (hα : K[α] = ⊤) :

{w : NumberField.InfinitePlace L | w.comap (algebraMap K L) = v}.card = (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map ((NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal hv).toRingHom.comp (algebraMap K v.Completion)) (minpoly K α))).card

Alias of corollary_13_6_places_above_real.

source

theorem placesAboveComplex_card_eq_finrank (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : NumberField.InfinitePlace K) (hv : v.IsComplex) (α : L) (hα : K[α] = ⊤) :

{w : NumberField.InfinitePlace L | w.comap (algebraMap K L) = v}.card = Module.finrank K L

Alias of corollary_13_6_places_above_complex.

source

theorem placesAboveFinite_equiv_irredFactors (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (α : L) (hα : K[α] = ⊤) :

Alias of corollary_13_6_places_above_finite.

source

theorem completionIso_finitePlace_adjoinRoot (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (α : L) (hα : K[α] = ⊤) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

∃ (q : Polynomial (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), q.Monic ∧ Irreducible q ∧ q ∣ Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (minpoly K α) ∧ Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w ≃+* AdjoinRoot q)

Alias of corollary_13_6_completion_iso_finite.

source

def galoisOrbit_infinitePlace_equiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsGalois k K] :

Quotient (MulAction.orbitRel Gal(K/k) (NumberField.InfinitePlace K)) ≃ NumberField.InfinitePlace k

Alias of corollary_13_7_orbit_equiv.

Instances For

source

theorem infinitePlace_mem_orbit_iff_comap_eq {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] {w w' : NumberField.InfinitePlace K} :

w' ∈ MulAction.orbit Gal(K/k) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)

Alias of corollary_13_7_mem_orbit_iff.

source

theorem infinitePlace_exists_smul_eq_of_comap_eq {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsGalois k K] {w w' : NumberField.InfinitePlace K} (h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)) :

∃ (σ : Gal(K/k)), σ • w = w'

Alias of corollary_13_7_exists_smul_eq.

source

theorem infinitePlace_comap_surjective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] :

Function.Surjective fun (x : NumberField.InfinitePlace K) => x.comap (algebraMap k K)

Alias of corollary_13_7_comap_surjective.

source

theorem infinitePlace_mk_eq_iff_conjugate {K : Type u_1} [Field K] {φ ψ : K →+* ℂ} :

NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk ψ ↔ φ = ψ ∨ NumberField.ComplexEmbedding.conjugate φ = ψ

Alias of corollary_13_7_mk_eq_iff.

source

def conjugateOrbit_equiv_infinitePlace (L : Type u_1) [Field L] :

Quotient (ComplexEmbedding.conjugateSetoid L) ≃ NumberField.InfinitePlace L

Alias of corollary_13_7_embedding_orbit_equiv_Q.

Instances For

source

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

Quotient (conjugateSetoidAbove v) ≃ { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }

Alias of corollary_13_7_embeddings_equiv.

Instances For

source

theorem nrRealPlaces_add_two_nrComplexPlaces_eq_finrank (K : Type u_1) [Field K] [NumberField K] :

NumberField.InfinitePlace.nrRealPlaces K + 2 * NumberField.InfinitePlace.nrComplexPlaces K = Module.finrank ℚ K

Alias of corollary_13_9.

source

theorem discr_sign_eq_neg_one_pow_nrComplexPlaces (K : Type u_1) [Field K] [NumberField K] :

(NumberField.discr K).sign = (-1) ^ NumberField.InfinitePlace.nrComplexPlaces K

Alias of proposition_13_11.

source

theorem tensorProduct_isSemisimpleRing_finitePlace {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

IsSemisimpleRing (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

Alias of prop_4_36_tensorProduct_finite_isSemisimpleRing.

source

theorem completionEmbedding_finiteDimensional {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) :

FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

Alias of prop_10_3_10_4_finiteDimensional_completion.

source

theorem finrank_tensorProduct_eq_finrank_completionProd {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ((w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

Alias of prop_10_3_10_4_finrank_eq.

source

theorem localDegree_eq_ramificationIdx_mul_inertiaDeg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)] :

Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) = v.asIdeal.ramificationIdx w.asIdeal * v.asIdeal.inertiaDeg w.asIdeal

Alias of thm_11_23_4_local_degree_ef.

source

theorem finrank_eq_sum_localDegrees {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (instAlg : (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) (instST : ∀ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }), IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) :

Module.finrank K L = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)

Alias of thm_5_35_11_23_degree_identity_finrank.

source

theorem canonicalMap_finite_ker_no_nonzero_idempotent {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (e : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (he_idem : IsIdempotentElem e) (he_ker : (canonicalMap_finite v) e = 0) :

e = 0

Alias of cor_4_32_no_nonzero_idempotent_in_ker_finite.

source

theorem completionProd_finiteDimensional_infinitePlace {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

FiniteDimensional v.Completion ((w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)

Alias of canonicalMap_surjective_hfd_tgt.

source

theorem finrank_tensorProduct_eq_finrank_completionProd_infinite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) :

Module.finrank v.Completion (TensorProduct K L v.Completion) = Module.finrank v.Completion ((w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)

Alias of canonicalMap_surjective_hdim.

source

theorem finrank_eq_sum_localDegrees_infinite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) [Fintype { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }] :

Module.finrank K L = ∑ w : { w : NumberField.InfinitePlace L // w.comap (algebraMap K L) = v }, Module.finrank v.Completion (↑w).Completion

Alias of degree_identity_infinite_finrank.

source

theorem canonicalMap_finite_completionLinear {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :

∃ (f : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) →ₗ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w), ∀ (x : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), f x = (canonicalMap_finite v) x

Alias of canonicalMap_finite_isKvLinear.