coverage

Mathlib.CategoryTheory.Sites.MorphismProperty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.coverage

Lean4

/-- If `P` is stable under base change, this is the coverage on `C` where covering presieves
are those where every morphism satisfies `P`. -/
@[simps toPrecoverage]
def coverage (P : MorphismProperty C) [P.IsStableUnderBaseChange] [P.HasPullbacks] : Coverage C
    where
  __ := precoverage P
  pullback X Y f S
    hS := by
    have : S.HasPullbacks f := ⟨fun {W} h hh ↦ P.hasPullback _ (hS hh)⟩
    refine ⟨S.pullbackArrows f, ?_, .pullbackArrows f S⟩
    intro Z g ⟨W, a, h⟩
    have := S.hasPullback f h
    exact P.pullback_snd _ _ (hS h)

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

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

Разделы

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

Аффилиация

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