instSmallPullback₁OfIsStableUnderBaseChange

English

If E is a ZeroHypercover over S with Small, and f: T → S is a base change that is stable under base change for J (and has pullbacks), then the pullback of E along f is Small.

Русский

Если E — нулевой гиперохват над S с малостью, и f: T → S — базовое изменение, стабилизируемое по отношению к J и имеющее притяжения, тогда вытянутый по f гиперохват EAlso мал.

LaTeX

$$$\\forall f:\\, T\\to S,\\; (HasPullback\\;f\\; (E_i))\\;\\Rightarrow\\; ZeroHypercover.Small(E.pullback_1 f)$$$

Lean4

instance (E : ZeroHypercover.{w} J S) [ZeroHypercover.Small.{w'} E] {T : C} (f : T ⟶ S) [IsStableUnderBaseChange.{w} J]
    [IsStableUnderBaseChange.{w'} J] [∀ (i : E.I₀), HasPullback f (E.f i)] :
    ZeroHypercover.Small.{w'} (E.pullback₁ f) :=
  by
  use Small.Index E, Small.restrictFun E
  have _ (i) : HasPullback f (E.restrictIndexOfSmall.f i) := by dsimp; infer_instance
  exact ((restrictIndexOfSmall.{w'} E).pullback₁ f).mem₀

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