hasSheafComposeEssentiallySmallSite

English

An equivalence yields that the inverse functor is dense subsite with respect to the target topology.

Русский

Эквивалентность делает обратнофунктор плотным подсайтом по отношению к целевой топологии.

LaTeX

$$$e.functor.IsDenseSubsite J K e.inverse$$$

Lean4

instance hasSheafComposeEssentiallySmallSite : HasSheafCompose J F :=
  (equivSmallModel C).hasSheafCompose J ((equivSmallModel C).inverse.inducedTopology J) F

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