rank_le_of_isSMulRegular — Mathlib

English

If f is injective, then the lifted rank of the domain is at most the lifted rank of the codomain.

Русский

Если отображение × инъективно, тогда поднимаемый ранг области не превосходит поднимаемый ранг кодомного пространства.

LaTeX

$$$\operatorname{lift} (\operatorname{Module.rank} R (\operatorname{range} f)) \le \operatorname{lift} (\operatorname{Module.rank} R M)$$$

Lean4

theorem rank_le_of_isSMulRegular {S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M]
    (L L' : Submodule R M) {s : S} (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') :
    Module.rank R L ≤ Module.rank R L' :=
  ((Algebra.lsmul S R M s).restrict h).rank_le_of_injective <| fun _ _ h ↦ by simpa using hr (Subtype.ext_iff.mp h)

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