fromMiddle

Mathlib.CategoryTheory.Sites.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddle

Lean4

/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
and `B ⟶ X` is an arrow of `S`. This is the hom `B ⟶ X`, as an arrow. -/
noncomputable def fromMiddle {X : C} {S : J.Cover X} {T : ∀ I : S.Arrow, J.Cover I.Y} (I : (S.bind T).Arrow) :
    S.Arrow :=
  ⟨_, I.fromMiddleHom, I.from_middle_condition⟩

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

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

Разделы

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

Аффилиация

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