lift_rank_le_of_injective_injective

English

If M ≅ M' as modules and the scalar action matches, then the ranks coincide.

Русский

Если M и M' эквивалентны как модули и скалярное действие согласуется, то их ранги совпадают.

LaTeX

$$$\operatorname{rank}_R M = \operatorname{rank}_{R'} M'$$$

Lean4

/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map which sends non-zero elements to
non-zero elements, `j : M →+ M'` is an injective group 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 [AddCommGroup M'] [Module R' M'] (i : R' → R) (j : M →+ M')
    (hi : ∀ r, i r = 0 → r = 0) (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 (fun _ _ ↦ hj <| by rwa [j.map_zero]) hc⟩,
        lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

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