surjective_comp_right_iff_injective

English

For γ nontrivial, the map g ↦ g ∘ f is surjective iff f is injective.

Русский

Для ненулевого γ отображение g ↦ g ∘ f сюръективно тогда и только тогда, когда f инъективна.

LaTeX

$$$\operatorname{Surjective}(\lambda g: \beta \to \gamma.\ g \circ f) \iff \operatorname{Injective}(f)$$$

Lean4

theorem surjective_comp_right_iff_injective {γ : Type*} [Nontrivial γ] :
    Surjective (fun g : β → γ ↦ g ∘ f) ↔ Injective f := by
  classical
  refine ⟨not_imp_not.mp fun not_inj surj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩, (·.surjective_comp_right)⟩
  simp only [Injective, not_forall] at not_inj
  have ⟨a₁, a₂, eq, ne⟩ := not_inj
  have ⟨f, hf⟩ := surj (if · = a₂ then c else c')
  have h₁ := congr_fun hf a₁
  have h₂ := congr_fun hf a₂
  simp only [comp_apply, if_neg ne, reduceIte] at h₁ h₂
  rw [← h₁, eq, h₂]

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