lift_trdeg_le_of_injective — Mathlib

English

If f: A →ₐ[R] A' is injective, then lift(trdeg_R A) ≤ lift(trdeg_R A').

Русский

Если f: A →ₐ[R] A' инъективно, то подъем трансцендентной степени не меньше для A' чем для A.

LaTeX

$$$\\text{lift}.(\\operatorname{trdeg}_R A) \\le \\text{lift}.(\\operatorname{trdeg}_R A')$$$

Lean4

theorem lift_trdeg_le_of_injective (f : A →ₐ[R] A') (hf : Injective f) :
    lift.{v'} (trdeg R A) ≤ lift.{v} (trdeg R A') :=
  by
  nontriviality R
  rw [trdeg, lift_iSup (bddAbove_range _)]
  exact ciSup_le' fun i ↦ (i.2.map' hf).lift_cardinalMk_le_trdeg

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