Bounded algebraic integers lying in an intermediate field inject into the bounded integers of that field. Every archimedean place of the subfield is obtained by restricting an ambient place.

def CCDN.boundedIntegersInSubfield (K : Type u_1) [Field K] [NumberField K] (L : IntermediateField ℚ K) (B : ℝ) : Set (NumberField.RingOfIntegers K)

The algebraic integers of K bounded by B at every infinite place that lie in the intermediate field L.

Equations

• CCDN.boundedIntegersInSubfield K L B = {β : NumberField.RingOfIntegers K | β ∈ CCDN.boundedArchimedeanIntegers K B ∧ ↑β ∈ L}

theorem CCDN.boundedIntegersInSubfield_finite (K : Type u_1) [Field K] [NumberField K] (L : IntermediateField ℚ K) (B : ℝ) : (boundedIntegersInSubfield K L B).Finite

The set boundedIntegersInSubfield K L B is finite.

def CCDN.boundedIntegerToSubfield (K : Type u_1) [Field K] [NumberField K] (L : IntermediateField ℚ K) (B : ℝ) : ↑(boundedIntegersInSubfield K L B) → ↑(boundedArchimedeanIntegers (↥L) B)

The map sending a bounded algebraic integer of K lying in L to the same element viewed as a bounded algebraic integer of L; every infinite place of L is restricted from one of K.

Equations

• CCDN.boundedIntegerToSubfield K L B β = ⟨⟨⟨↑↑β, ⋯⟩, ⋯⟩, ⋯⟩

@[simp]

theorem CCDN.boundedIntegerToSubfield_coe (K : Type u_1) [Field K] [NumberField K] (L : IntermediateField ℚ K) (B : ℝ) (β : ↑(boundedIntegersInSubfield K L B)) : ↑↑↑(boundedIntegerToSubfield K L B β) = ↑↑β

The map boundedIntegerToSubfield does not change the underlying element of K.

theorem CCDN.boundedIntegersInSubfield_count (K : Type u_1) [Field K] [NumberField K] (L : IntermediateField ℚ K) {B : ℝ} (hB : 0 ≤ B) : ↑(boundedIntegersInSubfield K L B).ncard ≤ (2 * √↑(Module.finrank ℚ ↥L) * B + 1) ^ Module.finrank ℚ ↥L

For B ≥ 0, the number of algebraic integers of K bounded by B at every infinite place and lying in L is at most (2 * √m * B + 1) ^ m, where m = [L : ℚ].