def termD_𝔸 : Lean.ParserDescr

D_𝔸 is notation for D ⊗[K] 𝔸_K.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Df (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Type (max u_2 u_1)

Df is notation for D ⊗ 𝔸_K^∞

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Type (max u_2 u_1)

Dfx is notation for (D ⊗ 𝔸_K^∞)ˣ.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Type (max u_2 u_1)

Dinf is notation for D ⊗ 𝔸_K^∞

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Dinfx (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Type (max u_2 u_1)

Dinfx is notation for (D ⊗ 𝔸_K^∞)ˣ

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.incl (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Dˣ →* (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ

The inclusion Dˣ → D_𝔸ˣ as a group homomorphism.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁ (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Dˣ →* Dfx K D

The inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.incl_Kn_𝔸Kn (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : (Fin (Module.finrank K D) → K) → Fin (Module.finrank K D) → AdeleRing (RingOfIntegers K) K

The inclusion of K^n into 𝔸^n.

noncomputable instance NumberField.AdeleRing.DivisionAlgebra.Aux.instAlgebraRealDinf (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Algebra ℝ (Dinf K D)

The ℝ-algebra structure on Dinf K D.

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instIsScalarTowerRealInfiniteAdeleRingDinf (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] : IsScalarTower ℝ (InfiniteAdeleRing K) (Dinf K D)

noncomputable instance NumberField.AdeleRing.DivisionAlgebra.Aux.instMeasurableSpaceTensorProductRingOfIntegers_fLT (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : MeasurableSpace (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

We put the Borel measurable space structure on D_𝔸 in this file.

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceTensorProductRingOfIntegers_fLT (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : BorelSpace (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instFiniteRealDinf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Module.Finite ℝ (Dinf K D)

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instIsModuleTopologyRealDinf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsModuleTopology ℝ (Dinf K D)

Dinf K D has the ℝ-module topology.

noncomputable instance NumberField.AdeleRing.DivisionAlgebra.Aux.instMeasurableSpaceDinf (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : MeasurableSpace (Dinf K D)

Dinf K D is given the borel sigma algebra (for Haar measure).

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDinf (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : BorelSpace (Dinf K D)

noncomputable instance NumberField.AdeleRing.DivisionAlgebra.Aux.instMeasurableSpaceDf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : MeasurableSpace (Df K D)

Df K D is given the borel sigma algebra (for Haar measure).

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instBorelSpaceDf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : BorelSpace (Df K D)

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instSecondCountableTopologyDinf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : SecondCountableTopology (Dinf K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Kn_discrete (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] (x : Fin (Module.finrank K D) → K) : ∃ (U : Set (Fin (Module.finrank K D) → AdeleRing (RingOfIntegers K) K)), IsOpen U ∧ incl_Kn_𝔸Kn K D ⁻¹' U = {x}

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D_iso (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : D ≃ₗ[K] Fin (Module.finrank K D) → K

The K-algebra equivalence of D and K^n.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_iso (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : TensorProduct K D (AdeleRing (RingOfIntegers K) K) ≃ₗ[AdeleRing (RingOfIntegers K) K] Fin (Module.finrank K D) → AdeleRing (RingOfIntegers K) K

The 𝔸_K-algebra equivalence of D_𝔸 and 𝔸_K^d.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_iso_top (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : TensorProduct K D (AdeleRing (RingOfIntegers K) K) ≃L[AdeleRing (RingOfIntegers K) K] Fin (Module.finrank K D) → AdeleRing (RingOfIntegers K) K

The topological 𝔸_K-linear equivalence D_𝔸 ≃ 𝔸_K^d.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete_aux (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (U : Set (Fin (Module.finrank K D) → AdeleRing (RingOfIntegers K) K)) : incl_Kn_𝔸Kn K D ⁻¹' U = ⇑(D_iso K D) '' (⇑(D𝔸_iso_top K D) ∘ ⇑Algebra.TensorProduct.includeLeft ⁻¹' U)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (x : D) : ∃ (U : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))), IsOpen U ∧ ⇑Algebra.TensorProduct.includeLeft ⁻¹' U = {x}

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.includeLeft_subgroup (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : AddSubgroup (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

The additive subgroup D of D_𝔸.

instance NumberField.AdeleRing.DivisionAlgebra.Aux.discrete_includeLeft_subgroup (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : DiscreteTopology ↑(includeLeft_subgroup K D).carrier

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instT2SpaceTensorProductRingOfIntegers_fLT (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : T2Space (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

instance NumberField.AdeleRing.DivisionAlgebra.Aux.discrete_principalSubgroup (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↑↑(principalSubgroup (RingOfIntegers K) K)

instance NumberField.AdeleRing.DivisionAlgebra.Aux.compact_includeLeft_subgroup (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : CompactSpace (TensorProduct K D (AdeleRing (RingOfIntegers K) K) ⧸ includeLeft_subgroup K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.not_injective_of_large_measure (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : ∃ (B : NNReal), ∀ (U : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))), IsOpen U → ↑B < MeasureTheory.Measure.addHaar U → ¬Set.InjOn QuotientAddGroup.mk U

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : TensorProduct K D (AdeleRing (RingOfIntegers K) K) ≃ₐ[K] Dinf K D × Df K D

The K-algebra isomorphism D_𝔸 ≃ D_∞ × D_f -- adelic D is infinite adele D times finite adele D.

noncomputable instance NumberField.AdeleRing.DivisionAlgebra.Aux.instModuleRingOfIntegersProdDinfDf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : Module (AdeleRing (RingOfIntegers K) K) (Dinf K D × Df K D)

The (InfiniteAdeleRing K × FiniteAdeleRing (𝓞 K) K)-module structure on (Dinf K D × Df K D).

instance NumberField.AdeleRing.DivisionAlgebra.Aux.instIsModuleTopologyRingOfIntegersProdDinfDf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsModuleTopology (AdeleRing (RingOfIntegers K) K) (Dinf K D × Df K D)

(Dinf K D × Df K D) has the 𝔸_K module topology.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight' (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : TensorProduct K D (AdeleRing (RingOfIntegers K) K) ≃ₗ[AdeleRing (RingOfIntegers K) K] Dinf K D × Df K D

The 𝔸_K linear map D_𝔸 ≃ D_∞ × D_f.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight'' (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : TensorProduct K D (AdeleRing (RingOfIntegers K) K) ≃ₜ+ Dinf K D × Df K D

The continuous additive isomorphism D_𝔸 ≃ D_∞ × D_f.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight_units (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ ≃* Dinfx K D × Dfx K D

The equivalence of the units of D_𝔸 and the product of the units of (D ⊗ 𝔸_K^f) and (D ⊗ 𝔸_K^∞).

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.smul_D𝔸_prodRight_symm (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] (a : (Dinf K D)ˣ) (b : (Df K D)ˣ) (di : Dinf K D) (df : Df K D) : (D𝔸_prodRight_units K D).symm (a, b) • (D𝔸_prodRight K D).symm (di, df) = (D𝔸_prodRight K D).symm (a • di, b • df)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight_units_cont (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Continuous ⇑(D𝔸_prodRight_units K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸 (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (a : Dinfx K D) (b : Dfx K D) : MeasureTheory.ringHaarChar ((D𝔸_prodRight_units K D).symm (a, b)) = MeasureTheory.ringHaarChar (MulEquiv.prodUnits.symm (a, b))

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (r : ℝ) (h : r > 0) : ∃ (ρ : ℝˣ), ↑(MeasureTheory.ringHaarChar ((D𝔸_prodRight_units K D).symm ((Units.map ↑(algebraMap ℝ (Dinf K D))) ρ, 1))) = r

For any positive real r, there's some ρ ∈ ℝˣ such that the haar character of (ρ, 1) ∈ D_f × D_∞ is r.

instance NumberField.InfiniteAdeleRing.instSecondCountableTopologyTensorProductCompletion_fLT (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (vi : InfinitePlace K) : SecondCountableTopology (TensorProduct K D vi.Completion)

theorem NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [(vi : InfinitePlace K) → MeasurableSpace (TensorProduct K D vi.Completion)] [∀ (vi : InfinitePlace K), BorelSpace (TensorProduct K D vi.Completion)] [Algebra.IsCentral K D] (u : ((vi : InfinitePlace K) → TensorProduct K D vi.Completion)ˣ) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u) = MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulRight u)

Left and right Haar characters agree for u : (Π vi : InfinitePlace K, (D ⊗[K] vi.Completion))ˣ.

noncomputable def NumberField.InfiniteAdeleRing.real_to_completion (K : Type u_1) [Field K] (vi : InfinitePlace K) : ℝ →+* vi.Completion

The canonical ℝ-algebra structure on InfinitePlace.Completion.

noncomputable instance NumberField.InfiniteAdeleRing.instAlgebraRealCompletion_fLT (K : Type u_1) [Field K] (vi : InfinitePlace K) : Algebra ℝ vi.Completion

theorem NumberField.InfiniteAdeleRing.algebraMap_completion_def (K : Type u_1) [Field K] (vi : InfinitePlace K) : algebraMap ℝ vi.Completion = real_to_completion K vi

instance NumberField.InfiniteAdeleRing.instFiniteRealCompletion_fLT (K : Type u_1) [Field K] (vi : InfinitePlace K) : Module.Finite ℝ vi.Completion

instance NumberField.InfiniteAdeleRing.instContinuousSMulRealCompletion_fLT (K : Type u_1) [Field K] (vi : InfinitePlace K) : ContinuousSMul ℝ vi.Completion

instance NumberField.InfiniteAdeleRing.instIsModuleTopologyRealCompletion_fLT (K : Type u_1) [Field K] (vi : InfinitePlace K) : IsModuleTopology ℝ vi.Completion

noncomputable instance NumberField.InfiniteAdeleRing.instAlgebraRealTensorProductCompletion_fLT (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] (vi : InfinitePlace K) : Algebra ℝ (TensorProduct K D vi.Completion)

instance NumberField.InfiniteAdeleRing.instIsScalarTowerRealCompletionTensorProduct_fLT (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] (vi : InfinitePlace K) : IsScalarTower ℝ vi.Completion (TensorProduct K D vi.Completion)

instance NumberField.InfiniteAdeleRing.instIsModuleTopologyRealTensorProductCompletion_fLT (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (vi : InfinitePlace K) : IsModuleTopology ℝ (TensorProduct K D vi.Completion)

instance NumberField.InfiniteAdeleRing.instIsModuleTopologyRealForallTensorProductCompletion_fLT (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsModuleTopology ℝ ((vi : InfinitePlace K) → TensorProduct K D vi.Completion)

theorem NumberField.InfiniteAdeleRing.algebraMap_completion (K : Type u_1) [Field K] {vi : InfinitePlace K} {x : ℝ} : (algebraMap ℝ (InfiniteAdeleRing K)) x vi = (algebraMap ℝ vi.Completion) x

theorem NumberField.InfiniteAdeleRing.tensorPi_equiv_piTensor_map_mul (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] {x y : AdeleRing.DivisionAlgebra.Aux.Dinf K D} : (tensorPi_equiv_piTensor K D InfinitePlace.Completion) (x * y) = (tensorPi_equiv_piTensor K D InfinitePlace.Completion) x * (tensorPi_equiv_piTensor K D InfinitePlace.Completion) y

noncomputable def NumberField.InfiniteAdeleRing.Dinf_tensorPi_equiv_piTensor_aux (K : Type u_1) [Field K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : AdeleRing.DivisionAlgebra.Aux.Dinf K D ≃ₗ[ℝ] (vi : InfinitePlace K) → TensorProduct K D vi.Completion

tensorPi_equiv_piTensor applied to Dinf, as a ℝ-linear equiv.

noncomputable def NumberField.InfiniteAdeleRing.Dinf_tensorPi_equiv_piTensor (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : AdeleRing.DivisionAlgebra.Aux.Dinf K D ≃L[ℝ] (vi : InfinitePlace K) → TensorProduct K D vi.Completion

tensorPi_equiv_piTensor applied to Dinf, as a continuous ℝ-linear equiv.

noncomputable def NumberField.InfiniteAdeleRing.Dinf_tensorPi_equiv_piTensor_mulEquiv (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : AdeleRing.DivisionAlgebra.Aux.Dinf K D ≃* ((vi : InfinitePlace K) → TensorProduct K D vi.Completion)

tensorPi_equiv_piTensor applied to Dinf, as a mul equiv.

theorem NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] (u : (AdeleRing.DivisionAlgebra.Aux.Dinf K D)ˣ) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u) = MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulRight u)

noncomputable def NumberField.AdeleRing.instTopologicalSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : TopologicalSpace (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) D)

We give 𝔸_K^f ⊗ D the 𝔸_K^f-module topology.

noncomputable def NumberField.AdeleRing.instMeasurableSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : MeasurableSpace (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) D)

We give 𝔸_K^f ⊗ D the Borel measurable space structure.

theorem NumberField.AdeleRing.instBorelSpaceTensorProductFiniteAdeleRingRingOfIntegers_fLT (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] : BorelSpace (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) D)

theorem NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] (u : (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u) = MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulRight u)

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.Uf (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set (TensorProduct K D (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K))

An auxiliary compact subset of D_𝔸^f with nonempty interior

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Uf.spec (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (Uf K D) ∧ Uf K D ∈ nhds 0

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.Ui (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set (TensorProduct K D (InfiniteAdeleRing K))

An auxiliary compact subset of D_∞ with nonempty interior

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Ui.spec (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (Ui K D) ∧ Ui K D ∈ nhds 0

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.Efamily (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (r : ℝ) : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

An auxiliary definition of an increasing family of compact subsets of D_𝔸, defined as the product of a compact neighbourhood of 0 at the finite places and a compact neighbourhood of 0, scaled by r, at the infinite places.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_compact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (r : ℝ) : IsCompact (Efamily K D r)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_nonempty_interior (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : (interior (Efamily K D 1)).Nonempty

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_unbounded (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (B : NNReal) : ∃ (r : ℝ), MeasureTheory.Measure.addHaar (Efamily K D r) > ↑B

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.existsE (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : ∃ (E : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))), IsCompact E ∧ ∀ (φ : TensorProduct K D (AdeleRing (RingOfIntegers K) K) ≃ₜ+ TensorProduct K D (AdeleRing (RingOfIntegers K) K)), MeasureTheory.addEquivAddHaarChar φ = 1 → ∃ e₁ ∈ E, ∃ e₂ ∈ E, e₁ ≠ e₂ ∧ φ e₁ - φ e₂ ∈ Set.range ⇑Algebra.TensorProduct.includeLeft

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.E (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

An auxiliary set E used in the proof of Fujisaki's lemma.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.E_compact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (E K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_left (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] {x : (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ} (h : x ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))) : ∃ e₁ ∈ E K D, ∃ e₂ ∈ E K D, e₁ ≠ e₂ ∧ ↑x * e₁ - ↑x * e₂ ∈ Set.range ⇑Algebra.TensorProduct.includeLeft

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_right (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] {x : (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ} (h : x ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))) : ∃ e₁ ∈ E K D, ∃ e₂ ∈ E K D, e₁ ≠ e₂ ∧ e₁ * ↑x⁻¹ - e₂ * ↑x⁻¹ ∈ Set.range ⇑Algebra.TensorProduct.includeLeft

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.X (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

An auxiliary set X used in the proof of Fukisaki's lemma. Defined as E - E.

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.Y (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))

An auxiliary set Y used in the proof of Fukisaki's lemma. Defined as X * X.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (X K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (Y K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] {β : (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ} (hβ : β ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))) : ∃ x ∈ X K D, ∃ d ∈ Set.range ⇑(incl K D), ↑β * x = ↑d

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel' (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] {β : (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ} (hβ : β ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))) : ∃ x ∈ X K D, ∃ d ∈ Set.range ⇑(incl K D), x * ↑β⁻¹ = ↑d

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.T (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ

An auxiliary set T used in the proof of Fukisaki's lemma. Defined as Y ∩ Dˣ.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite_extracted1 (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (Y K D ∩ Set.range ⇑Algebra.TensorProduct.includeLeft)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : (T K D).Finite

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.C (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set (TensorProduct K D (AdeleRing (RingOfIntegers K) K) × TensorProduct K D (AdeleRing (RingOfIntegers K) K))

An auxiliary set C used in the proof of Fukisaki's lemma. Defined as T⁻¹X × X.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (C K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] {β : (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ˣ} (hβ : β ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))) : ∃ b ∈ Set.range ⇑(incl K D), ∃ ν ∈ MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K)), β = b * ν ∧ (↑ν, ↑ν⁻¹) ∈ C K D

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂ (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : ↥(MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))) → TensorProduct K D (AdeleRing (RingOfIntegers K) K) × (TensorProduct K D (AdeleRing (RingOfIntegers K) K))ᵐᵒᵖ

The inclusion of ringHaarChar_ker D_𝔸 into the product space D_𝔸 × D_𝔸ᵐᵒᵖ.

noncomputable def NumberField.AdeleRing.DivisionAlgebra.Aux.M (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Set ↥(MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K)))

An auxiliary set used in the proof of compact_quotient'.

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (a : ↥(MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K)))) : Quotient (QuotientGroup.rightRel (Subgroup.comap (MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))).subtype (incl K D).range))

The map from ringHaarChar_ker D_𝔸 to the quotient Dˣ \ ringHaarChar_ker D_𝔸.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_cont (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Continuous (toQuot K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_surjective (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] : toQuot K D '' M K D = Set.univ

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂_isClosedEmbedding (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Topology.IsClosedEmbedding (incl₂ K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.ImAux_isCompact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact ((fun (p : TensorProduct K D (AdeleRing (RingOfIntegers K) K) × TensorProduct K D (AdeleRing (RingOfIntegers K) K)) => (p.1, MulOpposite.op p.2)) '' C K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.M_compact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : IsCompact (M K D)

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁ (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : ↥(MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))) → Dfx K D

The restriction of ringHaarChar_ker D_𝔸 to (D ⊗ 𝔸_K^∞)ˣ via D𝔸_iso_prod_units.

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_continuous (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Continuous (rest₁ K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_aux (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (r : ℝ) (h : r > 0) : ∃ (y : Dinfx K D), ↑(MeasureTheory.ringHaarChar ((D𝔸_prodRight_units K D).symm (y, 1))) = r

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_surjective (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Function.Surjective (rest₁ K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_equivariant (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] (a b : ↥(MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K)))) : (QuotientGroup.rightRel (Subgroup.comap (MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))).subtype (incl K D).range)) a b → ⟦rest₁ K D a⟧ = ⟦rest₁ K D b⟧

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Quotient (QuotientGroup.rightRel (Subgroup.comap (MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))).subtype (incl K D).range)) → Quotient (QuotientGroup.rightRel (incl₁ K D).range)

The obvious map Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D).

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_continuous (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Continuous (incl_D𝔸quot K D)

theorem NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_surjective (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] : Function.Surjective (incl_D𝔸quot K D)

theorem NumberField.AdeleRing.DivisionAlgebra.compact_quotient (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] : CompactSpace (Quotient (QuotientGroup.rightRel (Subgroup.comap (MeasureTheory.ringHaarChar_ker (TensorProduct K D (AdeleRing (RingOfIntegers K) K))).subtype (Aux.incl K D).range)))

Dˣ \ D_𝔸^{(1)} is compact.

theorem NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] : CompactSpace (Quotient (QuotientGroup.rightRel (AdeleRing.DivisionAlgebra.Aux.incl₁ K D).range))

Dˣ \ D_𝔸^fˣ is compact.

If D is a finite-dimensional division K-algebra with centre a number field K then the double coset space Dˣ \ (D ⊗ 𝔸_K^infty)ˣ / U is finite for any open subgroup U of (D ⊗ 𝔸_K^infty)ˣ.

theorem NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset (K : Type u_1) [Field K] [NumberField K] (D : Type u_2) [DivisionRing D] [Algebra K D] [FiniteDimensional K D] [Algebra.IsCentral K D] {U : Subgroup (AdeleRing.DivisionAlgebra.Aux.Dfx K D)} (hU : IsOpen ↑U) : Finite (DoubleCoset.Quotient (Set.range ⇑(AdeleRing.DivisionAlgebra.Aux.incl₁ K D)) ↑U)