finite_of_discr_bdd_of_isComplex — Mathlib

English

Same as 152014, reaffirming finiteness under Real place and discriminant bound.

Русский

То же, что и в 152014, повторяющее конечность при реальном месте и ограничении дискриминанта.

LaTeX

$$$$\\text{(Real place finiteness statement)}$$$$

Lean4

theorem finite_of_discr_bdd_of_isComplex :
    {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F } |
        haveI : NumberField K := @NumberField.mk _ _ inferInstance K.prop
        {w : InfinitePlace K | IsComplex 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 (sqrt (1 + B ^ 2)) 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 < (convexBodyLT'Factor K) * boundOfDiscBdd N
    by
    obtain ⟨x, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isComplex 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 [val_eq_coe, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_max, NNReal.coe_one, Real.coe_sqrt, NNReal.coe_add 1,
          NNReal.coe_one, NNReal.coe_pow]
        gcongr
        · exact le_max_right _ 1
        · exact rank_le_rankOfDiscrBdd hK₂
        · rw [NNReal.coe_natCast, Nat.cast_le]
          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]
    _ ≤ convexBodyLT'Factor K * B := by gcongr; exact mod_cast one_le_convexBodyLT'Factor K

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