ofTruncSplitMono

Mathlib.CategoryTheory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Groupoid.ofTruncSplitMono

Lean4

/-- A category where every morphism has a `Trunc` retraction is computably a groupoid. -/
noncomputable def ofTruncSplitMono (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)) :
    Groupoid.{v₁} C := by
  apply Groupoid.ofIsIso
  intro X Y f
  have ⟨a, _⟩ := Trunc.exists_rep <| all_split_mono f
  have ⟨b, _⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
  apply IsIso.of_mono_retraction

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

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

Разделы

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

Аффилиация

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