W

Mathlib.CategoryTheory.Localization.Bousfield

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.LeftBousfield.W

Lean4

/-- Given `P : ObjectProperty C`, this is the class of morphisms `f : X ⟶ Y`
such that for all `Z : C` such that `P Z`, the precomposition with `f` induces
a bijection `(Y ⟶ Z) ≃ (X ⟶ Z)`. -/
def W : MorphismProperty C := fun _ _ f => ∀ Z, P Z → Function.Bijective (fun (g : _ ⟶ Z) => f ≫ g)

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

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

Разделы

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

Аффилиация

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