isTranscendenceBasis_of_lift_trdeg_le

English

If hx is a transcendence basis, lift_trdeg equality holds and deduces equality under certain conditions.

Русский

Если hx — базис трансцендентности, выполняются соответствующие равенства для lift_trdeg и выводы.

LaTeX

$$$ (lx) \\Rightarrow (IsTranscendenceBasis R x) $$$

Lean4

theorem isTranscendenceBasis_of_lift_trdeg_le (hx : AlgebraicIndependent R x) (fin : trdeg R A < ℵ₀)
    (le : lift.{u} (trdeg R A) ≤ lift.{w} #ι) : IsTranscendenceBasis R x :=
  by
  have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.algebraMap_injective
  rw [← matroid_cRank_eq, ← Matroid.rankFinite_iff_cRank_lt_aleph0] at fin
  exact
    .of_subtype_range hx.injective <|
      matroid_indep_iff.mpr hx.to_subtype_range |>.isBase_of_cRank_le <|
        lift_le.mp <| (matroid_cRank_eq R A ▸ le).trans_eq (mk_range_eq_of_injective hx.injective).symm

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