mem_inducedTopology_sieves_iff — Mathlib

English

Let G: C → D be a functor between categories equipped with Grothendieck topologies J on C and K on D. The induced topology on C via G is defined so that a sieve S on X belongs to this induced topology exactly when its pushforward along G is a covering sieve in K on G(X).

Русский

Пусть G: C → D — функтор между категориями, на C и D заданы топологии Гротендий (J и K соответственно). Вводимая по G топология на C определяется так, что сита (решётка) S на X принадлежит этой топологии тогда и только тогда, когда образ S по G является покрывающей решёткой в K на G(X).

LaTeX

$$$S \\in (G.\\mathrm{inducedTopology}\,K)\\,X \\;\\Longleftrightarrow\\; (S.\\mathrm{functorPushforward}\\, G) \\in K (G\\.obj X)$$$

Lean4

@[simp]
theorem mem_inducedTopology_sieves_iff {X : C} (S : Sieve X) :
    S ∈ (G.inducedTopology K) X ↔ (S.functorPushforward G) ∈ K (G.obj X) :=
  Iff.rfl

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