lift_rank_eq_max_lift — Mathlib

English

Under a transcendence basis, there is an equality expressing the rank in terms of cardinals and lift operations.

Русский

При базисе трансцендентности существует равенство ранга через кардиналы и операции подъёма.

LaTeX

$$$\\text{IsTranscendenceBasis } F x \\Rightarrow \\mathrm{Module.rank}\\, F\\, E = \\mathrm{lift}(\\#F) \\lor \\mathrm{lift}(\\iota) \\lor \\aleph_0$$$

Lean4

theorem lift_rank_eq_max_lift {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {ι : Type w} {x : ι → E}
    [Nonempty ι] (hx : IsTranscendenceBasis F x) :
    lift.{max u w} (Module.rank F E) = lift.{max v w} #F ⊔ lift.{max u v} #ι ⊔ ℵ₀ :=
  by
  let K := IntermediateField.adjoin F (Set.range x)
  haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic_field
  rw [← rank_mul_rank F K E, lift_mul, ← hx.1.aevalEquivField.toLinearEquiv.lift_rank_eq, MvRatFunc.rank_eq_max_lift,
    lift_max, lift_max, lift_lift, lift_lift, lift_aleph0]
  refine
    mul_eq_left le_sup_right
      ((lift_le.2 ((rank_le_card K E).trans (Algebra.IsAlgebraic.cardinalMk_le_max K E))).trans_eq ?_)
      (by simp [rank_pos.ne'])
  simp [K, ← lift_mk_eq'.2 ⟨hx.1.aevalEquivField.toEquiv⟩]

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