noncomputable def InfinitePlace.localNormHom {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) : w.Completion →* v.Completion

noncomputable def infiniteNormComponent (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : NumberField.InfinitePlace K) : NumberField.InfiniteAdeleRing L →* v.Completion

noncomputable def infiniteAdeleNormHom (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : NumberField.InfiniteAdeleRing L →* NumberField.InfiniteAdeleRing K

theorem extensionEmbedding_algebraMap {K : Type u_1} [Field K] [NumberField K] (v : NumberField.InfinitePlace K) (y : K) : (NumberField.InfinitePlace.Completion.extensionEmbedding v) ((algebraMap K v.Completion) y) = v.embedding y

theorem infiniteNormComponent_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (x : L) (v : NumberField.InfinitePlace K) : (infiniteNormComponent K L v) ((algebraMap L (NumberField.InfiniteAdeleRing L)) x) = (algebraMap K v.Completion) ((Algebra.norm K) x)

theorem infiniteAdeleNormHom_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (x : L) : (infiniteAdeleNormHom K L) ((algebraMap L (NumberField.InfiniteAdeleRing L)) x) = (algebraMap K (NumberField.InfiniteAdeleRing K)) ((Algebra.norm K) x)

@[reducible]

noncomputable def HeightOneSpectrum.adicCompletionAlgebra {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hw : v.asIdeal ≤ Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal) : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

noncomputable def HeightOneSpectrum.localNormHom {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hw : v.asIdeal ≤ Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal) : IsDedekindDomain.HeightOneSpectrum.adicCompletion L w →* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

theorem HeightOneSpectrum.localNormHom_mem_integers {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hw : v.asIdeal ≤ Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) (hx : x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w) : (localNormHom w v hw) x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

theorem HeightOneSpectrum.finite_placesAbove {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : {w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) | Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal}.Finite

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

theorem HeightOneSpectrum.liesOver_of_mem_placesAbove {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)} (hw : w ∈ placesAbove v) : v.asIdeal ≤ Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal

noncomputable def finiteNormComponent (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L →* IsDedekindDomain.HeightOneSpectrum.adicCompletion K v

theorem finiteNormComponent_mem_integers_almost_all (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (b : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) in Filter.cofinite, (finiteNormComponent K L v) b ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v

noncomputable def finiteAdeleNormHom (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L →* IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K

theorem finiteNormComponent_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : L) : (finiteNormComponent K L v) ((algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x) = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.norm K) x)

theorem finiteAdeleNormHom_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (x : L) : (finiteAdeleNormHom K L) ((algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x) = (algebraMap K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)) ((Algebra.norm K) x)

noncomputable def adeleNormHom (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : NumberField.AdeleRing (NumberField.RingOfIntegers L) L →* NumberField.AdeleRing (NumberField.RingOfIntegers K) K

theorem adeleNormHom_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (x : L) : (adeleNormHom K L) ((algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) x) = (algebraMap K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K)) ((Algebra.norm K) x)

noncomputable def ideleNorm (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : Ideles.IdeleGroup L →* Ideles.IdeleGroup K

theorem ideleNorm_principalIdeles (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (x : Lˣ) : (ideleNorm K L) ((Ideles.principalIdeleEmb L) x) = (Ideles.principalIdeleEmb K) ((Units.map (Algebra.norm K)) x)

noncomputable def ideleNormCK (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : Ideles.IdeleClassGroup L →* Ideles.IdeleClassGroup K

theorem ideleNormCK_compat (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (a : Ideles.IdeleGroup L) : (ideleNormCK K L) ↑a = ↑((ideleNorm K L) a)