hom_ext — Mathlib

English

Two morphisms f,g: X ⟶ Y are equal if their φ f n coincide for every n ∈ ℕ.

Русский

Две стрелки f,g: X → Y равны, если их компоненты φ f n совпадают для всех n∈ℕ.

LaTeX

$$$\forall n, \phi(f,n) = \phi(g,n) \Rightarrow f = g$$$

Lean4

theorem hom_ext (f g : X ⟶ Y) (h : ∀ n : ℕ, s.φ f n = s.φ g n) : f = g :=
  by
  ext ⟨Δ⟩
  apply s.hom_ext'
  intro A
  induction Δ using SimplexCategory.rec with
  | _ n
  dsimp
  simp only [s.cofan_inj_comp_app, h]

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