pullback — Mathlib

English

Pullback equips a functor J.pullback f: J.Cover X ⥤ J.Cover Y sending each cover S to its pullback along f and mapping refinements to their pullback refinements.

Русский

Вытягивание по f задаёт функтор J.pullback f: J.Cover X ⥤ J.Cover Y, отправляющий каждое покрытие S в S.pullback f и отображающий уточнения в соответствующие вытягивания.

LaTeX

$$$\mathrm{pullback}(f): J.Cover X \to J.Cover Y$ with $\mathrm{obj}(S) = S.pullback f$ and $\mathrm{map}$ induced by monotone pullbacks.$$

Lean4

/-- Pull back a cover along a morphism. -/
@[simps obj]
def pullback (f : Y ⟶ X) : J.Cover X ⥤ J.Cover Y
    where
  obj S := S.pullback f
  map f := (Sieve.pullback_monotone _ f.le).hom

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