pullback_top — Mathlib

English

Let f be any morphism Y → X in a category. The pullback of the indiscrete (top) sieve on X along f is the indiscrete sieve on Y.

Русский

Пусть f : Y → X — любая морфизм в категории. Обратное по f верхнего (indiscrete) сита на X равно верхнему ситу на Y.

LaTeX

$$$ (\\top_X) \\\\ pullback \\\\ f = \\top_Y $$$

Lean4

@[simp]
theorem pullback_top {f : Y ⟶ X} : (⊤ : Sieve X).pullback f = ⊤ :=
  top_unique fun _ _ => id

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