Apartness of reals agrees with apartness in the heyting field (#1744)

Author: lowasser

src/commutative-algebra/heyting-fields.lagda.md

@@ -12,14 +12,23 @@ open import commutative-algebra.invertible-elements-commutative-rings
 open import commutative-algebra.local-commutative-rings
 open import commutative-algebra.trivial-commutative-rings
 
+open import foundation.apartness-relations
+open import foundation.binary-relations
 open import foundation.conjunction
 open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.functoriality-disjunction
+open import foundation.identity-types
 open import foundation.negation
 open import foundation.propositions
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.tight-apartness-relations
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import group-theory.abelian-groups
+
 open import ring-theory.rings
 ```
 
@@ -88,9 +97,18 @@ module _
   commutative-ring-Heyting-Field =
     commutative-ring-Local-Commutative-Ring local-commutative-ring-Heyting-Field
 
+  is-local-commutative-ring-Heyting-Field :
+    is-local-Commutative-Ring commutative-ring-Heyting-Field
+  is-local-commutative-ring-Heyting-Field =
+    is-local-commutative-ring-Local-Commutative-Ring
+      ( local-commutative-ring-Heyting-Field)
+
   ring-Heyting-Field : Ring l
   ring-Heyting-Field = ring-Commutative-Ring commutative-ring-Heyting-Field
 
+  ab-Heyting-Field : Ab l
+  ab-Heyting-Field = ab-Ring ring-Heyting-Field
+
   type-Heyting-Field : UU l
   type-Heyting-Field = type-Ring ring-Heyting-Field
 
@@ -100,6 +118,9 @@ module _
   zero-Heyting-Field : type-Heyting-Field
   zero-Heyting-Field = zero-Ring ring-Heyting-Field
 
+  is-zero-Heyting-Field : type-Heyting-Field → UU l
+  is-zero-Heyting-Field = is-zero-Ring ring-Heyting-Field
+
   one-Heyting-Field : type-Heyting-Field
   one-Heyting-Field = one-Ring ring-Heyting-Field
 
@@ -113,6 +134,152 @@ module _
 
   neg-Heyting-Field : type-Heyting-Field → type-Heyting-Field
   neg-Heyting-Field = neg-Ring ring-Heyting-Field
+
+  diff-Heyting-Field :
+    type-Heyting-Field → type-Heyting-Field → type-Heyting-Field
+  diff-Heyting-Field x y =
+    add-Heyting-Field x (neg-Heyting-Field y)
+
+  is-invertible-element-prop-Heyting-Field : type-Heyting-Field → Prop l
+  is-invertible-element-prop-Heyting-Field =
+    is-invertible-element-prop-Commutative-Ring commutative-ring-Heyting-Field
+
+  is-invertible-element-Heyting-Field : type-Heyting-Field → UU l
+  is-invertible-element-Heyting-Field x =
+    type-Prop (is-invertible-element-prop-Heyting-Field x)
+
+  is-zero-is-not-invertible-element-Heyting-Field :
+    (x : type-Heyting-Field) → ¬ (is-invertible-element-Heyting-Field x) →
+    is-zero-Heyting-Field x
+  is-zero-is-not-invertible-element-Heyting-Field = pr2 (pr2 F)
+
+  is-nontrivial-commutative-ring-Heyting-Field :
+    is-nontrivial-Commutative-Ring commutative-ring-Heyting-Field
+  is-nontrivial-commutative-ring-Heyting-Field = pr1 (pr2 F)
+
+  right-inverse-law-add-Heyting-Field :
+    (x : type-Heyting-Field) → diff-Heyting-Field x x ＝ zero-Heyting-Field
+  right-inverse-law-add-Heyting-Field =
+    right-inverse-law-add-Ring ring-Heyting-Field
+
+  left-zero-law-mul-Heyting-Field :
+    (x : type-Heyting-Field) →
+    mul-Heyting-Field zero-Heyting-Field x ＝ zero-Heyting-Field
+  left-zero-law-mul-Heyting-Field = left-zero-law-mul-Ring ring-Heyting-Field
+
+  ap-mul-Heyting-Field :
+    {x x' y y' : type-Heyting-Field} → x ＝ x' → y ＝ y' →
+    mul-Heyting-Field x y ＝ mul-Heyting-Field x' y'
+  ap-mul-Heyting-Field = ap-mul-Ring ring-Heyting-Field
+
+  mul-neg-Heyting-Field :
+    (x y : type-Heyting-Field) →
+    mul-Heyting-Field (neg-Heyting-Field x) (neg-Heyting-Field y) ＝
+    mul-Heyting-Field x y
+  mul-neg-Heyting-Field = mul-neg-Ring ring-Heyting-Field
+
+  distributive-neg-diff-Heyting-Field :
+    (x y : type-Heyting-Field) →
+    neg-Heyting-Field (diff-Heyting-Field x y) ＝ diff-Heyting-Field y x
+  distributive-neg-diff-Heyting-Field =
+    neg-right-subtraction-Ab ab-Heyting-Field
+
+  commutative-mul-Heyting-Field :
+    (x y : type-Heyting-Field) → mul-Heyting-Field x y ＝ mul-Heyting-Field y x
+  commutative-mul-Heyting-Field =
+    commutative-mul-Commutative-Ring commutative-ring-Heyting-Field
+
+  add-diff-Heyting-Field :
+    (x y z : type-Heyting-Field) →
+    add-Heyting-Field (diff-Heyting-Field x y) (diff-Heyting-Field y z) ＝
+    diff-Heyting-Field x z
+  add-diff-Heyting-Field =
+    add-right-subtraction-Ab ab-Heyting-Field
+
+  eq-is-zero-diff-Heyting-Field :
+    (x y : type-Heyting-Field) →
+    is-zero-Heyting-Field (diff-Heyting-Field x y) →
+    x ＝ y
+  eq-is-zero-diff-Heyting-Field x y =
+    eq-is-zero-right-subtraction-Ab ab-Heyting-Field
+```
+
+## Properties
+
+### Invertibility of `x - y` is a tight apartness relation
+
+```agda
+module _
+  {l : Level}
+  (F : Heyting-Field l)
+  where
+
+  apart-prop-Heyting-Field : Relation-Prop l (type-Heyting-Field F)
+  apart-prop-Heyting-Field x y =
+    is-invertible-element-prop-Heyting-Field F (diff-Heyting-Field F x y)
+
+  apart-Heyting-Field : Relation l (type-Heyting-Field F)
+  apart-Heyting-Field = type-Relation-Prop apart-prop-Heyting-Field
+
+  abstract
+    antirefl-apart-Heyting-Field : is-antireflexive apart-prop-Heyting-Field
+    antirefl-apart-Heyting-Field x is-invertible-x-x =
+      is-nontrivial-commutative-ring-Heyting-Field
+        ( F)
+        ( is-trivial-is-invertible-zero-Commutative-Ring
+          ( commutative-ring-Heyting-Field F)
+          ( tr
+            ( is-invertible-element-Heyting-Field F)
+            ( right-inverse-law-add-Heyting-Field F x)
+            ( is-invertible-x-x)))
+
+    symmetric-apart-Heyting-Field : is-symmetric apart-Heyting-Field
+    symmetric-apart-Heyting-Field x y is-invertible-⟨x-y⟩ =
+      tr
+        ( is-invertible-element-Heyting-Field F)
+        ( distributive-neg-diff-Heyting-Field F x y)
+        ( is-invertible-element-neg-is-invertible-element-Commutative-Ring
+          ( commutative-ring-Heyting-Field F)
+          ( _)
+          ( is-invertible-⟨x-y⟩))
+
+    cotransitive-apart-Heyting-Field :
+      is-cotransitive apart-prop-Heyting-Field
+    cotransitive-apart-Heyting-Field x y z is-invertible-⟨x-y⟩ =
+      map-disjunction
+        ( id)
+        ( symmetric-apart-Heyting-Field z y)
+        ( is-local-commutative-ring-Heyting-Field F
+          ( diff-Heyting-Field F x z)
+          ( diff-Heyting-Field F z y)
+          ( inv-tr
+            ( is-invertible-element-Heyting-Field F)
+            ( add-diff-Heyting-Field F x z y)
+            ( is-invertible-⟨x-y⟩)))
+
+  apartness-relation-Heyting-Field : Apartness-Relation l (type-Heyting-Field F)
+  apartness-relation-Heyting-Field =
+    ( apart-prop-Heyting-Field ,
+      antirefl-apart-Heyting-Field ,
+      symmetric-apart-Heyting-Field ,
+      cotransitive-apart-Heyting-Field)
+
+  abstract
+    is-tight-apartness-relation-Heyting-Field :
+      is-tight-Apartness-Relation apartness-relation-Heyting-Field
+    is-tight-apartness-relation-Heyting-Field x y ¬apart-x-y =
+      eq-is-zero-diff-Heyting-Field F
+        ( x)
+        ( y)
+        ( is-zero-is-not-invertible-element-Heyting-Field F
+          ( diff-Heyting-Field F x y)
+          ( ¬apart-x-y))
+
+  tight-apartness-relation-Heyting-Field :
+    Tight-Apartness-Relation l (type-Heyting-Field F)
+  tight-apartness-relation-Heyting-Field =
+    ( apartness-relation-Heyting-Field ,
+      is-tight-apartness-relation-Heyting-Field)
 ```
 
 ## External links

src/commutative-algebra/invertible-elements-commutative-rings.lagda.md

@@ -341,6 +341,22 @@ module _
       ( ring-Commutative-Ring A)
 ```
 
+### The negation of an invertible element is invertible
+
+```agda
+module _
+  {l : Level} (A : Commutative-Ring l)
+  where
+
+  abstract
+    is-invertible-element-neg-is-invertible-element-Commutative-Ring :
+      (x : type-Commutative-Ring A)
+      (H : is-invertible-element-Commutative-Ring A x) →
+      is-invertible-element-Commutative-Ring A (neg-Commutative-Ring A x)
+    is-invertible-element-neg-is-invertible-element-Commutative-Ring =
+      is-invertible-element-neg-Ring (ring-Commutative-Ring A)
+```
+
 ## See also
 
 - The group of multiplicative units of a commutative ring is defined in

src/commutative-algebra/trivial-commutative-rings.lagda.md

@@ -8,6 +8,7 @@ module commutative-algebra.trivial-commutative-rings where
 
 ```agda
 open import commutative-algebra.commutative-rings
+open import commutative-algebra.invertible-elements-commutative-rings
 open import commutative-algebra.isomorphisms-commutative-rings
 
 open import foundation.contractible-types
@@ -109,6 +110,31 @@ is-trivial-trivial-Commutative-Ring :
 is-trivial-trivial-Commutative-Ring = refl
 ```
 
+### The zero of a commutative ring is invertible if and only if the commutative ring is trivial
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  where
+
+  abstract
+    is-invertible-zero-is-trivial-Commutative-Ring :
+      is-trivial-Commutative-Ring R →
+      is-invertible-element-Commutative-Ring R (zero-Commutative-Ring R)
+    is-invertible-zero-is-trivial-Commutative-Ring 0=1 =
+      ( one-Commutative-Ring R ,
+        ( ( ap-mul-Commutative-Ring R 0=1 refl) ∙
+          ( right-unit-law-mul-Commutative-Ring R _)) ,
+        ( ( ap-mul-Commutative-Ring R refl 0=1) ∙
+          ( left-unit-law-mul-Commutative-Ring R _)))
+
+    is-trivial-is-invertible-zero-Commutative-Ring :
+      is-invertible-element-Commutative-Ring R (zero-Commutative-Ring R) →
+      is-trivial-Commutative-Ring R
+    is-trivial-is-invertible-zero-Commutative-Ring (r , 0r=1 , _) =
+      inv (left-zero-law-mul-Commutative-Ring R r) ∙ 0r=1
+```
+
 ### The type of trivial rings is contractible
 
 To-do: complete proof of uniqueness of the zero ring using SIP, ideally refactor

src/real-numbers/apartness-real-numbers.lagda.md

@@ -285,6 +285,10 @@ module _
         ( sim-eq-ℝ (left-unit-law-add-ℝ y))
         ( preserves-apart-right-add-ℝ y _ _ x-y#0)
 
+  apart-iff-is-nonzero-diff-ℝ : (apart-ℝ x y) ↔ (is-nonzero-ℝ (x -ℝ y))
+  apart-iff-is-nonzero-diff-ℝ =
+    ( is-nonzero-diff-is-apart-ℝ , apart-is-nonzero-diff-ℝ)
+
   nonzero-diff-apart-ℝ : apart-ℝ x y → nonzero-ℝ (l1 ⊔ l2)
   nonzero-diff-apart-ℝ x#y = (x -ℝ y , is-nonzero-diff-is-apart-ℝ x#y)
 ```

src/real-numbers/field-of-real-numbers.lagda.md

@@ -14,15 +14,19 @@ open import commutative-algebra.trivial-commutative-rings
 open import elementary-number-theory.rational-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.negated-equality
 open import foundation.negation
 open import foundation.universe-levels
 
 open import real-numbers.apartness-real-numbers
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
 open import real-numbers.large-ring-of-real-numbers
 open import real-numbers.local-ring-of-real-numbers
+open import real-numbers.multiplication-nonzero-real-numbers
 open import real-numbers.multiplicative-inverses-nonzero-real-numbers
 open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
@@ -71,3 +75,16 @@ heyting-field-ℝ l =
   ( local-commutative-ring-ℝ l ,
     is-heyting-field-local-commutative-ring-ℝ l)
 ```
+
+## Properties
+
+### The apartness relation of the Heyting field of real numbers agrees with the apartness relation of the real numbers
+
+```agda
+apart-iff-apart-heyting-field-ℝ :
+  {l : Level} (x y : ℝ l) →
+  (apart-ℝ x y) ↔ (apart-Heyting-Field (heyting-field-ℝ l) x y)
+apart-iff-apart-heyting-field-ℝ x y =
+  ( inv-iff (is-invertible-iff-is-nonzero-ℝ (x -ℝ y))) ∘iff
+  ( apart-iff-is-nonzero-diff-ℝ x y)
+```

src/real-numbers/multiplication-nonzero-real-numbers.lagda.md

@@ -17,6 +17,7 @@ open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
+open import foundation.logical-equivalences
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
@@ -150,3 +151,14 @@ abstract
           { y = raise-ℝ l one-ℝ}
           ( sim-raise-ℝ l one-ℝ)))
 ```
+
+### A real number is invertible iff it is nonzero
+
+```agda
+is-invertible-iff-is-nonzero-ℝ :
+  {l : Level} (x : ℝ l) →
+  (is-invertible-element-Commutative-Ring (commutative-ring-ℝ l) x) ↔
+  (is-nonzero-ℝ x)
+is-invertible-iff-is-nonzero-ℝ x =
+  ( is-nonzero-is-invertible-ℝ x , is-invertible-is-nonzero-ℝ x)
+```

src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md

@@ -27,6 +27,7 @@ open import foundation.disjunction
 open import foundation.empty-types
 open import foundation.existential-quantification
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.subtypes

src/ring-theory/invertible-elements-rings.lagda.md

@@ -328,27 +328,28 @@ module _
   {l : Level} (R : Ring l)
   where
 
-  is-invertible-element-neg-Ring :
-    (x : type-Ring R) →
-    is-invertible-element-Ring R x →
-    is-invertible-element-Ring R (neg-Ring R x)
-  is-invertible-element-neg-Ring x =
-    map-Σ _
-      ( neg-Ring R)
-      ( λ y →
-        map-product
-          ( mul-neg-Ring R x y ∙_)
-          ( mul-neg-Ring R y x ∙_))
-
-  is-invertible-element-neg-Ring' :
-    (x : type-Ring R) →
-    is-invertible-element-Ring R (neg-Ring R x) →
-    is-invertible-element-Ring R x
-  is-invertible-element-neg-Ring' x H =
-    tr
-      ( is-invertible-element-Ring R)
-      ( neg-neg-Ring R x)
-      ( is-invertible-element-neg-Ring (neg-Ring R x) H)
+  abstract
+    is-invertible-element-neg-Ring :
+      (x : type-Ring R) →
+      is-invertible-element-Ring R x →
+      is-invertible-element-Ring R (neg-Ring R x)
+    is-invertible-element-neg-Ring x =
+      map-Σ _
+        ( neg-Ring R)
+        ( λ y →
+          map-product
+            ( mul-neg-Ring R x y ∙_)
+            ( mul-neg-Ring R y x ∙_))
+
+    is-invertible-element-neg-Ring' :
+      (x : type-Ring R) →
+      is-invertible-element-Ring R (neg-Ring R x) →
+      is-invertible-element-Ring R x
+    is-invertible-element-neg-Ring' x H =
+      tr
+        ( is-invertible-element-Ring R)
+        ( neg-neg-Ring R x)
+        ( is-invertible-element-neg-Ring (neg-Ring R x) H)
 ```
 
 ### The inverse of an invertible element is invertible