functorialSurjectiveInjectiveFactorizationData

Mathlib.CategoryTheory.ConcreteCategory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ConcreteCategory.functorialSurjectiveInjectiveFactorizationData

Lean4

/-- A concrete category with strong epi mono factorizations and such that
the forget functor preserves mono and epi admits functorial surjective/injective
factorizations. -/
noncomputable def functorialSurjectiveInjectiveFactorizationData : FunctorialSurjectiveInjectiveFactorizationData C :=
  (functorialEpiMonoFactorizationData C).ofLE (by rw [surjective_eq_epimorphisms]) (by rw [injective_eq_monomorphisms])

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

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

Разделы

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

Аффилиация

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