diff --git a/src/elementary-number-theory/field-of-rational-numbers.lagda.md b/src/elementary-number-theory/field-of-rational-numbers.lagda.md
index 88e4a88422..9aef7bc04e 100644
--- a/src/elementary-number-theory/field-of-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/field-of-rational-numbers.lagda.md
@@ -1,6 +1,8 @@
 # The field of rational numbers
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module elementary-number-theory.field-of-rational-numbers where
 ```
 
@@ -9,15 +11,61 @@ module elementary-number-theory.field-of-rational-numbers where
 ```agda
 open import commutative-algebra.discrete-fields
 
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.additive-group-of-rational-numbers
+open import elementary-number-theory.greatest-common-divisor-integers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers
 open import elementary-number-theory.multiplicative-group-of-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-integers
 open import elementary-number-theory.nonzero-rational-numbers
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.reduced-integer-fractions
+open import elementary-number-theory.relatively-prime-integers
+open import elementary-number-theory.ring-of-integers
 open import elementary-number-theory.ring-of-rational-numbers
+open import elementary-number-theory.unit-fractions-rational-numbers
 
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.identity-types
+open import foundation.images
+open import foundation.iterating-automorphisms
+open import foundation.reflecting-maps-equivalence-relations
+open import foundation.unit-type
+open import foundation.universe-levels
+
+open import foundation-core.contractible-maps
+open import foundation-core.contractible-types
+open import foundation-core.coproduct-types
+open import foundation-core.empty-types
+open import foundation-core.equivalences
+open import foundation-core.fibers-of-maps
+open import foundation-core.retractions
+open import foundation-core.sections
+open import foundation-core.sets
+open import foundation-core.subtypes
+open import foundation-core.transport-along-identifications
+
+open import group-theory.cores-monoids
+open import group-theory.groups
+open import group-theory.invertible-elements-monoids
 
 open import ring-theory.division-rings
+open import ring-theory.groups-of-units-rings
+open import ring-theory.homomorphisms-rings
+open import ring-theory.initial-rings
+open import ring-theory.invertible-elements-rings
+open import ring-theory.localizations-rings
+open import ring-theory.rings
+open import ring-theory.semirings
 ```
 
 </details>
@@ -49,3 +97,81 @@ pr2 is-division-ring-ℚ x H = is-invertible-element-ring-is-nonzero-ℚ x (H 
 is-discrete-field-ℚ : is-discrete-field-Commutative-Ring commutative-ring-ℚ
 is-discrete-field-ℚ = is-division-ring-ℚ
 ```
+
+## Properties
+
+### The ring of rational numbers is the [localization](ring-theory.localizations-rings.md) of the ring of [integers](elementary-number-theory.ring-of-integers.md) at the set of [positive integers](elementary-number-theory.positive-integers.md)
+
+```agda
+inverts-positive-integers-ℚ :
+  inverts-subset-hom-Ring ℤ-Ring ring-ℚ subtype-positive-ℤ
+  ( initial-hom-Ring ring-ℚ)
+inverts-positive-integers-ℚ (inr (inr x)) star =
+  is-invertible-element-ring-is-nonzero-ℚ (pr1 (pr1 (initial-hom-Ring ring-ℚ))
+  ( inr (inr x))) lem where
+  lem : is-nonzero-ℚ (pr1 (pr1 (initial-hom-Ring ring-ℚ)) (inr (inr x)))
+  lem =
+    is-nonzero-is-nonzero-numerator-ℚ (pr1 (pr1 (initial-hom-Ring ring-ℚ))
+    ( inr (inr x))) {!   !}
+
+inverts-positive-integers-hom-ℚ :
+  {l : Level} (R : Ring l) → inverts-subset-hom-Ring ℤ-Ring R subtype-positive-ℤ
+  ( initial-hom-Ring R) → hom-Ring ring-ℚ R
+pr1 (pr1 (inverts-positive-integers-hom-ℚ R R-inv)) ((x , y , y>0) , _) =
+  mul-Ring R (map-hom-Ring ℤ-Ring R (initial-hom-Ring R) x)
+  ( inv-is-invertible-element-Ring R (R-inv y y>0))
+pr2 (pr1 (inverts-positive-integers-hom-ℚ R R-inv))
+  {(x , y , y>0) , xy-red} {(z , w , w>0) , zw-red} =
+    {!   !}
+pr1 (pr2 (inverts-positive-integers-hom-ℚ R R-inv))
+  {(x , y , y>0) , xy-red} {(z , w , w>0) , zw-red} =
+    {!   !}
+pr2 (pr2 (inverts-positive-integers-hom-ℚ R R-inv)) = pr1
+  (pr2
+    (R-inv
+      (pr1
+        (pr1
+          (pr1
+            (pr2
+              (multiplicative-monoid-Semiring
+                (semiring-Ring ring-ℚ))))))
+    star))
+
+universal-property-ℚ-ℤ :
+  (l : Level) → universal-property-localization-subset-Ring l ℤ-Ring ring-ℚ
+  subtype-positive-ℤ (initial-hom-Ring ring-ℚ) inverts-positive-integers-ℚ
+pr1 (pr1 (universal-property-ℚ-ℤ l R)) (f , f-inv) =
+  inverts-positive-integers-hom-ℚ R lem where
+  lem : inverts-subset-hom-Ring ℤ-Ring R subtype-positive-ℤ (initial-hom-Ring R)
+  lem =
+    tr (inverts-subset-hom-Ring ℤ-Ring R subtype-positive-ℤ)
+    ( inv (contraction-initial-hom-Ring R f)) f-inv
+pr2 (pr1 (universal-property-ℚ-ℤ l R)) (f , f-inv) =
+  eq-type-subtype (inverts-subset-hom-ring-Prop ℤ-Ring R subtype-positive-ℤ)
+  ( inv (contraction-initial-hom-Ring R (pr1
+  ((precomp-universal-property-localization-subset-Ring ℤ-Ring ring-ℚ
+    R subtype-positive-ℤ (initial-hom-Ring ring-ℚ)
+    inverts-positive-integers-ℚ
+    ∘ pr1 (pr1 (universal-property-ℚ-ℤ l R)))
+    (f , f-inv))))) ∙ eq-type-subtype
+    ( inverts-subset-hom-ring-Prop ℤ-Ring R subtype-positive-ℤ)
+    ( contraction-initial-hom-Ring R f)
+pr1 (pr2 (universal-property-ℚ-ℤ l R)) (f , f-inv) =
+  inverts-positive-integers-hom-ℚ R lem where
+  lem : inverts-subset-hom-Ring ℤ-Ring R subtype-positive-ℤ (initial-hom-Ring R)
+  lem =
+    tr (inverts-subset-hom-Ring ℤ-Ring R subtype-positive-ℤ)
+    ( inv (contraction-initial-hom-Ring R f)) f-inv
+pr2 (pr2 (universal-property-ℚ-ℤ l R)) f =
+  eq-htpy-hom-Ring ring-ℚ R ((pr1 (pr2 (universal-property-ℚ-ℤ l R)) ∘
+    precomp-universal-property-localization-subset-Ring ℤ-Ring ring-ℚ R
+    subtype-positive-ℤ (initial-hom-Ring ring-ℚ)
+    inverts-positive-integers-ℚ)
+    f) f htpy where
+  htpy :
+    htpy-hom-Ring ring-ℚ R ((pr1 (pr2 (universal-property-ℚ-ℤ l R)) ∘
+    precomp-universal-property-localization-subset-Ring ℤ-Ring ring-ℚ R
+    subtype-positive-ℤ
+    (initial-hom-Ring ring-ℚ) inverts-positive-integers-ℚ) f) f
+  htpy ((x , y , y>0) , _) = {!   !}
+```
diff --git a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md
index fc8abf413d..bef19260ad 100644
--- a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md
+++ b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md
@@ -310,7 +310,7 @@ is-commutative-gcd-ℤ x y =
   ap int-ℕ (is-commutative-gcd-ℕ (abs-ℤ x) (abs-ℤ y))
 ```
 
-### `gcd-ℕ 1 b ＝ 1`
+### `gcd-ℤ 1 b ＝ 1`
 
 ```agda
 is-one-is-gcd-one-ℤ : {b x : ℤ} → is-gcd-ℤ one-ℤ b x → is-one-ℤ x
diff --git a/src/elementary-number-theory/integer-fractions.lagda.md b/src/elementary-number-theory/integer-fractions.lagda.md
index 3ee0891636..8e8782a422 100644
--- a/src/elementary-number-theory/integer-fractions.lagda.md
+++ b/src/elementary-number-theory/integer-fractions.lagda.md
@@ -302,3 +302,11 @@ is-countable-fraction-ℤ =
     ( is-countable-ℤ)
     ( is-countable-positive-ℤ)
 ```
+
+### `n / n` is similar to 1
+
+```agda
+is-sim-one-fraction-ℤ :
+  (n : ℤ⁺) → sim-fraction-ℤ ((int-positive-ℤ n) , n) one-fraction-ℤ
+is-sim-one-fraction-ℤ (n , n≠0) = right-unit-law-mul-ℤ n ∙ left-unit-law-mul-ℤ n
+```
diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md
index aa38ca9d21..c773c6ca1f 100644
--- a/src/elementary-number-theory/rational-numbers.lagda.md
+++ b/src/elementary-number-theory/rational-numbers.lagda.md
@@ -7,8 +7,11 @@ module elementary-number-theory.rational-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.absolute-value-integers
 open import elementary-number-theory.divisibility-integers
+open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.greatest-common-divisor-integers
+open import elementary-number-theory.greatest-common-divisor-natural-numbers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
 open import elementary-number-theory.mediant-integer-fractions
@@ -19,6 +22,7 @@ open import elementary-number-theory.positive-integers
 open import elementary-number-theory.reduced-integer-fractions
 
 open import foundation.action-on-identifications-functions
+open import foundation.decidable-equality
 open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.equality-dependent-pair-types
@@ -29,6 +33,7 @@ open import foundation.reflecting-maps-equivalence-relations
 open import foundation.retracts-of-types
 open import foundation.sections
 open import foundation.sets
+open import foundation.subtype-identity-principle
 open import foundation.subtypes
 open import foundation.surjective-maps
 open import foundation.universe-levels
diff --git a/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md b/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md
index 6d3a883ac8..77506b9431 100644
--- a/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md
@@ -12,12 +12,16 @@ module elementary-number-theory.unit-fractions-rational-numbers where
 open import elementary-number-theory.archimedean-property-positive-rational-numbers
 open import elementary-number-theory.inequality-integers
 open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
 open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers
+open import elementary-number-theory.multiplicative-inverses-positive-integer-fractions
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.nonzero-natural-numbers
+open import elementary-number-theory.positive-integers
 open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-integers
@@ -26,7 +30,13 @@ open import elementary-number-theory.strict-inequality-rational-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.dependent-pair-types
+open import foundation.equality-cartesian-product-types
+open import foundation.equality-dependent-pair-types
 open import foundation.functoriality-dependent-pair-types
+open import foundation.unit-type
+
+open import foundation-core.coproduct-types
+open import foundation-core.identity-types
 
 open import group-theory.groups
 ```
@@ -118,3 +128,15 @@ smaller-reciprocal-ℚ⁺ q⁺@(q , _) =
           ( 1<nq)))
     ( bound-archimedean-property-ℚ⁺ q⁺ one-ℚ⁺)
 ```
+
+### For every `n : ℕ⁺`, `n * 1/n = 1`
+
+```agda
+{-
+unit-fraction-is-left-inv-ℚ : (n : ℕ⁺) → mul-ℚ (reciprocal-rational-ℕ⁺ n) (rational-ℕ (nat-ℕ⁺ n)) ＝ one-ℚ
+unit-fraction-is-left-inv-ℚ (n , n>0) = ap rational-fraction-ℤ (eq-pair refl {!   !}) ∙ (eq-ℚ-sim-fraction-ℤ (int-positive-ℤ (positive-int-ℕ⁺ (n , n>0)) , positive-int-ℕ⁺ (n , n>0)) one-fraction-ℤ (is-sim-one-fraction-ℤ (positive-int-ℕ⁺ (n , n>0))) ∙ {!   !})
+
+unit-fraction-is-right-inv-ℚ : (n : ℕ⁺) → mul-ℚ (rational-ℕ (nat-ℕ⁺ n)) (reciprocal-rational-ℕ⁺ n) ＝ one-ℚ
+unit-fraction-is-right-inv-ℚ (n , n>0) = {!   !}
+-}
+```
diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
index 3c5c80aba9..5994dab957 100644
--- a/src/group-theory.lagda.md
+++ b/src/group-theory.lagda.md
@@ -58,6 +58,7 @@ open import group-theory.dependent-products-monoids public
 open import group-theory.dependent-products-semigroups public
 open import group-theory.dihedral-group-construction public
 open import group-theory.dihedral-groups public
+open import group-theory.divisible-groups public
 open import group-theory.e8-lattice public
 open import group-theory.elements-of-finite-order-groups public
 open import group-theory.embeddings-abelian-groups public
@@ -162,6 +163,7 @@ open import group-theory.pullbacks-subsemigroups public
 open import group-theory.quotient-groups public
 open import group-theory.quotient-groups-concrete-groups public
 open import group-theory.quotients-abelian-groups public
+open import group-theory.rational-abelian-groups public
 open import group-theory.rational-commutative-monoids public
 open import group-theory.representations-monoids-precategories public
 open import group-theory.saturated-congruence-relations-commutative-monoids public
diff --git a/src/group-theory/divisible-groups.lagda.md b/src/group-theory/divisible-groups.lagda.md
new file mode 100644
index 0000000000..711b77d02c
--- /dev/null
+++ b/src/group-theory/divisible-groups.lagda.md
@@ -0,0 +1,45 @@
+# Divisible groups
+
+```agda
+module group-theory.divisible-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.surjective-maps
+open import foundation.universe-levels
+
+open import group-theory.groups
+open import group-theory.powers-of-elements-groups
+```
+
+</details>
+
+## Idea
+
+A group `G` is called **divisible** if for every `n : ℕ⁺`, the
+[power-of-`n` map](group-theory.powers-of-elements-groups.md)
+`x ↦ power-Group G n x` is surjective.
+
+## Definition
+
+```agda
+is-divisible-Group : {l : Level} (G : Group l) → UU l
+is-divisible-Group G = (n : ℕ⁺) → is-surjective (power-Group G (nat-ℕ⁺ n))
+
+is-prop-is-divisible-Group :
+  {l : Level} (G : Group l) → is-prop (is-divisible-Group G)
+is-prop-is-divisible-Group G =
+  is-prop-Π λ n → is-prop-is-surjective (power-Group G (nat-ℕ⁺ n))
+
+is-divisible-Group-Prop : {l : Level} (G : Group l) → Prop l
+is-divisible-Group-Prop G = is-divisible-Group G , is-prop-is-divisible-Group G
+```
diff --git a/src/group-theory/endomorphism-rings-abelian-groups.lagda.md b/src/group-theory/endomorphism-rings-abelian-groups.lagda.md
index d3dfb679a9..4fdc01cca2 100644
--- a/src/group-theory/endomorphism-rings-abelian-groups.lagda.md
+++ b/src/group-theory/endomorphism-rings-abelian-groups.lagda.md
@@ -7,13 +7,22 @@ module group-theory.endomorphism-rings-abelian-groups where
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.large-precategories
+
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
+open import foundation-core.cartesian-product-types
+open import foundation-core.identity-types
+
 open import group-theory.abelian-groups
 open import group-theory.addition-homomorphisms-abelian-groups
 open import group-theory.homomorphisms-abelian-groups
+open import group-theory.invertible-elements-monoids
+open import group-theory.isomorphisms-abelian-groups
+open import group-theory.precategory-of-semigroups
 
+open import ring-theory.invertible-elements-rings
 open import ring-theory.rings
 ```
 
