ker_eq_bot_of_mono — Mathlib

English

If f is mono in GrpCat, then its kernel is trivial: ker f = ⊥.

Русский

Если f является моноида-мономорфизмом в GrpCat, то его ядро тривиально: ker f = ⊥.

LaTeX

$$$ \ker f = \bot $$$

Lean4

@[to_additive]
theorem ker_eq_bot_of_mono [Mono f] : f.hom.ker = ⊥ :=
  MonoidHom.ker_eq_bot_of_cancel fun u v h =>
    ConcreteCategory.ext_iff.mp <| (@cancel_mono _ _ _ _ _ f _ (ofHom u) (ofHom v)).1 <| ConcreteCategory.ext h

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