effectiveEpi_of_effectiveEpi_epi_comp

English

If g: Y → X is epi and g ≫ f is effective epi, then f is effective epi.

Русский

Если g — эпиморфия и g ∘ f — эффективная эпиморфия, тогда f — эффективная эпиморфия.

LaTeX

$$$\operatorname{Epi}(g) \wedge \operatorname{EffectiveEpi}(g \circ f) \Rightarrow \operatorname{EffectiveEpi}(f)$$$

Lean4

theorem effectiveEpi_of_effectiveEpi_epi_comp {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X) [Epi g] [EffectiveEpi (g ≫ f)] :
    EffectiveEpi f :=
  have := (effectiveEpi_iff_effectiveEpiFamily (g ≫ f)).mp inferInstance
  have := effectiveEpiFamily_of_effectiveEpi_epi_comp (X := fun () ↦ X) (Y := fun () ↦ Y) (fun () ↦ f) (fun () ↦ g)
  inferInstance

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