@@ -51,3 +60,39 @@ module _
   pr2 (pr2 (pr2 (pr2 endomorphism-ring-Ab))) =
     right-distributive-comp-add-hom-Ab A A A
 ```
+
+## Properties
+
+### [Isomorphisms](group-theory.isomorphisms-abelian-groups.md) `A ≃ A` are [units](ring-theory.invertible-elements-rings.md) in the endomorphism ring
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  is-iso-is-invertible-endomorphism-ring-Ab :
+    (f : hom-Ab A A) → is-iso-Ab A A f → is-invertible-element-Ring
+    ( endomorphism-ring-Ab A) f
+  pr1 (is-iso-is-invertible-endomorphism-ring-Ab f f-iso) =
+    hom-inv-is-iso-Ab A A f f-iso
+  pr1 (pr2 (is-iso-is-invertible-endomorphism-ring-Ab f f-iso)) =
+    pr1 (pr2 f-iso)
+  pr2 (pr2 (is-iso-is-invertible-endomorphism-ring-Ab f f-iso)) =
+    pr2 (pr2 f-iso)
+```
+
+### Units in the endomorphism ring are isomorphisms `A ≃ A`
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  is-invertible-is-iso-endomorphism-ring-Ab :
+    (f : hom-Ab A A) → is-invertible-element-Ring (endomorphism-ring-Ab A) f →
+    is-iso-Ab A A f
+  pr1 (is-invertible-is-iso-endomorphism-ring-Ab f (f-inv , f-inv-is-inv)) =
+    f-inv
+  pr2 (is-invertible-is-iso-endomorphism-ring-Ab f (f-inv , f-inv-is-inv)) =
+    f-inv-is-inv
+```
diff --git a/src/group-theory/kernels-homomorphisms-groups.lagda.md b/src/group-theory/kernels-homomorphisms-groups.lagda.md
index ba177596f8..f089d8b6b0 100644
--- a/src/group-theory/kernels-homomorphisms-groups.lagda.md
+++ b/src/group-theory/kernels-homomorphisms-groups.lagda.md
@@ -15,12 +15,15 @@ open import foundation.propositions
 open import foundation.sets
 open import foundation.universe-levels
 
+open import foundation-core.injective-maps
+
 open import group-theory.embeddings-groups
 open import group-theory.groups
 open import group-theory.homomorphisms-groups
 open import group-theory.normal-subgroups
 open import group-theory.subgroups
 open import group-theory.subsets-groups
+open import group-theory.trivial-subgroups
 ```
 
 </details>
