Rational abelian groups

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) , _) = {!   !}
+```

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

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
+```

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

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) = {!   !}
+-}
+```

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

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
+```

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
+```