subcanonical — Mathlib

English

The coherent topology on a precoherent category is subcanonical.

Русский

Когерентная топология над предкоерентной категорией субканонична.

LaTeX

$$$\mathrm{Subcanonical}(\mathrm{coherentTopology}\ C)$$$

Lean4

/-- The coherent topology on a precoherent category is subcanonical. -/
instance subcanonical : (coherentTopology C).Subcanonical :=
  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj

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