lift_relrank_comap — Mathlib

English

For a field homomorphism f, the lift of relrank(A.comap f, B) equals the lift of relrank(A, B.map f).

Русский

Для отображения f подъём relrank(A.comap f, B) равен подъёму relrank(A, B.map f).

LaTeX

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

Lean4

theorem lift_relrank_comap (f : L →+* E) (B : Subfield L) :
    lift.{v} (relrank (A.comap f) B) = lift.{w} (relrank A (B.map f)) :=
  (lift_relrank_map_map _ _ f).symm.trans <|
    congr_arg lift <|
      relrank_eq_of_inf_eq <| by rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]

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