algebra_epi_of_epi — Mathlib

English

If an algebra morphism X → Y has an epimorphic carrier map f.f in C, then f is an epimorphism in the algebra category.

Русский

Если морфизм алгебр X → Y имеет эпиморфную carrier-часть f.f в C, то f является эпиморфизмом в категории алгебр.

LaTeX

$$$\\\\forall X,Y \\\\in \\\\mathrm{Alg}(T), \\\\forall f: X \\\\to Y, \\\\operatorname{Epi}(f.f) \\\\Rightarrow \\\\operatorname{Epi}(f).$$$

Lean4

/-- Given an algebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.
-/
theorem algebra_epi_of_epi {X Y : Algebra T} (f : X ⟶ Y) [h : Epi f.f] : Epi f :=
  (forget T).epi_of_epi_map h

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