PullbackCompatible — Mathlib

English

For presieve of arrows, its IsSheafFor is equivalent to IsSheafFor with PullbackCompatibility when HasPairwisePullbacks holds.

Русский

Для пресивы стрелок IsSheafFor эквивалентно IsSheafFor через PullbackCompatible при условии HasPairwisePullbacks.

LaTeX

$$$(ofArrows X π).IsSheafFor P \iff (∀ x, Arrows.PullbackCompatible P π x → \exists! t, ∀ i, P.map(π_i).op t = x_i)$$$

Lean4

/-- A more explicit version of `FamilyOfElements.PullbackCompatible` for a `Presieve.ofArrows`.
-/
def PullbackCompatible (x : (i : I) → P.obj (op (X i))) : Prop :=
  ∀ i j, P.map (pullback.fst (π i) (π j)).op (x i) = P.map (pullback.snd (π i) (π j)).op (x j)

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