bijective_of_surjective — Mathlib

English

Canonical endomorphism map from the base ring to endomorphisms of M is a bijection for invertible M.

Русский

Каноническое отображение из базового кольца в концевые отображения модуля M биективно, когда M обратим.

LaTeX

$$$\operatorname{toModuleEnd}_R(M): R \to \operatorname{End}_R(M) \text{ is bijective}$$$

Lean4

theorem bijective_of_surjective [Module.Invertible R N] {f : M →ₗ[R] N} (hf : Function.Surjective f) :
    Function.Bijective f := by
  simpa [lTensor_bijective_iff] using
    bijective_self_of_surjective (f.lTensor _ ∘ₗ (linearEquiv R M).symm.toLinearMap)
      (by simpa [lTensor_surjective_iff] using hf)

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