lift_cardinalMk_eq — Mathlib

English

For any R, A with a transcendence basis x, the cardinal of ι equals the transcendence degree trdeg R A when lifted.

Русский

Для любых R, A с трансцендентным базисом x кардинал множества индексов ι равен транзцендентному размеру A над R после поднятия.

LaTeX

$$$ \\forall {ι} {x : ι \\to A}, IsTranscendenceBasis R x \\rightarrow (#ι).lift = (trdeg R A).lift $$$

Lean4

/-- Any two transcendence bases of a domain `A` have the same cardinality.
May fail if `A` is not a domain; see https://mathoverflow.net/a/144580. -/
@[stacks 030F]
theorem lift_cardinalMk_eq (hx : IsTranscendenceBasis R x) (hy : IsTranscendenceBasis R y) :
    lift.{u'} #ι = lift.{u} #ι' := by
  rw [← lift_inj.{_, w}, lift_lift, lift_lift, ← lift_lift.{w, u'}, hx.lift_cardinalMk_eq_trdeg, ← lift_lift.{w, u},
    hy.lift_cardinalMk_eq_trdeg, lift_lift, lift_lift]

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