multiplicativeClosure

Mathlib.CategoryTheory.MorphismProperty.Composition

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

Lean4

/-- Given a morphism property `W`, the `multiplicativeClosure W` is the smallest
multiplicative property greater than or equal to `W`. -/
inductive multiplicativeClosure (W : MorphismProperty C) : MorphismProperty C
  | of {x y : C} (f : x ⟶ y) (hf : W f) : multiplicativeClosure W f
  | id (x : C) : multiplicativeClosure W (𝟙 x)
  |
  comp_of {x y z : C} (f : x ⟶ y) (g : y ⟶ z) (hf : multiplicativeClosure W f) (hg : W g) :
    multiplicativeClosure W (f ≫ g)

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

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

Разделы

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

Аффилиация

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