relfinrank_comap_comap_eq_relfinrank_inf

English

If f is surjective, lift of relrank(A.comap f, B.comap f) equals lift of relrank A B.

Русский

Если f сюръективен, поднятый relrank(A.comap f, B.comap f) равен поднятому relrank(A,B).

LaTeX

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

Lean4

theorem relfinrank_comap_comap_eq_relfinrank_inf (f : L →ₐ[F] E) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A (B ⊓ f.fieldRange) := by
  simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))

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