English
The free functor F: Set -> AddCommGrp preserves monomorphisms. In particular, if f: X → Y is injective, then F(f): F(X) → F(Y) is a monomorphism in AddCommGrp.
Русский
Свободный функтор F: множество → свободные аддитивные коммутативные группы сохраняет моно morphisms. В частности, если f: X → Y инъективен, то F(f): F(X) → F(Y) моно в категории AddCommGrp.
LaTeX
$$$\operatorname{Mono}(f) \implies \operatorname{Mono}(F(f)).$$$
Lean4
instance : (free.{u}).PreservesMonomorphisms where
preserves {X Y} f
_ := by
by_cases hX : IsEmpty X
· constructor
intros
apply (IsInitial.isInitialObj free _ ((Types.initial_iff_empty X).2 hX).some).isZero.eq_of_tgt
· push_neg at hX
have hf : Function.Injective f := by rwa [← mono_iff_injective]
obtain ⟨g, hg⟩ := hf.hasLeftInverse
have : IsSplitMono f := IsSplitMono.mk' { retraction := g }
infer_instance