@@ -133,3 +136,56 @@ module _
   pr1 kernel-hom-Group = subgroup-kernel-hom-Group G H f
   pr2 kernel-hom-Group = is-normal-kernel-hom-Group
 ```
+
+### When `ker f` is [trivial](group-theory.trivial-subgroups.md), `f` is [injective](foundation-core.injective-maps.md)
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
+  ( f-ker-triv : is-trivial-Subgroup G (subgroup-kernel-hom-Group G H f))
+  where
+
+  kernel-is-trivial-is-injective-Group : is-injective (map-hom-Group G H f)
+  kernel-is-trivial-is-injective-Group {x} {y} p = inv lem-3 where
+    lem-1 : is-in-kernel-hom-Group G H f (mul-Group G (inv-Group G y) x)
+    lem-1 = equational-reasoning
+      unit-Group H ＝ mul-Group H (inv-Group H (map-hom-Group G H f y))
+      ( map-hom-Group G H f y)
+        by inv (left-inverse-law-mul-Group H (pr1 f y))
+      ＝ mul-Group H (map-hom-Group G H f (inv-Group G y))
+      ( map-hom-Group G H f y)
+        by ap (λ z → mul-Group H z (pr1 f y))
+        ( inv (preserves-inv-hom-Group G H f))
+      ＝ mul-Group H (map-hom-Group G H f (inv-Group G y))
+      ( map-hom-Group G H f x)
+        by ap (mul-Group H (map-hom-Group G H f (inv-Group G y))) (inv p)
+      ＝ map-hom-Group G H f (mul-Group G (inv-Group G y) x)
+        by inv (preserves-mul-hom-Group G H f)
+
+    lem-2 : unit-Group G ＝ mul-Group G (inv-Group G y) x
+    lem-2 = f-ker-triv (mul-Group G (inv-Group G y) x) lem-1
+
+    lem-3 : y ＝ x
+    lem-3 = equational-reasoning
+      y ＝ mul-Group G y (unit-Group G)
+        by inv (right-unit-law-mul-Group G y)
+      ＝ mul-Group G y (mul-Group G (inv-Group G y) x)
+        by ap (mul-Group G y) lem-2
+      ＝ mul-Group G (mul-Group G y (inv-Group G y)) x
+        by inv (associative-mul-Group G y (inv-Group G y) x)
+      ＝ mul-Group G (unit-Group G) x
+        by ap (λ z → mul-Group G z x) (right-inverse-law-mul-Group G y)
+      ＝ x
+        by left-unit-law-mul-Group G x
+
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
+  where
+
+  is-injective-kernel-is-trivial-Group :
+    is-injective (map-hom-Group G H f) → is-trivial-Subgroup G
+    ( subgroup-kernel-hom-Group G H f)
+  is-injective-kernel-is-trivial-Group f-inj x fx-unit = f-inj lem where
+    lem : pr1 f (unit-Group G) ＝ pr1 f x
+    lem = preserves-unit-hom-Group G H f ∙ fx-unit
+```
diff --git a/src/group-theory/monomorphisms-groups.lagda.md b/src/group-theory/monomorphisms-groups.lagda.md
index eeebe4fb6c..cac98a8c03 100644
--- a/src/group-theory/monomorphisms-groups.lagda.md
+++ b/src/group-theory/monomorphisms-groups.lagda.md
@@ -1,21 +1,43 @@
 # Monomorphisms in the category of groups
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module group-theory.monomorphisms-groups where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import category-theory.large-precategories
 open import category-theory.monomorphisms-in-large-precategories
 
+open import elementary-number-theory.group-of-integers
+open import elementary-number-theory.integers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.propositions
 open import foundation.universe-levels
 
+open import foundation-core.embeddings
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.injective-maps
+open import foundation-core.retractions
+open import foundation-core.sections
+open import foundation-core.sets
+
+open import group-theory.free-groups-with-one-generator
 open import group-theory.groups
 open import group-theory.homomorphisms-groups
+open import group-theory.integer-powers-of-elements-groups
 open import group-theory.isomorphisms-groups
+open import group-theory.kernels-homomorphisms-groups
 open import group-theory.precategory-of-groups
+open import group-theory.trivial-subgroups
 ```
 
 </details>
@@ -61,3 +83,117 @@ module _
   is-mono-iso-Group =
     is-mono-iso-Large-Precategory Group-Large-Precategory l3 G H f
 ```
