equalizer_self

Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.equalizer_self

English

The equalizer of a morphism with itself is the indiscrete (top) sieve; i.e., the equalizer of f with itself equals the top sieve.

Русский

Нулевой эквивалент для равноправного равенства: равнитель равенства f и f равен топ-сиве.

LaTeX

$$$\operatorname{equalizer}(f,f) = \top$$$

Lean4

@[simp]
theorem equalizer_self {U V : C} (f : U ⟶ V) : equalizer f f = ⊤ := by ext; simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru