instSmall — Mathlib

English

Every ZeroHypercover E over S admits a Small structure; i.e., there is a Small instance for E.

Русский

Любое нулевое гиперохватие E над S имеет малую структуру; существует малый инстанс для E.

LaTeX

$$$\\forall E: J.ZeroHypercover(S),\\; ZeroHypercover.Small(E)$$$

Lean4

instance (E : ZeroHypercover.{w} J S) : ZeroHypercover.Small.{max u v} E where
  exists_restrictIndex_mem := by
    obtain ⟨ι, Y, f, h⟩ := E.presieve₀.exists_eq_ofArrows
    have (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g) : ∃ (j : E.I₀) (h : Z = E.X j), g = eqToHom h ≫ E.f j :=
      by
      obtain ⟨j⟩ : E.presieve₀ g := by rwa [h]
      use j, rfl
      simp
    choose j h₁ h₂ using this
    refine ⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩
    convert E.mem₀
    exact le_antisymm (fun Z g ⟨i⟩ ↦ ⟨_⟩) (h ▸ fun Z g ⟨i⟩ ↦ .mk' i (h₁ _ _ _) (h₂ _ _ _))

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