relrank_comap_comap_eq_relrank_of_surjective

English

Another formulation: surjectivity implies relrank of comaps equals relrank of originals.

Русский

Сюръективность порождает равенство relrank для комапов и оригиналов.

LaTeX

$$$\text{surjective}(f) \Rightarrow \operatorname{relrank}(A \operatorname{comap} f, B \operatorname{comap} f) = \operatorname{relrank}(A, B)$$$

Lean4

theorem relrank_comap_comap_eq_relrank_of_surjective {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E)
    (h : Function.Surjective f) : relrank (A.comap f) (B.comap f) = relrank A B := by
  simpa using lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h

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