of_injective — Mathlib

English

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

Русский

Если N изотипичен к S и существует инъективное отображение M → N, то M изотипичен к S.

LaTeX

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

Lean4

theorem of_injective (h : IsIsotypic R N) (f : M →ₗ[R] N) (inj : Function.Injective f) : IsIsotypic R M := fun m _ ↦
  have em := (m.equivMapOfInjective f inj).symm
  have := IsSimpleModule.congr em
  ((h (m.map f)).of_injective f inj).of_linearEquiv_type em

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