lift_rank_le_of_injective_injectiveₛ

English

If an infinite family is linearly independent, then aleph-null is below the rank.

Русский

Если существует бесконечная линейно независимая семейство, то ℵ0 не превосходит ранг.

LaTeX

$$$\aleph_0 \le \operatorname{rank}_R(M)$$$

Lean4

/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is an injective map
non-zero elements, `j : M →+ M'` is an injective monoid homomorphism, such that the scalar
multiplications on `M` and `M'` are compatible, then the rank of `M / R` is smaller than or equal to
the rank of `M' / R'`. As a special case, taking `R = R'` it is
`LinearMap.lift_rank_le_of_injective`. -/
theorem lift_rank_le_of_injective_injectiveₛ (i : R' → R) (j : M →+ M') (hi : Injective i) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M') :=
  by
  simp_rw [Module.rank, lift_iSup (bddAbove_range _)]
  exact
    ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦
      ⟨⟨j '' s, LinearIndepOn.id_image (h.linearIndependent.map_of_injective_injectiveₛ i j hi hj hc)⟩,
        lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

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