Vector spaces

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,112 @@
+# 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)
+  elements are [equal](foundation.identity-types.md) to zero
+
+## 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,12 @@ 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
+[local](ring-theory.local-rings.md)
+[commutative ring](commutative-algebra.commutative-rings.md).
+
+A local commutative ring is one limited version of the classical notion of field
+that applies usefully in constructive contexts.
 
 ## Definition
 
@@ -66,4 +68,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/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

@@ -33,6 +33,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
@@ -46,4 +47,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
 ```

src/linear-algebra/real-vector-spaces.lagda.md

@@ -0,0 +1,174 @@
+# Real vector spaces
+
+```agda
+module linear-algebra.real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+
+open import linear-algebra.vector-spaces
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.field-of-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "real vector space" WD="real vector space" WDID=Q46996054 Agda=ℝ-Vector-Space}}
+is a [vector space](linear-algebra.vector-spaces.md) over the
+[Heyting field of real numbers](real-numbers.field-of-real-numbers.md).
+
+## Definition
+
+```agda
+ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+ℝ-Vector-Space l1 l2 = Vector-Space l2 (heyting-field-ℝ l1)
+```
+
+## Properties
+
+```agda
+module _
+  {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2)
+  where
+
+  ab-ℝ-Vector-Space : Ab l2
+  ab-ℝ-Vector-Space = ab-Vector-Space (heyting-field-ℝ l1) V
+
+  set-ℝ-Vector-Space : Set l2
+  set-ℝ-Vector-Space = set-Ab ab-ℝ-Vector-Space
+
+  type-ℝ-Vector-Space : UU l2
+  type-ℝ-Vector-Space = type-Ab ab-ℝ-Vector-Space
+
+  add-ℝ-Vector-Space :
+    type-ℝ-Vector-Space → type-ℝ-Vector-Space → type-ℝ-Vector-Space
+  add-ℝ-Vector-Space = add-Ab ab-ℝ-Vector-Space
+
+  zero-ℝ-Vector-Space : type-ℝ-Vector-Space
+  zero-ℝ-Vector-Space = zero-Ab ab-ℝ-Vector-Space
+
+  neg-ℝ-Vector-Space : type-ℝ-Vector-Space → type-ℝ-Vector-Space
+  neg-ℝ-Vector-Space = neg-Ab ab-ℝ-Vector-Space
+
+  mul-ℝ-Vector-Space : ℝ l1 → type-ℝ-Vector-Space → type-ℝ-Vector-Space
+  mul-ℝ-Vector-Space = mul-Vector-Space (heyting-field-ℝ l1) V
+
+  associative-add-ℝ-Vector-Space :
+    (v w x : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space (add-ℝ-Vector-Space v w) x ＝
+    add-ℝ-Vector-Space v (add-ℝ-Vector-Space w x)
+  associative-add-ℝ-Vector-Space = associative-add-Ab ab-ℝ-Vector-Space
+
+  left-unit-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) → add-ℝ-Vector-Space zero-ℝ-Vector-Space v ＝ v
+  left-unit-law-add-ℝ-Vector-Space = left-unit-law-add-Ab ab-ℝ-Vector-Space
+
+  right-unit-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) → add-ℝ-Vector-Space v zero-ℝ-Vector-Space ＝ v
+  right-unit-law-add-ℝ-Vector-Space = right-unit-law-add-Ab ab-ℝ-Vector-Space
+
+  left-inverse-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space (neg-ℝ-Vector-Space v) v ＝ zero-ℝ-Vector-Space
+  left-inverse-law-add-ℝ-Vector-Space =
+    left-inverse-law-add-Ab ab-ℝ-Vector-Space
+
+  right-inverse-law-add-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space v (neg-ℝ-Vector-Space v) ＝ zero-ℝ-Vector-Space
+  right-inverse-law-add-ℝ-Vector-Space =
+    right-inverse-law-add-Ab ab-ℝ-Vector-Space
+
+  commutative-add-ℝ-Vector-Space :
+    (v w : type-ℝ-Vector-Space) →
+    add-ℝ-Vector-Space v w ＝ add-ℝ-Vector-Space w v
+  commutative-add-ℝ-Vector-Space = commutative-add-Ab ab-ℝ-Vector-Space
+
+  left-unit-law-mul-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (raise-ℝ l1 one-ℝ) v ＝ v
+  left-unit-law-mul-ℝ-Vector-Space =
+    left-unit-law-mul-Vector-Space (heyting-field-ℝ l1) V
+
+  left-distributive-mul-add-ℝ-Vector-Space :
+    (r : ℝ l1) (v w : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space r (add-ℝ-Vector-Space v w) ＝
+    add-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space r w)
+  left-distributive-mul-add-ℝ-Vector-Space =
+    left-distributive-mul-add-Vector-Space (heyting-field-ℝ l1) V
+
+  right-distributive-mul-add-ℝ-Vector-Space :
+    (r s : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (r +ℝ s) v ＝
+    add-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space s v)
+  right-distributive-mul-add-ℝ-Vector-Space =
+    right-distributive-mul-add-Vector-Space (heyting-field-ℝ l1) V
+
+  associative-mul-ℝ-Vector-Space :
+    (r s : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (r *ℝ s) v ＝
+    mul-ℝ-Vector-Space r (mul-ℝ-Vector-Space s v)
+  associative-mul-ℝ-Vector-Space =
+    associative-mul-Vector-Space (heyting-field-ℝ l1) V
+
+  left-zero-law-mul-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (raise-ℝ l1 zero-ℝ) v ＝ zero-ℝ-Vector-Space
+  left-zero-law-mul-ℝ-Vector-Space =
+    left-zero-law-mul-Vector-Space (heyting-field-ℝ l1) V
+
+  right-zero-law-mul-ℝ-Vector-Space :
+    (r : ℝ l1) →
+    mul-ℝ-Vector-Space r zero-ℝ-Vector-Space ＝ zero-ℝ-Vector-Space
+  right-zero-law-mul-ℝ-Vector-Space =
+    right-zero-law-mul-Vector-Space (heyting-field-ℝ l1) V
+
+  left-negative-law-mul-ℝ-Vector-Space :
+    (r : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (neg-ℝ r) v ＝
+    neg-ℝ-Vector-Space (mul-ℝ-Vector-Space r v)
+  left-negative-law-mul-ℝ-Vector-Space =
+    left-negative-law-mul-Vector-Space (heyting-field-ℝ l1) V
+
+  right-negative-law-mul-ℝ-Vector-Space :
+    (r : ℝ l1) (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space r (neg-ℝ-Vector-Space v) ＝
+    neg-ℝ-Vector-Space (mul-ℝ-Vector-Space r v)
+  right-negative-law-mul-ℝ-Vector-Space =
+    right-negative-law-mul-Vector-Space (heyting-field-ℝ l1) V
+
+  mul-neg-one-ℝ-Vector-Space :
+    (v : type-ℝ-Vector-Space) →
+    mul-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝ neg-ℝ-Vector-Space v
+  mul-neg-one-ℝ-Vector-Space =
+    mul-neg-one-Vector-Space (heyting-field-ℝ l1) V
+```
+
+### The real numbers are a real vector space
+
+```agda
+real-vector-space-ℝ : (l : Level) → ℝ-Vector-Space l (lsuc l)
+real-vector-space-ℝ l =
+  vector-space-heyting-field-Heyting-Field
+    ( heyting-field-ℝ l)
+```
+
+## See also
+
+- [Vector spaces](linear-algebra.vector-spaces.md)