comp

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreZeroHypercover.Hom.comp

Lean4

/-- Composition of refinement morphisms of pre-`0`-hypercovers. -/
@[simps]
def comp (f : E.Hom F) (g : F.Hom G) : E.Hom G where
  s₀ := g.s₀ ∘ f.s₀
  h₀ i := f.h₀ i ≫ g.h₀ _

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

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

Разделы

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

Аффилиация

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