of_injective — Mathlib

English

If N is isotypic to S and f: M → N is injective, then M isotypic to S.

Русский

Если N изотипичен к S и линейное вложение f: M → N инъективно, то M изотипичен к S.

LaTeX

$$$IsIsotypicOfType(R, N, S) \land (f : M \to N) \text{ injective} \Rightarrow IsIsotypicOfType(R, M, S)$$$

Lean4

theorem of_injective (h : IsIsotypicOfType R N S) (f : M →ₗ[R] N) (inj : Function.Injective f) :
    IsIsotypicOfType R M S := fun m ↦
  have em := m.equivMapOfInjective f inj
  have := IsSimpleModule.congr em.symm
  ⟨em.trans (h (m.map f)).some⟩

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