lift_cardinalMk_eq_max_lift — Mathlib

English

For a transcendence basis x over F in E, the rank of E over F matches the maximal lift of ranks.

Русский

Для базы трансцендентности x над F в E ранг E над F равен максимальному подъему рангов.

LaTeX

$$$\\text{IsTranscendenceBasis } F x \\Rightarrow \\mathrm{Module.rank}\\, F\\, E = \\#E$$$

Lean4

theorem lift_cardinalMk_eq_max_lift {F : Type u} {E : Type v} [CommRing F] [Nontrivial F] [CommRing E] [IsDomain E]
    [Algebra F E] {ι : Type w} {x : ι → E} [Nonempty ι] (hx : IsTranscendenceBasis F x) :
    lift.{max u w} #E = lift.{max v w} #F ⊔ lift.{max u v} #ι ⊔ ℵ₀ :=
  by
  let K := Algebra.adjoin F (Set.range x)
  suffices #E = #K by simp [K, this, ← lift_mk_eq'.2 ⟨hx.1.aevalEquiv.toEquiv⟩]
  haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic
  refine le_antisymm ?_ (mk_le_of_injective Subtype.val_injective)
  haveI : Infinite K := hx.1.aevalEquiv.infinite_iff.1 inferInstance
  simpa only [sup_eq_left.2 (aleph0_le_mk K)] using Algebra.IsAlgebraic.cardinalMk_le_max K E

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