+
+### Monomorphisms are [injective](foundation.injective-maps.md)
+
+```agda
+{-
+module _
+  {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
+  (f-mono : is-mono-hom-Group l3 G H f)
+  where
+
+  is-mono-is-injective-Group : is-injective (map-hom-Group G H f)
+  is-mono-is-injective-Group {x} {y} p =
+    inv (integer-power-one-Group G x) ∙ htpy-2 one-ℤ ∙
+      integer-power-one-Group G y where
+    x-ℤ : hom-Group ℤ-Group G
+    x-ℤ = hom-element-Group G x
+
+    y-ℤ : hom-Group ℤ-Group G
+    y-ℤ = hom-element-Group G y
+
+    htpy-1 :
+      htpy-hom-Group ℤ-Group H (comp-hom-Group ℤ-Group G H f x-ℤ)
+      ( comp-hom-Group ℤ-Group G H f y-ℤ)
+    htpy-1 =
+      inv-htpy (htpy-hom-element-Group H (map-hom-Group G H f x)
+      ( comp-hom-Group ℤ-Group G H f x-ℤ) lem-1) ∙h lem-3 ∙h
+      htpy-hom-element-Group H (map-hom-Group G H f y)
+      ( comp-hom-Group ℤ-Group G H f y-ℤ) lem-2 where
+        lem-1 :
+          map-hom-Group ℤ-Group H (comp-hom-Group ℤ-Group G H f
+          ( hom-element-Group G x)) one-ℤ ＝ pr1 f x
+        lem-1 =
+          preserves-integer-powers-hom-Group G H f one-ℤ x ∙
+          integer-power-one-Group H (pr1 f x)
+
+        lem-2 :
+          map-hom-Group ℤ-Group H (comp-hom-Group ℤ-Group G H f
+          ( hom-element-Group G y)) one-ℤ ＝ pr1 f y
+        lem-2 =
+          preserves-integer-powers-hom-Group G H f one-ℤ y ∙
+          integer-power-one-Group H (pr1 f y)
+
+        lem-3 :
+          map-hom-element-Group H (pr1 f x) ~ map-hom-element-Group H (pr1 f y)
+        lem-3 z = ap (integer-power-Group H z) p
+
+    eq-1 :
+      (comp-hom-Group ℤ-Group G H f x-ℤ) ＝ (comp-hom-Group ℤ-Group G H f y-ℤ)
+    eq-1 = eq-htpy-hom-Group ℤ-Group H htpy-1
+
+    eq-2 : x-ℤ ＝ y-ℤ
+    eq-2 =
+      map-equiv (inv-equiv-ap-emb
+      (( λ g → comp-hom-Group ℤ-Group G H f g) , {!   !})) eq-1
+
+    htpy-2 : htpy-hom-Group ℤ-Group G x-ℤ y-ℤ
+    htpy-2 = htpy-eq-hom-Group ℤ-Group G x-ℤ y-ℤ eq-2
+-}
+```
+
+### `f : G → H` is a monomorphism when it is [injective](foundation-core.injective-maps.md)
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
+  (f-inj : is-injective (map-hom-Group G H f))
+  where
+
+  is-injective-is-mono-Group : {l : Level} → is-mono-hom-Group l G H f
+  pr1 (pr1 (is-injective-is-mono-Group K g h)) comp =
+    eq-htpy-hom-Group K G htpy where
+    htpy : htpy-hom-Group K G g h
+    htpy x =
+      f-inj (htpy-eq-hom-Group K H (comp-hom-Group K G H f g)
+      ( comp-hom-Group K G H f h) comp x)
+  pr2 (pr1 (is-injective-is-mono-Group K g h)) comp =
+    is-set-has-uip (is-set-hom-Group K H) (comp-hom-Group K G H f g)
+    ( comp-hom-Group K G H f h)
+    (( ap (comp-hom-Large-Precategory Group-Large-Precategory f) ∘
+    pr1 (pr1 (is-injective-is-mono-Group K g h))) comp) comp
+  pr1 (pr2 (is-injective-is-mono-Group K g h)) comp =
+    eq-htpy-hom-Group K G htpy where
+    htpy : htpy-hom-Group K G g h
+    htpy x =
+      f-inj (htpy-eq-hom-Group K H (comp-hom-Group K G H f g)
+      ( comp-hom-Group K G H f h) comp x)
+  pr2 (pr2 (is-injective-is-mono-Group K g h)) p =
+    is-set-has-uip (is-set-hom-Group K G) g h
+    (( pr1 (pr2 (is-injective-is-mono-Group K g h)) ∘
+    ap (comp-hom-Large-Precategory Group-Large-Precategory f)) p) p
+```
+
+### `f : G → H` is a monomorphism iff its [kernel](group-theory.kernels-homomorphisms-groups.md) is [trivial](group-theory.trivial-subgroups.md)
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
+  where
+
+  kernel-is-trivial-is-mono-Group :
+    {l : Level} → is-trivial-Subgroup G (subgroup-kernel-hom-Group G H f) →
+    is-mono-hom-Group l G H f
+  kernel-is-trivial-is-mono-Group f-ker-triv =
+    is-injective-is-mono-Group G H f
+    ( kernel-is-trivial-is-injective-Group G H f f-ker-triv)
+  {-
+  is-mono-kernel-is-trivial-Group :
+    {l : Level} → is-mono-hom-Group l G H f →
+    is-trivial-Subgroup G (subgroup-kernel-hom-Group G H f)
+  is-mono-kernel-is-trivial-Group f-mono x x-in-ker =
+    is-mono-is-injective-Group G H f f-mono
+    ( preserves-unit-hom-Group G H f ∙ x-in-ker)
+    -}
+```
diff --git a/src/group-theory/multiples-of-elements-abelian-groups.lagda.md b/src/group-theory/multiples-of-elements-abelian-groups.lagda.md
index 475f609270..51ef670834 100644
--- a/src/group-theory/multiples-of-elements-abelian-groups.lagda.md
+++ b/src/group-theory/multiples-of-elements-abelian-groups.lagda.md
@@ -11,11 +11,15 @@ open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels
 
+open import foundation-core.sets
+
 open import group-theory.abelian-groups
+open import group-theory.homomorphisms-abelian-groups
 open import group-theory.powers-of-elements-groups
 ```
 
@@ -152,3 +156,15 @@ module _
     multiple-Ab A (m *ℕ n) x ＝ multiple-Ab A n (multiple-Ab A m x)
   multiple-mul-Ab = power-mul-Group (group-Ab A)
 ```
