finite_of_discr_bdd_of_isReal — Mathlib

English

For fixed N, the set of number fields K (in a fixed ambient algebra) with a real place and |discr K| ≤ N is finite.

Русский

При фиксированном N множество полей K (в фиксированном окружении) с действительным вложением и |дискр K| ≤ N конечно.

LaTeX

$$$$\\{K : {\\mathbb{Q} \\text{-field} \\mid |\\operatorname{discr} K| \\le N \\} \\text{ with a Real place} \\}.\\text{Finite}$$$$

Lean4

theorem finite_of_discr_bdd_of_isReal :
    {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F } |
        haveI : NumberField K := @NumberField.mk _ _ inferInstance K.prop
        {w : InfinitePlace K | IsReal w}.Nonempty ∧ |discr K| ≤ N}.Finite :=
  by
  classical
    -- The bound on the degree of the generating polynomials

  let D := rankOfDiscrBdd N
  let B := boundOfDiscBdd N
  let C := Nat.ceil ((max B 1) ^ D * Nat.choose D (D / 2))
  refine
    finite_of_finite_generating_set A _ (bUnion_roots_finite (algebraMap ℤ A) D (Set.finite_Icc (-C : ℤ) C))
      (fun ⟨K, hK₀⟩ ⟨hK₁, hK₂⟩ ↦ ?_)
        -- We now need to prove that each field is generated by an element of the union of the root set

  simp_rw [Set.mem_iUnion]
    -- this is purely an optimization

  have : CharZero K := SubsemiringClass.instCharZero K
  haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀
  obtain ⟨w₀, hw₀⟩ := hK₁
  suffices minkowskiBound K ↑1 < (convexBodyLTFactor K) * B
    by
    obtain ⟨x, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isReal K hw₀ this
    have hx := x.isIntegral_coe
    refine ⟨x, ⟨⟨minpoly ℤ (x : K), ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩
    · exact natDegree_le_rankOfDiscrBdd hK₂ x hx₁
    · rw [Set.mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
      refine
        (Eq.trans_le ?_ <|
              Embeddings.coeff_bdd_of_norm_le ((le_iff_le (x : K) _).mp (fun w ↦ le_of_lt (hx₂ w))) i).trans
          ?_
      ·
        rw [minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx, coeff_map, eq_intCast, Int.norm_cast_rat,
          Int.norm_eq_abs, Int.cast_abs]
      · refine le_trans ?_ (Nat.le_ceil _)
        rw [show max ↑(max (B : ℝ≥0) 1) (1 : ℝ) = max (B : ℝ) 1 by simp, val_eq_coe, NNReal.coe_mul, NNReal.coe_pow,
          NNReal.coe_max, NNReal.coe_one, NNReal.coe_natCast]
        gcongr
        · exact le_max_right _ 1
        · exact rank_le_rankOfDiscrBdd hK₂
        · exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans (Nat.choose_le_middle _ _)
    · refine mem_rootSet.mpr ⟨minpoly.ne_zero hx, ?_⟩
      exact (aeval_algebraMap_eq_zero_iff A (x : K) _).mpr (minpoly.aeval ℤ (x : K))
    · rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁
      convert hx₁
      · simp only [IntermediateField.lift_top]
      · simp only [IntermediateField.lift_adjoin, Set.image_singleton]
  calc
    minkowskiBound K 1 < B := minkowskiBound_lt_boundOfDiscBdd hK₂
    _ = 1 * B := by rw [one_mul]
    _ ≤ convexBodyLTFactor K * B := by gcongr; exact mod_cast one_le_convexBodyLTFactor K

Похожие утверждения