mem_ker_iff — Mathlib

English

For a functor φ, an arrow f lies in the kernel of φ precisely when there exists a morphism between φ.obj c and φ.obj d transporting the identity along some equality h between φ.obj c and φ.obj d, and φ.map f equals this transported identity.

Русский

Для функторa φ стрелка f принадлежит ядру φ тогда и только тогда, когда существует мороморфизм между φ.obj c и φ.obj d, переносящий тождество по некоторому равенству между этими объектами, и φ.map f равен этому перенесённому тождеству.

LaTeX

$${c d : C} (f : c ⟶ d) : f ∈ (\\ker φ).arrows c d \\iff ∃ h : φ.obj c = φ.obj d, φ.map f = eqToHom h$$

Lean4

theorem mem_ker_iff {c d : C} (f : c ⟶ d) : f ∈ (ker φ).arrows c d ↔ ∃ h : φ.obj c = φ.obj d, φ.map f = eqToHom h :=
  mem_discrete_iff (φ.map f)

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