of_zeroHypercover_target — Mathlib

English

If P is local at target K and we have a zero hypercover 𝒰 of Y with small, and for all i, P(pullback.snd f (𝒰.f i)) holds, then P f.

Русский

Если P локально в цели относительно K и 𝒰 — нулевая гиперборка Y; если для всех i выполняется P(pullback.snd f (𝒰.f i)), тогда P f.

LaTeX

$$$P f \iff \forall i, P(pullback.snd f (𝒰.f i))$$$

Lean4

theorem of_zeroHypercover_target {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks] [P.IsLocalAtTarget K]
    {X Y : C} {f : X ⟶ Y} (𝒰 : Precoverage.ZeroHypercover.{w} K Y) [Precoverage.ZeroHypercover.Small.{v} 𝒰]
    (h : ∀ i, P (pullback.snd f (𝒰.f i))) : P f :=
  by
  rw [IsLocalAtTarget.iff_of_zeroHypercover (P := P) 𝒰.restrictIndexOfSmall]
  simp [h]

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