instIsDenseSubsite — Mathlib

English

Under suitable hypotheses, coherent topology is cover-preserving for a functor F between categories.

Русский

При подходящих гипотезах когерентная топология сохраняет покрытие для функторa F между категориями.

LaTeX

$$coverPreserving$$

Lean4

instance :
    haveI := F.reflects_precoherent;
    F.IsDenseSubsite (coherentTopology C) (coherentTopology D)
    where
  functorPushforward_mem_iff := by
    rw [eq_induced F]
    rfl

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