lift_cardinalMk_eq_trdeg — Mathlib

English

If x is a transcendence basis of A over R, then the cardinality of the index type equals the transcendence degree: lift #ι = lift (trdeg R A).

Русский

Если x — трансцендентный базис A над R, то кардинал числа элементов индексов равен трансцендентному размеру: lift #ι = lift (trdeg R A).

LaTeX

$$$ (\\text{hx} : IsTranscendenceBasis R x) \\Rightarrow \\mathrm{lift}.#ι = \\mathrm{lift}.(\\operatorname{trdeg} R A) $$$

Lean4

theorem lift_cardinalMk_eq_trdeg (hx : IsTranscendenceBasis R x) : lift.{w} #ι = lift.{u} (trdeg R A) :=
  by
  have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.1.algebraMap_injective
  rw [← matroid_cRank_eq, ← ((matroid_isBase_iff).mpr hx.to_subtype_range).cardinalMk_eq_cRank,
    lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩]

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