lift_relrank_comap_comap_eq_lift_relrank_inf

English

For f, A, B, we have lift(relrank(A.comap f, B.comap f)) = lift(relrank(A, B ⊓ f.fieldRange)).

Русский

Для f, A, B выполнено: подъём relrank(A.comap f, B.comap f) = подъём relrank(A, B ⊓ f.fieldRange).

LaTeX

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

Lean4

theorem lift_relrank_comap_comap_eq_lift_relrank_inf (f : L →+* E) :
    lift.{v} (relrank (A.comap f) (B.comap f)) = lift.{w} (relrank A (B ⊓ f.fieldRange)) :=
  by
  conv_lhs => rw [← lift_relrank_map_map _ _ f, map_comap_eq, map_comap_eq]
  congr 1
  apply relrank_eq_of_inf_eq
  rw [inf_assoc, inf_left_comm _ B, inf_of_le_left (le_refl _)]

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