lift_rank_eq_of_surjective — Mathlib

English

Under a base change, the lifted ranks of P and M coincide: lift(rank_T P) = lift(rank_R M).

Русский

При базовом изменении подъем рангов совпадает: lift(rank_T P) = lift(rank_R M).

LaTeX

$$$\operatorname{lift}\big(\operatorname{Module.rank} T P\big) = \operatorname{lift}\big(\operatorname{Module.rank} R M\big)$$$

Lean4

theorem lift_rank_eq_of_surjective {f : M →ₗ[R] M'} (h : Surjective f) :
    lift.{v} (Module.rank R M) = lift.{u} (Module.rank R M') + lift.{v} (Module.rank R (LinearMap.ker f)) := by
  rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]

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