instCompleteSemilatticeSup

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IdealSheafData.instCompleteSemilatticeSup

Lean4

instance : CompleteSemilatticeSup (IdealSheafData X)
    where
  sSup
    s :=
    { ideal := sSup (ideal '' s),
      map_ideal_basicOpen :=
        by
        have : sSup (ideal '' s) = ⨆ i : s, ideal i.1 :=
          by
          conv_lhs => rw [← Subtype.range_val (s := s), ← Set.range_comp]
          rfl
        simp only [this, iSup_apply, Ideal.map_iSup, map_ideal_basicOpen, implies_true] }
  le_sSup s x hxs := le_sSup (s := ideal '' s) ⟨_, hxs, rfl⟩
  sSup_le s i hi := sSup_le (s := ideal '' s) (Set.forall_mem_image.mpr hi)

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

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

Разделы

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

Аффилиация

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