lift_rank_comap — Mathlib

English

For a field homomorphism f: L → E over F, the lifted rank of (A.comap f) over L equals the lifted relrank of A against f.fieldRange.

Русский

Для гомоморфизма полей f: L → E над F поднятая размерность (A.comap f) над L равна поднятой относительной степени A к f.fieldRange.

LaTeX

$$$\operatorname{lift}(\operatorname{rank}(A \operatorname{comap} f, L)) = \operatorname{lift}(\operatorname{relrank}(A, f.fieldRange))$$$

Lean4

theorem lift_rank_comap (f : L →ₐ[F] E) :
    Cardinal.lift.{v} (Module.rank (A.comap f) L) = Cardinal.lift.{w} (relrank A f.fieldRange) :=
  A.toSubfield.lift_rank_comap f.toRingHom

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