pullback₂

Mathlib.CategoryTheory.Sites.Hypercover.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Precoverage.ZeroHypercover.pullback₂

Lean4

/-- Pullback of a `0`-hypercover along a morphism. The components are `pullback (E.f i) f`. -/
@[simps toPreZeroHypercover]
noncomputable def pullback₂ [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : ZeroHypercover.{w} J T)
    [∀ i, HasPullback (E.f i) f] : J.ZeroHypercover S
    where
  __ := E.toPreZeroHypercover.pullback₂ f
  mem₀ :=
    J.mem_coverings_of_isPullback E.f E.mem₀ f _ (fun _ ↦ pullback.fst _ _) fun i ↦
      (IsPullback.of_hasPullback (E.f i) f).flip

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

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

Разделы

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

Аффилиация

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