lift_rank_map_le — Mathlib

English

The rank bound for a map composed with subobjects provides a comparison of ranks between subobjects and ambient modules.

Русский

Граница ранга отображения через композиции подмодулей и модулей задаёт сравнение рангов подмодулей и окружных модулей.

LaTeX

$$$\operatorname{lift}(\operatorname{rank}_R(p^{\prime})) \le \operatorname{lift}(\operatorname{rank}_R(M))$$$

Lean4

theorem lift_rank_map_le (f : M →ₗ[R] M') (p : Submodule R M) :
    Cardinal.lift.{v} (Module.rank R (p.map f)) ≤ Cardinal.lift.{v'} (Module.rank R p) :=
  by
  have h := lift_rank_range_le (f.comp (Submodule.subtype p))
  rwa [LinearMap.range_comp, range_subtype] at h

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