+
+### The multiply-by-`n` homomorphism `A → A`
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  multiple-hom-Ab : (n : ℕ) → hom-Ab A A
+  pr1 (multiple-hom-Ab n) = multiple-Ab A n
+  pr2 (multiple-hom-Ab n) {x} {y} = left-distributive-multiple-add-Ab A n
+```
diff --git a/src/group-theory/rational-abelian-groups.lagda.md b/src/group-theory/rational-abelian-groups.lagda.md
new file mode 100644
index 0000000000..4c429b8d20
--- /dev/null
+++ b/src/group-theory/rational-abelian-groups.lagda.md
@@ -0,0 +1,139 @@
+# Rational abelian groups
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module group-theory.rational-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-integers
+open import elementary-number-theory.nonzero-natural-numbers
+open import elementary-number-theory.ring-of-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.contractible-maps
+open import foundation-core.contractible-types
+open import foundation-core.equivalences
+open import foundation-core.fibers-of-maps
+open import foundation-core.function-types
+open import foundation-core.identity-types
+open import foundation-core.injective-maps
+open import foundation-core.path-split-maps
+open import foundation-core.sections
+
+open import group-theory.abelian-groups
+open import group-theory.divisible-groups
+open import group-theory.endomorphism-rings-abelian-groups
+open import group-theory.groups
+open import group-theory.homomorphisms-abelian-groups
+open import group-theory.integer-powers-of-elements-groups
+open import group-theory.isomorphisms-abelian-groups
+open import group-theory.multiples-of-elements-abelian-groups
+open import group-theory.torsion-free-groups
+open import group-theory.trivial-groups
+open import group-theory.trivial-subgroups
+
+open import linear-algebra.left-modules-rings
+
+open import ring-theory.homomorphisms-rings
+open import ring-theory.invertible-elements-rings
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+A group `G` is called **rational** when it is
+[divisible](group-theory.divisible-groups.md) and
+[torsion-free](group-theory.torsion-free-groups.md). Although this definition is
+reasonable for nonabelian groups, it is of particular interest for abelian
+groups: these turn out to be precisely the
+[modules](linear-algebra.left-modules-rings.md) over the
+[rational numbers](elementary-number-theory.ring-of-rational-numbers.md).
+
+## Definition
+
+```agda
+is-rational-Group : {l : Level} (G : Group l) → UU l
+is-rational-Group G = is-divisible-Group G × is-torsion-free-Group G
+
+is-rational-Ab : {l : Level} (A : Ab l) → UU l
+is-rational-Ab A = is-rational-Group (group-Ab A)
+```
+
+## Properties
+
+### Any rational abelian group is uniquely a `ℚ`-module
+
+Proof: Note that an abelian group is divisible precisely when its
+multiply-by-`n` map is surjective for all `n : ℕ⁺`, and torsion-free precisely
+when its multiply-by-`n` map is injective for all `n : ℕ⁺`. For abelian groups
+`G`, these maps are in fact group homomorphisms `G → G`. Maps of sets, such as
+the underlying set of `G`, which are both injective and surjective are
+equivalences, making each of these maps isomorphisms, which are the invertible
+elements in `endomorphism-ring-Ab G`. Now use the universal property of
+localizations with the fact that `ℚ` is the localization of `ℤ` at the positive
+integers to get the desired unique ring map `ℚ → endomorphism-ring-Ab G`.
+
+Note: The language of "rational abelian groups" is nonstandard. The common
+language is of a "rational vector space", or a ℚ-module; because the
+to-be-defined monoidal categories of abelian groups and (left/right) ℚ-modules
+are equivalent, and because the space of ℚ-module structures on an abelian group
+is a proposition, the author prefers the naming convention seen for other
+subspaces of (abelian) groups. Thus, rational abelian groups.
+
+Note 2: For some constructive purposes, especially those with tight apartness
+relations floating around, injectivity of a map `f` (say, of `multiple-Ab A n`)
+is insufficient and its to-be-defined counterpart of "strong injectivity" is
+needed. Here, however, we may use the generally weaker notion of injectivity;
+univalence combined with path transport in the universe shows all equivalences
+are strongly injective in this sense, and for sets a map is an equivalence iff
+it is surjective and (weakly) injective.
+
+### The multiply-by-`n` maps are isomorphisms for `A` rational abelian
+
+```agda
+module _
+  {l : Level} (A : Ab l)
+  where
+
+  multiple-is-contr-map-rational-Ab : is-rational-Ab A → (n : ℕ⁺) → is-contr-map (multiple-Ab A (nat-nonzero-ℕ n))
+  multiple-is-contr-map-rational-Ab (A-div , A-tf) (n , n>0) y = {!   !}
+
+  multiple-is-equiv-rational-Ab : is-rational-Ab A → (n : ℕ⁺) → is-equiv (multiple-Ab A (nat-nonzero-ℕ n))
+  multiple-is-equiv-rational-Ab A-rat n = is-equiv-is-contr-map (multiple-is-contr-map-rational-Ab A-rat n)
+
+  multiple-is-iso-rational-Ab : is-rational-Ab A → (n : ℕ⁺) → is-iso-Ab A A (multiple-hom-Ab A (nat-nonzero-ℕ n))
+  multiple-is-iso-rational-Ab A-rat (n , n>0) = is-iso-is-equiv-hom-Ab A A (multiple-hom-Ab A n) (multiple-is-equiv-rational-Ab A-rat (n , n>0))
+```
+
+```agda
+module _
+  {l : Level}
+  where
+
+  is-rational-has-ℚ-module-structure :
+    (A : Ab l) → is-rational-Ab A → left-module-Ring l ring-ℚ
+  pr1 (is-rational-has-ℚ-module-structure A A-rat) = A
+  pr2 (is-rational-has-ℚ-module-structure A A-rat) = {!   !}
+
+  has-ℚ-module-structure-is-rational :
+    (M : left-module-Ring l ring-ℚ) →
+    is-rational-Ab (ab-left-module-Ring ring-ℚ M)
+  pr1 (has-ℚ-module-structure-is-rational M) = {!   !}
+  pr2 (has-ℚ-module-structure-is-rational M) =
+    mul-is-injective-is-torsion-free-Group (pr1 M) lem where
+    lem :
+      (k : nonzero-ℤ) → is-injective
+        ( integer-power-Group (group-Ab (pr1 M)) (int-nonzero-ℤ k))
+    lem k = {!   !}
+```
diff --git a/src/group-theory/torsion-free-groups.lagda.md b/src/group-theory/torsion-free-groups.lagda.md
index d7e4ed6170..2da56da21a 100644
--- a/src/group-theory/torsion-free-groups.lagda.md
+++ b/src/group-theory/torsion-free-groups.lagda.md
@@ -24,8 +24,13 @@ open import foundation.singleton-subtypes
 open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
+open import foundation-core.injective-maps
+
+open import group-theory.abelian-groups
 open import group-theory.groups
+open import group-theory.integer-multiples-of-elements-abelian-groups
 open import group-theory.integer-powers-of-elements-groups
+open import group-theory.kernels-homomorphisms-groups
 open import group-theory.orders-of-elements-groups
 open import group-theory.subgroups
 open import group-theory.torsion-elements-groups
@@ -166,3 +171,32 @@ module _
               ( Id-Prop (set-Group G) (unit-Group G) x)
               ( λ k p → inv (H x k p))))
 ```
