English
A variant of the previous existence result where closed sets are defined only for objects over a fixed index j.
Русский
Вариант предыдущего существования, где замкнутые множества заданы только относительно фиксированного индекса j.
LaTeX
$$$\exists s\in c.pt, \forall i, hij, (c.\pi.app i).base\,s \in Z_i(hij)$$$
Lean4
/-- A variant of `exists_mem_of_isClosed_of_nonempty` where the closed sets are only defined
for the objects over a given `j : I`.
-/
@[stacks 01Z3]
theorem exists_mem_of_isClosed_of_nonempty' [IsCofilteredOrEmpty I] [∀ {i j} (f : i ⟶ j), IsAffineHom (D.map f)] {j : I}
(Z : ∀ (i : I), (i ⟶ j) → Set (D.obj i)) (hZc : ∀ i hij, IsClosed (Z i hij)) (hZne : ∀ i hij, (Z i hij).Nonempty)
(hZcpt : ∀ i hij, IsCompact (Z i hij))
(hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (D.map hi'i).base (Z i' (hi'i ≫ hij)) (Z i hij)) :
∃ (s : c.pt), ∀ i hij, (c.π.app i).base s ∈ Z i hij :=
by
have {i₁ i₂ : Over j} (f : i₁ ⟶ i₂) : IsAffineHom ((Over.forget j ⋙ D).map f) := by dsimp; infer_instance
simpa [Over.forall_iff] using
exists_mem_of_isClosed_of_nonempty (Over.forget j ⋙ D) _
((Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c).symm hc) (fun i ↦ Z i.left i.hom) (fun _ ↦ hZc _ _)
(fun _ ↦ hZne _ _) (fun _ ↦ hZcpt _ _) (fun {i₁ i₂} f ↦ by dsimp; rw [← Over.w f]; exact hstab ..)
