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 f (E.f i)`. -/
@[simps toPreZeroHypercover]
noncomputable def pullback₁ [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : ZeroHypercover.{w} J T)
    [∀ i, HasPullback f (E.f i)] : J.ZeroHypercover S
    where
  __ := E.toPreZeroHypercover.pullback₁ f
  mem₀ :=
    J.mem_coverings_of_isPullback E.f E.mem₀ f _ (fun _ ↦ pullback.snd _ _) fun i ↦ IsPullback.of_hasPullback f (E.f i)

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

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

Разделы

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

Аффилиация

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