mono_iff_injective — Mathlib

English

Let A,B be representations of G over k and f: A → B a morphism. Then f is a monomorphism in Rep k G if and only if the underlying map f.hom is injective.

Русский

Пусть A, B — представления G над k и f: A → B — морфизм. Тогда f является мономорфизмом в Rep_k(G) тогда и только тогда, когда attaching f.hom инъективна.

LaTeX

$$$\mathrm{Mono}(f) \iff \operatorname{Injective}(f_{\mathrm{hom}})$$$

Lean4

theorem mono_iff_injective {A B : Rep k G} (f : A ⟶ B) : Mono f ↔ Function.Injective f.hom :=
  ⟨fun _ => (ModuleCat.mono_iff_injective ((forget₂ _ _).map f)).1 inferInstance, fun h =>
    (forget₂ _ _).mono_of_mono_map ((ModuleCat.mono_iff_injective <| (forget₂ _ _).map f).2 h)⟩

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