English
If an element x satisfies lt-one at all infinite places except w, the generated subalgebra by x is the whole field.
Русский
Если x удовлетворяет условию lt для всех бесконечных мест помимо w, образованная подалгебра Rat(x) равна всему полю.
LaTeX
$$$\text{adjoin } \mathbb{Q}\{x\} = \top$ under LT-type conditions$$
Lean4
theorem _root_.NumberField.is_primitive_element_of_infinitePlace_lt {x : 𝓞 K} {w : InfinitePlace K} (h₁ : x ≠ 0)
(h₂ : ∀ ⦃w'⦄, w' ≠ w → w' x < 1) (h₃ : IsReal w ∨ |(w.embedding x).re| < 1) : ℚ⟮(x : K)⟯ = ⊤ :=
by
rw [Field.primitive_element_iff_algHom_eq_of_eval ℚ ℂ ?_ _ w.embedding.toRatAlgHom]
· intro ψ hψ
have h : 1 ≤ w x := one_le_of_lt_one h₁ h₂
have main : w = InfinitePlace.mk ψ.toRingHom :=
by
simp only [RingHom.toRatAlgHom_apply] at hψ
rw [← norm_embedding_eq, hψ] at h
contrapose! h
exact h₂ h.symm
rw [(mk_embedding w).symm, mk_eq_iff] at main
cases h₃ with
| inl hw =>
rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
exact congr_arg RingHom.toRatAlgHom main
| inr hw =>
refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
have : (embedding w x).im = 0 := by
rw [← Complex.conj_eq_iff_im]
have := RingHom.congr_fun h' x
simp at this
rw [this]
exact hψ.symm
rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero, zero_mul, add_zero,
Complex.norm_real] at h
· exact fun x ↦ IsAlgClosed.splits_codomain (minpoly ℚ x)