+
+### When `G` is abelian, the property of being torsion-free is equivalent to the [multiply-by-`n` maps](group-theory.multiples-of-elements-abelian-groups.md) being [injective](group-theory.monomorphisms-groups.md) for nonzero `n`
+
+Proof : Condition 1. above says the
+[kernel](group-theory.kernels-homomorphisms-groups.md) of
+`hom-integer-multiple-Ab G n` is [trivial](group-theory.trivial-subgroups.md).
+By work in the file on kernels, these conditions are equivalent.
+
+```agda
+module _
+  {l : Level} (G : Ab l)
+  where
+
+  is-torsion-free-mul-is-injective-Group :
+    is-torsion-free-Group (group-Ab G) → (k : nonzero-ℤ) →
+    is-injective (integer-power-Group (group-Ab G) (int-nonzero-ℤ k))
+  is-torsion-free-mul-is-injective-Group G-tf k =
+    kernel-is-trivial-is-injective-Group (pr1 G) (pr1 G)
+    ( hom-integer-multiple-Ab G (pr1 k)) λ x x-tor → inv (G-tf x k (inv x-tor))
+
+  mul-is-injective-is-torsion-free-Group :
+    ((k : nonzero-ℤ) →
+    is-injective (integer-power-Group (group-Ab G) (int-nonzero-ℤ k))) →
+    is-torsion-free-Group (group-Ab G)
+  mul-is-injective-is-torsion-free-Group is-inj x k x-tor =
+    inv
+    ( is-injective-kernel-is-trivial-Group (group-Ab G) (group-Ab G)
+    ( hom-integer-multiple-Ab G (pr1 k)) (is-inj k) x (inv x-tor))
+```
diff --git a/src/ring-theory/localizations-rings.lagda.md b/src/ring-theory/localizations-rings.lagda.md
index 0c3aeb511a..72b43d054c 100644
--- a/src/ring-theory/localizations-rings.lagda.md
+++ b/src/ring-theory/localizations-rings.lagda.md
@@ -212,6 +212,13 @@ is-prop-inverts-subset-hom-Ring :
 is-prop-inverts-subset-hom-Ring R S P f =
   is-prop-Π (λ x → is-prop-Π (λ p → is-prop-inverts-element-hom-Ring R S x f))
 
+inverts-subset-hom-ring-Prop :
+  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R) →
+  (f : hom-Ring R S) → Prop (l1 ⊔ l2 ⊔ l3)
+pr1 (inverts-subset-hom-ring-Prop R S P f) = inverts-subset-hom-Ring R S P f
+pr2 (inverts-subset-hom-ring-Prop R S P f) =
+  is-prop-inverts-subset-hom-Ring R S P f
+
 inv-inverts-subset-hom-Ring :
   {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (P : subset-Ring l3 R)
   (f : hom-Ring R S) (H : inverts-subset-hom-Ring R S P f)