effectiveEpiFamily_of_effectiveEpi_epi_comp

English

If f: α → X a ⟶ B, g: α → Y a ⟶ X a with epi(g a) for all a, and Y with EffectiveEpiFamily X π, then the family X and f is effective from the epi composition g a ≫ f a.

Русский

Если для каждого a эпиморфизм g(a) и EffectiveEpiFamily Y через g a ≫ f a, тогда EffectiveEpiFamily X f.

LaTeX

$$$\forall a,\operatorname{Epi}(g(a)) \wedge \operatorname{EffectiveEpiFamily}(Y,f(a)) \Rightarrow \operatorname{EffectiveEpiFamily}(X,f)$$$

Lean4

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

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