leastExt — Mathlib

English

For each i, the element φ(i) is the least index k such that b_k does not lie in the subfield E⟮<i⟯ generated by earlier basis elements.

Русский

Для каждого i элемент φ(i) есть минимальный индекс k, такой что b_k не лежит в подполе, порождаемом ранее заданными базисными элементами.

LaTeX

$$$$\\forall i,\\; IsLeast\\{k \\mid b_k \\notin E\\langle< i\\rangle\\}(\\varphi(i))$$$$

Lean4

/-- `leastExt i` is defined to be the smallest `k : ι` that generates a nontrivial extension over
(i.e. does not lie in) the subalgebra (= intermediate field) generated by all previous
`leastExt j`, `j < i`. For cardinality reasons, such `k` always exist if `ι` is infinite. -/
def leastExt : ι → ι :=
  wellFounded_lt.fix fun i ih ↦
    let s := range fun j : Iio i ↦ b (ih j j.2)
    wellFounded_lt.min {k | b k ∉ adjoin F s} <|
      by
      rw [← compl_setOf, nonempty_compl]; by_contra!
      simp_rw [eq_univ_iff_forall, mem_setOf] at this
      have := adjoin_le_iff.mpr (range_subset_iff.mpr this)
      rw [adjoin_basis_eq_top, ← eq_top_iff] at this
      apply_fun Module.rank F at this
      refine ne_of_lt ?_ this
      let _ : AddCommMonoid (⊤ : IntermediateField F E) := inferInstance
      conv_rhs => rw [topEquiv.toLinearEquiv.rank_eq]
      have := mk_Iio_ord_toType i
      obtain eq | lt := rank_inf.out.eq_or_lt
      · replace this := mk_lt_aleph0_iff.mp (this.trans_eq eq.symm)
        have : FiniteDimensional F (adjoin F s) :=
          finiteDimensional_adjoin fun x _ ↦ (IsAlgebraic.isAlgebraic x).isIntegral
        exact (Module.rank_lt_aleph0 _ _).trans_eq eq
      ·
        exact
          (Subalgebra.equivOfEq _ _ <|
                adjoin_algebraic_toSubalgebra fun x _ ↦ IsAlgebraic.isAlgebraic x) |>.toLinearEquiv.rank_eq.trans_lt <|
            (Algebra.rank_adjoin_le _).trans_lt (max_lt (mk_range_le.trans_lt this) lt)

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