effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi

Mathlib.CategoryTheory.EffectiveEpi.Comp

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

Lean4

/-- An effective epi family precomposed with a family of split epis is effective epimorphic.
-/
noncomputable def effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi {α : Type*} {B : C} {X Y : α → C}
    (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ a, IsSplitEpi (g a)] [EffectiveEpiFamily _ f] :
    EffectiveEpiFamilyStruct _ (fun a ↦ g a ≫ f a) :=
  effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi' f g (fun a ↦ section_ (g a)) (fun a ↦ IsSplitEpi.id (g a))

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

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

Разделы

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

Аффилиация

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