eq_δ_of_mono — Mathlib

English

If θ: ⦋n⦌ ⟶ ⦋n+1⦌ is mono, then there exists i with θ = δ_i.

Русский

Если θ: ⦋n⦌ ⟶ ⦋n+1⦧ моно, то существует i такое что θ = δ_i.

LaTeX

$$$\\\\forall n: \\\\mathbb{N},\\\\forall θ: \\\\langle n \\\\rangle \\\\to \\\\langle n+1 \\\\rangle,[\\\\text{Mono } θ] \\\Rightarrow \\\\exists i: \\\\mathrm{Fin}(n+2), θ = δ_i$$$

Lean4

theorem eq_δ_of_mono {n : ℕ} (θ : ⦋n⦌ ⟶ ⦋n + 1⦌) [Mono θ] : ∃ i : Fin (n + 2), θ = δ i :=
  by
  obtain ⟨i, θ', h⟩ :=
    eq_comp_δ_of_not_surjective θ
      (by
        rw [← epi_iff_surjective]
        grind [→ le_of_epi])
  use i
  haveI : Mono (θ' ≫ δ i) := by
    rw [← h]
    infer_instance
  haveI := CategoryTheory.mono_of_mono θ' (δ i)
  rw [h, eq_id_of_mono θ', Category.id_comp]

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