cover_lift — Mathlib

English

If a functor G is J–K cocontinuous, then the pullback of a cover S along G is again a cover in J.

Русский

Если Fунктор G конически непрерывно переносит покрытия, то вытягивание по G сохраняет покрытие.

LaTeX

$$$[G.IsCocontinuous\\ J\\ K]\\forall X\\forall S\\in K(G.obj X): S.functorPullback G \\in J X$$$

Lean4

theorem cover_lift [G.IsCocontinuous J K] {U : C} {S : Sieve (G.obj U)} (hS : S ∈ K (G.obj U)) :
    S.functorPullback G ∈ J U :=
  IsCocontinuous.cover_lift hS

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