lift_rank_le_of_injective — Mathlib

English

Given a linear map f and the identity ring, the lifted rank of the source does not exceed the lifted rank of the target.

Русский

Для линейного отображения f и отображения, являющегося тождеством на кольцах, подъём ранга исходного пространства не превышает подъема ранга целевого пространства.

LaTeX

$$$\operatorname{lift}(\operatorname{rank}_R M) \le \operatorname{lift}(\operatorname{rank}_R M')$$$

Lean4

theorem lift_rank_le_of_injective (f : M →ₗ[R] M') (i : Injective f) :
    Cardinal.lift.{v'} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R M') :=
  lift_rank_le_of_injective_injectiveₛ (RingHom.id R) f (fun _ _ h ↦ h) i f.map_smul

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