English
In the OrzechProperty setting, if i: N → M is injective and f: N → M is surjective, then f is injective.
Русский
В рамках свойства Ореха, если i: N → M инъективно, а f: N → M сюръективно, то f — инъективно.
LaTeX
$$If $i$ is injective and $f$ is surjective, then $f$ is injective.$$
Lean4
theorem injective_of_surjective_of_injective {N : Type w} [AddCommMonoid N] [Module R N] (i f : N →ₗ[R] M)
(hi : Injective i) (hf : Surjective f) : Injective f :=
by
obtain ⟨n, g, hg⟩ := Module.Finite.exists_fin' R M
haveI := small_of_surjective hg
letI := Equiv.addCommMonoid (equivShrink M).symm
letI := Equiv.module R (equivShrink M).symm
let j : Shrink.{u} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
haveI := Module.Finite.equiv j.symm
let i' := j.symm.toLinearMap ∘ₗ i
replace hi : Injective i' := by simpa [i'] using hi
let f' := j.symm.toLinearMap ∘ₗ f ∘ₗ (LinearEquiv.ofInjective i' hi).symm.toLinearMap
replace hf : Surjective f' := by simpa [f'] using hf
simpa [f'] using injective_of_surjective_of_submodule' f' hf
