comp_mem_iff

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.comp_mem_iff

← MathLib Explorer

English

If i is an isomorphism, then S(arrows (i ∘ f)) equals S(arrows f).

Русский

Если i — изоморфизм, то S.arrows(i ∘ f) = S.arrows(f).

LaTeX

$$S.arrows (i ∘ f) = S.arrows f$$

Lean4

@[simp]
theorem comp_mem_iff (i : X ⟶ Y) (f : Y ⟶ Z) [IsIso i] (S : Sieve Z) : S (i ≫ f) ↔ S f :=
  by
  refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
  convert S.downward_closed H (inv i)
  simp

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

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

Разделы

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

Аффилиация

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