Vector spaces (#1689)

Completes #1685 .  Builds on #1684 and #1679.

Author: lowasser

src/commutative-algebra.lagda.md

@@ -25,6 +25,7 @@ open import commutative-algebra.function-commutative-semirings public
 open import commutative-algebra.geometric-sequences-commutative-rings public
 open import commutative-algebra.geometric-sequences-commutative-semirings public
 open import commutative-algebra.groups-of-units-commutative-rings public
+open import commutative-algebra.heyting-fields public
 open import commutative-algebra.homomorphisms-commutative-rings public
 open import commutative-algebra.homomorphisms-commutative-semirings public
 open import commutative-algebra.ideals-commutative-rings public

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

@@ -0,0 +1,120 @@
+# Heyting fields
+
+```agda
+module commutative-algebra.heyting-fields where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+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.conjunction
+open import foundation.dependent-pair-types
+open import foundation.negation
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import ring-theory.rings
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "Heyting field" WDID=Q5749811 WD="Heyting field" Agda=Heyting-Field}}
+is a [local commutative ring](commutative-algebra.local-commutative-rings.md)
+with the properties:
+
+- it is [nontrivial](commutative-algebra.trivial-commutative-rings.md): 0 ≠ 1
+- any
+  [non](foundation.negation.md)-[invertible](commutative-algebra.invertible-elements-commutative-rings.md)
+  element is [equal](foundation.identity-types.md) to zero
+
+Note that this is distinct from the classical notion of a field, called
+[discrete field](commutative-algebra.discrete-fields.md) in constructive
+contexts, which asserts that every element is
+[either](foundation.exclusive-disjunction.md) invertible or equal to zero. A
+Heyting field is a discrete field if and only if its equality relation is
+[decidable](foundation.decidable-equality.md), which would not include e.g. the
+[real numbers](real-numbers.dedekind-real-numbers.md).
+
+## Definition
+
+```agda
+is-heyting-field-prop-Local-Commutative-Ring :
+  {l : Level} → Local-Commutative-Ring l → Prop l
+is-heyting-field-prop-Local-Commutative-Ring R =
+  ( is-nontrivial-commutative-ring-Prop
+    ( commutative-ring-Local-Commutative-Ring R)) ∧
+  ( Π-Prop
+    ( type-Local-Commutative-Ring R)
+    ( λ x →
+      hom-Prop
+        ( ¬'
+          ( is-invertible-element-prop-Commutative-Ring
+            ( commutative-ring-Local-Commutative-Ring R)
+            ( x)))
+        ( is-zero-prop-Local-Commutative-Ring R x)))
+
+is-heyting-field-Local-Commutative-Ring :
+  {l : Level} → Local-Commutative-Ring l → UU l
+is-heyting-field-Local-Commutative-Ring R =
+  type-Prop (is-heyting-field-prop-Local-Commutative-Ring R)
+
+Heyting-Field : (l : Level) → UU (lsuc l)
+Heyting-Field l =
+  type-subtype (is-heyting-field-prop-Local-Commutative-Ring {l})
+```
+
+## Properties
+
+```agda
+module _
+  {l : Level}
+  (F : Heyting-Field l)
+  where
+
+  local-commutative-ring-Heyting-Field : Local-Commutative-Ring l
+  local-commutative-ring-Heyting-Field = pr1 F
+
+  commutative-ring-Heyting-Field : Commutative-Ring l
+  commutative-ring-Heyting-Field =
+    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
+
+  type-Heyting-Field : UU l
+  type-Heyting-Field = type-Ring ring-Heyting-Field
+
+  set-Heyting-Field : Set l
+  set-Heyting-Field = set-Ring ring-Heyting-Field
+
+  zero-Heyting-Field : type-Heyting-Field
+  zero-Heyting-Field = zero-Ring ring-Heyting-Field
+
+  one-Heyting-Field : type-Heyting-Field
+  one-Heyting-Field = one-Ring ring-Heyting-Field
+
+  add-Heyting-Field :
+    type-Heyting-Field → type-Heyting-Field → type-Heyting-Field
+  add-Heyting-Field = add-Ring ring-Heyting-Field
+
+  mul-Heyting-Field :
+    type-Heyting-Field → type-Heyting-Field → type-Heyting-Field
+  mul-Heyting-Field = mul-Ring ring-Heyting-Field
+
+  neg-Heyting-Field : type-Heyting-Field → type-Heyting-Field
+  neg-Heyting-Field = neg-Ring ring-Heyting-Field
+```
+
+## External links
+
+- [Heyting field](https://ncatlab.org/nlab/show/Heyting+field) at $n$Lab

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

@@ -22,10 +22,9 @@ open import ring-theory.rings
 
 ## Idea
 
-A **local ring** is a ring such that whenever a sum of elements is invertible,
-then one of its summands is invertible. This implies that the noninvertible
-elements form an ideal. However, the law of excluded middle is needed to show
-that any ring of which the noninvertible elements form an ideal is a local ring.
+A {{#concept "local commutative ring" Agda=Local-Commutative-Ring}} is a
+[commutative ring](commutative-algebra.commutative-rings.md) that is
+[local](ring-theory.local-rings.md).
 
 ## Definition
 
@@ -66,4 +65,33 @@ module _
   is-local-commutative-ring-Local-Commutative-Ring :
     is-local-Commutative-Ring commutative-ring-Local-Commutative-Ring
   is-local-commutative-ring-Local-Commutative-Ring = pr2 A
+
+  zero-Local-Commutative-Ring : type-Local-Commutative-Ring
+  zero-Local-Commutative-Ring = zero-Ring ring-Local-Commutative-Ring
+
+  is-zero-prop-Local-Commutative-Ring : type-Local-Commutative-Ring → Prop l
+  is-zero-prop-Local-Commutative-Ring =
+    is-zero-ring-Prop ring-Local-Commutative-Ring
+
+  one-Local-Commutative-Ring : type-Local-Commutative-Ring
+  one-Local-Commutative-Ring = one-Ring ring-Local-Commutative-Ring
+
+  add-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring →
+    type-Local-Commutative-Ring
+  add-Local-Commutative-Ring = add-Ring ring-Local-Commutative-Ring
+
+  mul-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring →
+    type-Local-Commutative-Ring
+  mul-Local-Commutative-Ring = mul-Ring ring-Local-Commutative-Ring
+
+  neg-Local-Commutative-Ring :
+    type-Local-Commutative-Ring → type-Local-Commutative-Ring
+  neg-Local-Commutative-Ring = neg-Ring ring-Local-Commutative-Ring
 ```
+
+## See also
+
+- [Heyting fields](commutative-algebra.heyting-fields.md), a local commutative
+  ring with stronger constraints on invertibility

src/elementary-number-theory/rational-numbers.lagda.md

@@ -24,6 +24,7 @@ open import foundation.equality-cartesian-product-types
 open import foundation.equality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
+open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositions
 open import foundation.reflecting-maps-equivalence-relations
@@ -140,6 +141,9 @@ one-ℚ = rational-ℤ one-ℤ
 
 is-one-ℚ : ℚ → UU lzero
 is-one-ℚ x = (x ＝ one-ℚ)
+
+neq-zero-one-ℚ : zero-ℚ ≠ one-ℚ
+neq-zero-one-ℚ ()
 ```
 
 ### The negative of a rational number

src/foundation/large-apartness-relations.lagda.md

@@ -7,6 +7,10 @@ module foundation.large-apartness-relations where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.apartness-relations
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.functoriality-disjunction
 open import foundation.identity-types
 open import foundation.large-binary-relations
 open import foundation.negated-equality
@@ -99,3 +103,24 @@ module _
   nonequal-apart-Large-Apartness-Relation {a = a} p refl =
     antirefl-Large-Apartness-Relation R a p
 ```
+
+### Small apartness relations from large apartness relations
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  {A : (l : Level) → UU (α l)} (R : Large-Apartness-Relation β A)
+  where
+
+  apartness-relation-Large-Apartness-Relation :
+    (l : Level) → Apartness-Relation (β l l) (A l)
+  apartness-relation-Large-Apartness-Relation l =
+    ( apart-prop-Large-Apartness-Relation R ,
+      antirefl-Large-Apartness-Relation R ,
+      symmetric-Large-Apartness-Relation R ,
+      λ a b c a#b →
+      map-disjunction
+        ( id)
+        ( symmetric-Large-Apartness-Relation R c b)
+        ( cotransitive-Large-Apartness-Relation R a b c a#b))
+```

src/linear-algebra.lagda.md

@@ -34,6 +34,7 @@ open import linear-algebra.matrices-on-rings public
 open import linear-algebra.multiplication-matrices public
 open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public
 open import linear-algebra.rational-modules public
+open import linear-algebra.real-vector-spaces public
 open import linear-algebra.right-modules-rings public
 open import linear-algebra.scalar-multiplication-matrices public
 open import linear-algebra.scalar-multiplication-tuples public
@@ -47,4 +48,5 @@ open import linear-algebra.tuples-on-euclidean-domains public
 open import linear-algebra.tuples-on-monoids public
 open import linear-algebra.tuples-on-rings public
 open import linear-algebra.tuples-on-semirings public
+open import linear-algebra.vector-spaces public
 ```