Monomorphisms in the category of groups
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Eléonore Mangel.
Created on 2022-04-25.
Last modified on 2023-09-26.
module group-theory.monomorphisms-groups where
Imports
open import category-theory.monomorphisms-in-large-precategories open import foundation.propositions open import foundation.universe-levels open import group-theory.groups open import group-theory.homomorphisms-groups open import group-theory.isomorphisms-groups open import group-theory.precategory-of-groups
Idea
A group homomorphism f : x → y
is a monomorphism if whenever we have two group
homomorphisms g h : w → x
such that f ∘ g = f ∘ h
, then in fact g = h
. The
way to state this in Homotopy Type Theory is to say that postcomposition by f
is an embedding.
Definition
module _ {l1 l2 : Level} (l3 : Level) (G : Group l1) (H : Group l2) (f : hom-Group G H) where is-mono-Group-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3) is-mono-Group-Prop = is-mono-prop-Large-Precategory Group-Large-Precategory l3 G H f is-mono-Group : UU (l1 ⊔ l2 ⊔ lsuc l3) is-mono-Group = type-Prop is-mono-Group-Prop is-prop-is-mono-Group : is-prop is-mono-Group is-prop-is-mono-Group = is-prop-type-Prop is-mono-Group-Prop
Properties
Isomorphisms are monomorphisms
module _ {l1 l2 : Level} (l3 : Level) (G : Group l1) (H : Group l2) (f : type-iso-Group G H) where is-mono-iso-Group : is-mono-Group l3 G H (hom-iso-Group G H f) is-mono-iso-Group = is-mono-iso-Large-Precategory Group-Large-Precategory l3 G H f
Recent changes
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-05-06. Egbert Rijke. Big cleanup continued (#597).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).