instEffectiveEpiFamilyCompOfIsSplitEpi

English

If each g(a) is split epi and X π is an effective epi family, then Y a ↦ g(a) ≫ f(a) forms an effective epi family.

Русский

Если каждый g(a) является разложимой эпиморфией и X π образует эффективное эпиморфное семейство, тогда Y a ↦ g(a) ∘ f(a) образует эффективное эпиморфное семейство.

LaTeX

$$$\forall a,\operatorname{IsSplitEpi}(g(a))\quad\wedge\quad \operatorname{EffectiveEpiFamily}(X,\pi)\Rightarrow \operatorname{EffectiveEpiFamily}(Y,\,a\mapsto g(a)\circ f(a))$$$

Lean4

instance {α : Type*} {B : C} {X Y : α → C} (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ a, IsSplitEpi (g a)]
    [EffectiveEpiFamily _ f] : EffectiveEpiFamily _ (fun a ↦ g a ≫ f a) :=
  ⟨⟨effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi f g⟩⟩

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