lift_relrank_map_map — Mathlib

English

For a field homomorphism f, relrank is preserved under mapping by f up to lifting.

Русский

При отображении ф-и поля relrank сохраняется под отображением f до подъёма кардиналов.

LaTeX

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

Lean4

theorem lift_relrank_map_map (f : E →+* L) : lift.{v} (relrank (A.map f) (B.map f)) = lift.{w} (relrank A B) :=
  -- typeclass inference is slow

  .symm <|
    Algebra.lift_rank_eq_of_equiv_equiv
      (((A ⊓ B).equivMapOfInjective f f.injective).trans <| .subringCongr <| by rw [← map_inf]; rfl)
      (B.equivMapOfInjective f f.injective) rfl

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