effectiveEpiFamilyStructSingletonOfEffectiveEpi

Mathlib.CategoryTheory.EffectiveEpi.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi

Lean4

/-- An `EffectiveEpiFamily` consisting of a single `EffectiveEpi`
-/
noncomputable def effectiveEpiFamilyStructSingletonOfEffectiveEpi {B X : C} (f : X ⟶ B) [EffectiveEpi f] :
    EffectiveEpiFamilyStruct (fun () ↦ X) (fun () ↦ f)
    where
  desc e h := EffectiveEpi.desc f (e ()) (fun g₁ g₂ hg ↦ h () () g₁ g₂ hg)
  fac e h := fun _ ↦ EffectiveEpi.fac f (e ()) (fun g₁ g₂ hg ↦ h () () g₁ g₂ hg)
  uniq e h m hm := by apply EffectiveEpi.uniq f (e ()) (h () ()); exact hm ()

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

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

Разделы

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

Аффилиация

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