trivial

Mathlib.CategoryTheory.Sites.Hypercover.One

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.OneHypercover.trivial

Lean4

/-- The trivial `1`-hypercover of `S` where a single component `S`. -/
@[simps toPreOneHypercover]
def trivial (S : C) : OneHypercover.{w} J S
    where
  __ := PreOneHypercover.trivial S
  mem₀ := by simp only [PreOneHypercover.sieve₀_trivial, J.top_mem]
  mem₁ _ _ _ _ _
    h :=
    by
    simp only [PreOneHypercover.trivial_toPreZeroHypercover, PreZeroHypercover.singleton_X,
      PreZeroHypercover.singleton_f, Category.comp_id] at h
    subst h
    simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru