eq_σ_of_epi — Mathlib

English

If θ: ⟦n+1⟧ ⟶ ⟦n⟧ is epi, then there exists i such that θ = σ_i.

Русский

Если θ: ⟦n+1⟧ ⟶ ⟦n⟧ эпиморфизм, то существует i так, что θ = σ_i.

LaTeX

$$$\\\\forall n \\\\big(\\\\theta: \\\\langle n+1 \\\\rangle \\\\to \\\\langle n \\\\rangle \\\\big), [\\\\text{Epi } \\\\theta] \\\Rightarrow \\\\exists i: \\\\mathrm{Fin}(n+1), \\\\theta = σ_i$$$

Lean4

theorem eq_σ_of_epi {n : ℕ} (θ : ⦋n + 1⦌ ⟶ ⦋n⦌) [Epi θ] : ∃ i : Fin (n + 1), θ = σ i :=
  by
  obtain ⟨i, θ', h⟩ :=
    eq_σ_comp_of_not_injective θ
      (by
        rw [← mono_iff_injective]
        grind [→ le_of_mono])
  use i
  haveI : Epi (σ i ≫ θ') := by
    rw [← h]
    infer_instance
  haveI := CategoryTheory.epi_of_epi (σ i) θ'
  rw [h, eq_id_of_epi θ', Category.comp_id]

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