lift_relrank_comap_comap_eq_lift_relrank_inf

English

The lifted relrank of (A.comap f) with (B.comap f) equals the lift of relrank of A with B inf f.fieldRange.

Русский

Поднятый relrank (A.comap f) с (B.comap f) равен поднятому relrank(A,B ∩ f.fieldRange).

LaTeX

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

Lean4

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

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