epiOfEffectiveEpi — Mathlib

English

Every effective epi morphism is an epimorphism: the epi property holds for f when it is effective epi.

Русский

Любой эффективный эпиморфизм является эпиморфизмом: свойство эпима для f при условии эффективной эпиморфии.

LaTeX

$$Epi f$$

Lean4

instance epiOfEffectiveEpi {X Y : C} (f : Y ⟶ X) [EffectiveEpi f] : Epi f :=
  by
  constructor
  intro W m₁ m₂ h
  have : m₂ = EffectiveEpi.desc f (f ≫ m₂) (fun {Z} g₁ g₂ h => by simp only [← Category.assoc, h]) :=
    EffectiveEpi.uniq _ _ _ _ rfl
  rw [this]
  exact EffectiveEpi.uniq _ _ _ _ h

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