diff --git a/src/commutative-algebra.lagda.md b/src/commutative-algebra.lagda.md index 0f1fc660db..5391c928cf 100644 --- a/src/commutative-algebra.lagda.md +++ b/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 diff --git a/src/commutative-algebra/heyting-fields.lagda.md b/src/commutative-algebra/heyting-fields.lagda.md new file mode 100644 index 0000000000..95c0db1b7c --- /dev/null +++ b/src/commutative-algebra/heyting-fields.lagda.md @@ -0,0 +1,120 @@ +# Heyting fields + +```agda +module commutative-algebra.heyting-fields where +``` + +
Imports + +```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 +``` + +
+ +## 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 diff --git a/src/commutative-algebra/local-commutative-rings.lagda.md b/src/commutative-algebra/local-commutative-rings.lagda.md index 9de71b60fc..7caf5074f5 100644 --- a/src/commutative-algebra/local-commutative-rings.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index 1c7bb3cb8e..57eeec8112 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/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 diff --git a/src/foundation/large-apartness-relations.lagda.md b/src/foundation/large-apartness-relations.lagda.md index 88ed670657..0241d665c1 100644 --- a/src/foundation/large-apartness-relations.lagda.md +++ b/src/foundation/large-apartness-relations.lagda.md @@ -7,6 +7,10 @@ module foundation.large-apartness-relations where
Imports ```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)) +``` diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index c4a73fc050..bc84732dbb 100644 --- a/src/linear-algebra.lagda.md +++ 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 ``` diff --git a/src/linear-algebra/real-vector-spaces.lagda.md b/src/linear-algebra/real-vector-spaces.lagda.md new file mode 100644 index 0000000000..bc1d8cd6f2 --- /dev/null +++ b/src/linear-algebra/real-vector-spaces.lagda.md @@ -0,0 +1,174 @@ +# Real vector spaces + +```agda +module linear-algebra.real-vector-spaces where +``` + +
Imports + +```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 +``` + +
+ +## 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) diff --git a/src/linear-algebra/vector-spaces.lagda.md b/src/linear-algebra/vector-spaces.lagda.md new file mode 100644 index 0000000000..f04707ae80 --- /dev/null +++ b/src/linear-algebra/vector-spaces.lagda.md @@ -0,0 +1,198 @@ +# Vector spaces + +```agda +module linear-algebra.vector-spaces where +``` + +
Imports + +```agda +open import commutative-algebra.heyting-fields + +open import foundation.identity-types +open import foundation.sets +open import foundation.universe-levels + +open import group-theory.abelian-groups + +open import linear-algebra.left-modules-commutative-rings +``` + +
+ +## Idea + +A {{#concept "vector space" WD="vector space" WDID=Q125977}} is a +[left module](linear-algebra.left-modules-rings.md) over a +[Heyting field](commutative-algebra.heyting-fields.md). + +## Definition + +```agda +Vector-Space : + {l1 : Level} (l2 : Level) → Heyting-Field l1 → UU (l1 ⊔ lsuc l2) +Vector-Space l2 R = + left-module-Commutative-Ring l2 (commutative-ring-Heyting-Field R) +``` + +## Properties + +```agda +module _ + {l1 l2 : Level} (R : Heyting-Field l1) (V : Vector-Space l2 R) + where + + ab-Vector-Space : Ab l2 + ab-Vector-Space = + ab-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( 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 : + type-Heyting-Field R → type-Vector-Space → type-Vector-Space + mul-Vector-Space = + mul-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( 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 (one-Heyting-Field R) v ＝ v + left-unit-law-mul-Vector-Space = + left-unit-law-mul-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + left-distributive-mul-add-Vector-Space : + (r : type-Heyting-Field R) (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-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + right-distributive-mul-add-Vector-Space : + (r s : type-Heyting-Field R) (v : type-Vector-Space) → + mul-Vector-Space (add-Heyting-Field R 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-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + associative-mul-Vector-Space : + (r s : type-Heyting-Field R) (v : type-Vector-Space) → + mul-Vector-Space (mul-Heyting-Field R r s) v ＝ + mul-Vector-Space r (mul-Vector-Space s v) + associative-mul-Vector-Space = + associative-mul-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + left-zero-law-mul-Vector-Space : + (v : type-Vector-Space) → + mul-Vector-Space (zero-Heyting-Field R) v ＝ zero-Vector-Space + left-zero-law-mul-Vector-Space = + left-zero-law-mul-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + right-zero-law-mul-Vector-Space : + (r : type-Heyting-Field R) → + mul-Vector-Space r zero-Vector-Space ＝ zero-Vector-Space + right-zero-law-mul-Vector-Space = + right-zero-law-mul-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + left-negative-law-mul-Vector-Space : + (r : type-Heyting-Field R) (v : type-Vector-Space) → + mul-Vector-Space (neg-Heyting-Field R r) v ＝ + neg-Vector-Space (mul-Vector-Space r v) + left-negative-law-mul-Vector-Space = + left-negative-law-mul-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + right-negative-law-mul-Vector-Space : + (r : type-Heyting-Field R) (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-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + + mul-neg-one-Vector-Space : + (v : type-Vector-Space) → + mul-Vector-Space + ( neg-Heyting-Field R (one-Heyting-Field R)) + ( v) ＝ + neg-Vector-Space v + mul-neg-one-Vector-Space = + mul-neg-one-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) +``` + +### Any Heyting field is a vector space over itself + +```agda +vector-space-heyting-field-Heyting-Field : + {l : Level} (R : Heyting-Field l) → Vector-Space l R +vector-space-heyting-field-Heyting-Field R = + left-module-commutative-ring-Commutative-Ring + ( commutative-ring-Heyting-Field R) +``` + +## See also + +- [Real vector spaces](linear-algebra.real-vector-spaces.md) + +## External links + +- [Vector space](https://en.wikipedia.org/wiki/Vector_space) on Wikipedia diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 035444db6c..26bb420996 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -9,7 +9,9 @@ open import real-numbers.absolute-value-closed-intervals-real-numbers public open import real-numbers.absolute-value-real-numbers public open import real-numbers.accumulation-points-subsets-real-numbers public open import real-numbers.addition-lower-dedekind-real-numbers public +open import real-numbers.addition-negative-real-numbers public open import real-numbers.addition-nonnegative-real-numbers public +open import real-numbers.addition-nonzero-real-numbers public open import real-numbers.addition-positive-real-numbers public open import real-numbers.addition-real-numbers public open import real-numbers.addition-upper-dedekind-real-numbers public @@ -26,6 +28,7 @@ open import real-numbers.difference-real-numbers public open import real-numbers.distance-real-numbers public open import real-numbers.enclosing-closed-rational-intervals-real-numbers public open import real-numbers.equality-real-numbers public +open import real-numbers.field-of-real-numbers public open import real-numbers.finitely-enumerable-subsets-real-numbers public open import real-numbers.geometric-sequences-real-numbers public open import real-numbers.inequalities-addition-and-subtraction-real-numbers public @@ -48,6 +51,7 @@ open import real-numbers.large-multiplicative-monoid-of-real-numbers public open import real-numbers.large-ring-of-real-numbers public open import real-numbers.limits-sequences-real-numbers public open import real-numbers.lipschitz-continuity-multiplication-real-numbers public +open import real-numbers.local-ring-of-real-numbers public open import real-numbers.located-metric-space-of-real-numbers public open import real-numbers.lower-dedekind-real-numbers public open import real-numbers.maximum-finite-families-real-numbers public diff --git a/src/real-numbers/addition-negative-real-numbers.lagda.md b/src/real-numbers/addition-negative-real-numbers.lagda.md new file mode 100644 index 0000000000..c3e3cef113 --- /dev/null +++ b/src/real-numbers/addition-negative-real-numbers.lagda.md @@ -0,0 +1,85 @@ +# Addition of negative real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.addition-negative-real-numbers where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.functoriality-disjunction +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.negative-real-numbers +open import real-numbers.positive-and-negative-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +The [negative](real-numbers.negative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are closed under +[addition](real-numbers.addition-real-numbers.md). + +## Definition + +```agda +abstract + is-negative-add-ℝ : + {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → is-negative-ℝ x → is-negative-ℝ y → + is-negative-ℝ (x +ℝ y) + is-negative-add-ℝ {x = x} {y = y} x<0 y<0 = + transitive-le-ℝ + ( x +ℝ y) + ( x) + ( zero-ℝ) + ( x<0) + ( tr + ( le-ℝ (x +ℝ y)) + ( right-unit-law-add-ℝ x) + ( preserves-le-left-add-ℝ x y zero-ℝ y<0)) + +add-ℝ⁻ : {l1 l2 : Level} → ℝ⁻ l1 → ℝ⁻ l2 → ℝ⁻ (l1 ⊔ l2) +add-ℝ⁻ (x , x<0) (y , y<0) = (add-ℝ x y , is-negative-add-ℝ x<0 y<0) + +infixl 35 _+ℝ⁻_ + +_+ℝ⁻_ : {l1 l2 : Level} → ℝ⁻ l1 → ℝ⁻ l2 → ℝ⁻ (l1 ⊔ l2) +_+ℝ⁻_ = add-ℝ⁻ +``` + +## Properties + +### If `x + y` is negative, `x` or `y` is negative + +```agda +abstract + is-negative-either-is-negative-add-ℝ : + {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → is-negative-ℝ (x +ℝ y) → + disjunction-type (is-negative-ℝ x) (is-negative-ℝ y) + is-negative-either-is-negative-add-ℝ x y x+y<0 = + map-disjunction + ( is-negative-is-positive-neg-ℝ x) + ( is-negative-is-positive-neg-ℝ y) + ( is-positive-either-is-positive-add-ℝ + ( neg-ℝ x) + ( neg-ℝ y) + ( tr + ( is-positive-ℝ) + ( distributive-neg-add-ℝ x y) + ( neg-is-negative-ℝ (x +ℝ y) x+y<0))) +``` diff --git a/src/real-numbers/addition-nonzero-real-numbers.lagda.md b/src/real-numbers/addition-nonzero-real-numbers.lagda.md new file mode 100644 index 0000000000..e59f5b96f1 --- /dev/null +++ b/src/real-numbers/addition-nonzero-real-numbers.lagda.md @@ -0,0 +1,56 @@ +# Addition of nonzero real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.addition-nonzero-real-numbers where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.functoriality-disjunction +open import foundation.universe-levels + +open import real-numbers.addition-negative-real-numbers +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.nonzero-real-numbers +``` + +
+ +## Idea + +On this page we describe properties of +[addition](real-numbers.addition-real-numbers.md) of +[nonzero](real-numbers.nonzero-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md). + +## Properties + +### If `x + y` is nonzero, `x` is nonzero or `y` is nonzero + +```agda +abstract + is-nonzero-either-is-nonzero-add-ℝ : + {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → + is-nonzero-ℝ (x +ℝ y) → + disjunction-type (is-nonzero-ℝ x) (is-nonzero-ℝ y) + is-nonzero-either-is-nonzero-add-ℝ x y = + elim-disjunction + ( is-nonzero-prop-ℝ x ∨ is-nonzero-prop-ℝ y) + ( λ x+y<0 → + map-disjunction + ( inl-disjunction) + ( inl-disjunction) + ( is-negative-either-is-negative-add-ℝ x y x+y<0)) + ( λ 0Imports + +```agda +open import commutative-algebra.heyting-fields +open import commutative-algebra.invertible-elements-commutative-rings +open import commutative-algebra.trivial-commutative-rings + +open import elementary-number-theory.rational-numbers + +open import foundation.dependent-pair-types +open import foundation.identity-types +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.large-ring-of-real-numbers +open import real-numbers.local-ring-of-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 +open import real-numbers.similarity-real-numbers +``` + +
+ +## Idea + +The [real numbers](real-numbers.dedekind-real-numbers.md) form a +[Heyting field](commutative-algebra.heyting-fields.md) at each +[universe level](foundation.universe-levels.md). + +## Definition + +```agda +abstract + is-zero-is-noninvertible-commutative-ring-ℝ : + (l : Level) (x : ℝ l) → + ¬ is-invertible-element-Commutative-Ring (commutative-ring-ℝ l) x → + x ＝ raise-ℝ l zero-ℝ + is-zero-is-noninvertible-commutative-ring-ℝ l x ¬inv-x = + eq-sim-ℝ + ( sim-nonapart-ℝ _ _ + ( λ x#raise-l-zero → + ¬inv-x + ( is-invertible-is-nonzero-ℝ + ( x) + ( apart-right-sim-ℝ + ( x) + ( raise-ℝ l zero-ℝ) + ( zero-ℝ) + ( sim-raise-ℝ' l zero-ℝ) + ( x#raise-l-zero))))) + + is-heyting-field-local-commutative-ring-ℝ : + (l : Level) → + is-heyting-field-Local-Commutative-Ring (local-commutative-ring-ℝ l) + is-heyting-field-local-commutative-ring-ℝ l = + ( neq-raise-zero-one-ℝ l , + is-zero-is-noninvertible-commutative-ring-ℝ l) + +heyting-field-ℝ : (l : Level) → Heyting-Field (lsuc l) +heyting-field-ℝ l = + ( local-commutative-ring-ℝ l , + is-heyting-field-local-commutative-ring-ℝ l) +``` diff --git a/src/real-numbers/local-ring-of-real-numbers.lagda.md b/src/real-numbers/local-ring-of-real-numbers.lagda.md new file mode 100644 index 0000000000..e0445ee319 --- /dev/null +++ b/src/real-numbers/local-ring-of-real-numbers.lagda.md @@ -0,0 +1,50 @@ +# The local ring of Dedekind real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.local-ring-of-real-numbers where +``` + +
Imports + +```agda +open import commutative-algebra.local-commutative-rings + +open import foundation.dependent-pair-types +open import foundation.functoriality-disjunction +open import foundation.universe-levels + +open import real-numbers.addition-nonzero-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.large-ring-of-real-numbers +open import real-numbers.multiplicative-inverses-nonzero-real-numbers +open import real-numbers.nonzero-real-numbers +``` + +
+ +## Idea + +The [ring of real numbers](real-numbers.large-ring-of-real-numbers.md) is a +[local](commutative-algebra.local-commutative-rings.md) +[commutative ring](commutative-algebra.commutative-rings.md). + +## Definition + +```agda +is-local-commutative-ring-ℝ : + (l : Level) → is-local-Commutative-Ring (commutative-ring-ℝ l) +is-local-commutative-ring-ℝ l x y is-invertible-x+y = + map-disjunction + ( is-invertible-is-nonzero-ℝ x) + ( is-invertible-is-nonzero-ℝ y) + ( is-nonzero-either-is-nonzero-add-ℝ + ( x) + ( y) + ( is-nonzero-is-invertible-ℝ (x +ℝ y) is-invertible-x+y)) + +local-commutative-ring-ℝ : (l : Level) → Local-Commutative-Ring (lsuc l) +local-commutative-ring-ℝ l = + ( commutative-ring-ℝ l , is-local-commutative-ring-ℝ l) +``` diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md index aedb75f632..bd117101ec 100644 --- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md @@ -210,6 +210,20 @@ abstract opaque is-nonzero-has-left-inverse-mul-ℝ x y xy=1 = is-nonzero-has-right-inverse-mul-ℝ y x ( tr (λ z → sim-ℝ z one-ℝ) (commutative-mul-ℝ _ _) xy=1) + + is-nonzero-is-invertible-ℝ : + {l : Level} (x : ℝ l) → + is-invertible-element-Commutative-Ring (commutative-ring-ℝ l) x → + is-nonzero-ℝ x + is-nonzero-is-invertible-ℝ {l} x (y , xy=1 , _) = + is-nonzero-has-right-inverse-mul-ℝ x y + ( inv-tr + ( λ z → sim-ℝ z one-ℝ) + ( xy=1) + ( symmetric-sim-ℝ + { x = one-ℝ} + { y = raise-ℝ l one-ℝ} + ( sim-raise-ℝ l one-ℝ))) ``` ### The multiplicative inverse is unique diff --git a/src/real-numbers/positive-and-negative-real-numbers.lagda.md b/src/real-numbers/positive-and-negative-real-numbers.lagda.md index 18f7f33b89..e5964a4b3d 100644 --- a/src/real-numbers/positive-and-negative-real-numbers.lagda.md +++ b/src/real-numbers/positive-and-negative-real-numbers.lagda.md @@ -9,7 +9,10 @@ module real-numbers.positive-and-negative-real-numbers where
Imports ```agda +open import foundation.cartesian-product-types open import foundation.dependent-pair-types +open import foundation.logical-equivalences +open import foundation.negation open import foundation.transport-along-identifications open import foundation.universe-levels @@ -78,6 +81,38 @@ neg-ℝ⁻ : {l : Level} → ℝ⁻ l → ℝ⁺ l neg-ℝ⁻ (x , is-neg-x) = (neg-ℝ x , neg-is-negative-ℝ x is-neg-x) ``` +### A real number is negative if and only if its negation is positive + +```agda +abstract + is-negative-is-positive-neg-ℝ : + {l : Level} (x : ℝ l) → is-positive-ℝ (neg-ℝ x) → is-negative-ℝ x + is-negative-is-positive-neg-ℝ x 0<-x = + tr is-negative-ℝ (neg-neg-ℝ x) (neg-is-positive-ℝ (neg-ℝ x) 0<-x) + +is-negative-iff-neg-is-positive-ℝ : + {l : Level} (x : ℝ l) → is-negative-ℝ x ↔ is-positive-ℝ (neg-ℝ x) +is-negative-iff-neg-is-positive-ℝ x = + ( neg-is-negative-ℝ x , + is-negative-is-positive-neg-ℝ x) +``` + +### A real number is positive if and only if its negation is negative + +```agda +abstract + is-positive-is-negative-neg-ℝ : + {l : Level} (x : ℝ l) → is-negative-ℝ (neg-ℝ x) → is-positive-ℝ x + is-positive-is-negative-neg-ℝ x -x<0 = + tr is-positive-ℝ (neg-neg-ℝ x) (neg-is-negative-ℝ (neg-ℝ x) -x<0) + +is-positive-iff-neg-is-negative-ℝ : + {l : Level} (x : ℝ l) → is-positive-ℝ x ↔ is-negative-ℝ (neg-ℝ x) +is-positive-iff-neg-is-negative-ℝ x = + ( neg-is-positive-ℝ x , + is-positive-is-negative-neg-ℝ x) +``` + ### If a nonnegative real number `x` is less than a real number `y`, `y` is positive ```agda @@ -87,3 +122,13 @@ abstract is-positive-ℝ y is-positive-le-ℝ⁰⁺ (x , 0≤x) y = concatenate-leq-le-ℝ zero-ℝ x y 0≤x ``` + +### Real numbers are not both negative and nonnegative + +```agda +abstract + is-not-negative-and-nonnegative-ℝ : + {l : Level} {x : ℝ l} → ¬ (is-negative-ℝ x × is-nonnegative-ℝ x) + is-not-negative-and-nonnegative-ℝ {x = x} (x<0 , 0≤x) = + not-leq-le-ℝ x zero-ℝ x<0 0≤x +``` diff --git a/src/real-numbers/raising-universe-levels-real-numbers.lagda.md b/src/real-numbers/raising-universe-levels-real-numbers.lagda.md index c3f1b1d417..744062a62f 100644 --- a/src/real-numbers/raising-universe-levels-real-numbers.lagda.md +++ b/src/real-numbers/raising-universe-levels-real-numbers.lagda.md @@ -167,12 +167,16 @@ module _ ### Reals are similar to their raised-universe equivalents ```agda -opaque +abstract opaque unfolding sim-ℝ - sim-raise-ℝ : {l0 : Level} → (l : Level) → (x : ℝ l0) → sim-ℝ x (raise-ℝ l x) + sim-raise-ℝ : {l0 : Level} (l : Level) (x : ℝ l0) → sim-ℝ x (raise-ℝ l x) pr1 (sim-raise-ℝ l x) _ = map-raise pr2 (sim-raise-ℝ l x) _ = map-inv-raise + +abstract + sim-raise-ℝ' : {l0 : Level} (l : Level) (x : ℝ l0) → sim-ℝ (raise-ℝ l x) x + sim-raise-ℝ' l x = symmetric-sim-ℝ (sim-raise-ℝ l x) ``` ### Raising a real to its own level is the identity diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index 381ab6c0c6..3a435d0723 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -25,6 +25,7 @@ open import foundation.equivalences open import foundation.function-types open import foundation.identity-types open import foundation.injective-maps +open import foundation.negated-equality open import foundation.negation open import foundation.propositions open import foundation.retractions @@ -307,3 +308,24 @@ abstract opaque ( q) ( tr (λ x → is-in-lower-cut-ℝ x q) pℝ=qℝ q