mono_of_mono — Mathlib

English

If f is an epi morphism in the base category and f.f (the underlying morphism) is epi, then f is an epi in the structured category of Endofunctor.Algebra.

Русский

Если f — эпиморфизм в базовой категории, и f.f является эпиморфизмом, то f — эпиморфизм в категории Algebra над концевым функтором.

LaTeX

$$$\\forall {C} [\\mathbf{Category C}] {F : \\mathbf{Functor} C\\; C} {X Y : \\text{Endofunctor.Algebra} F} (f : X \\to Y) [Epi f.f] , Epi f$$

Lean4

/-- An algebra morphism with an underlying monomorphism hom in `C` is an algebra monomorphism. -/
theorem mono_of_mono {X Y : Algebra F} (f : X ⟶ Y) [h : Mono f.1] : Mono f :=
  (forget F).mono_of_mono_map h

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