From f879a802877de6a94a2b1eb6ca4672a2c8f1bde9 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 5 Mar 2026 08:49:43 -0800 Subject: [PATCH 1/6] Progress --- src/linear-algebra.lagda.md | 1 + .../trivial-left-modules-rings.lagda.md | 59 +++++++++++++++++++ 2 files changed, 60 insertions(+) create mode 100644 src/linear-algebra/trivial-left-modules-rings.lagda.md diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index 671203d4ea4..487ce8b7532 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -80,6 +80,7 @@ open import linear-algebra.subspaces-vector-spaces public open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces public open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public open import linear-algebra.transposition-matrices public +open import linear-algebra.trivial-left-modules-rings public open import linear-algebra.tuples-on-commutative-monoids public open import linear-algebra.tuples-on-commutative-rings public open import linear-algebra.tuples-on-commutative-semirings public diff --git a/src/linear-algebra/trivial-left-modules-rings.lagda.md b/src/linear-algebra/trivial-left-modules-rings.lagda.md new file mode 100644 index 00000000000..b3e99d83edd --- /dev/null +++ b/src/linear-algebra/trivial-left-modules-rings.lagda.md @@ -0,0 +1,59 @@ +# Trivial left modules over rings + +```agda +module linear-algebra.trivial-left-modules-rings where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.unit-type +open import foundation.universe-levels + +open import group-theory.trivial-groups + +open import linear-algebra.left-modules-rings + +open import ring-theory.rings +``` + +
+ +## Idea + +## Definition + +### The property of being a trivial module + +```agda +module _ + {l1 l2 : Level} + (R : Ring l1) + (M : left-module-Ring l2 R) + where + + is-trivial-prop-left-module-Ring : Prop l2 + is-trivial-prop-left-module-Ring = is-contr-Prop (type-left-module-Ring R M) + + is-trivial-left-module-Ring : UU l2 + is-trivial-left-module-Ring = type-Prop is-trivial-prop-left-module-Ring +``` + +### The trivial module + +```agda +trivial-left-module-Ring : {l : Level} (R : Ring l) → left-module-Ring lzero R +trivial-left-module-Ring R = + make-left-module-Ring + ( R) + ( trivial-Ab) + ( λ _ _ → star) + ( λ _ _ _ → refl) + ( λ _ _ _ → refl) + ( λ _ → refl) + ( λ _ _ _ → refl) +``` From 9d471e92742fc7a06b18642c5b77f08657827dc9 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 5 Jun 2026 16:37:22 -0700 Subject: [PATCH 2/6] Trivial vector spaces --- src/linear-algebra.lagda.md | 2 + ...al-left-modules-commutative-rings.lagda.md | 67 +++++++++++++++++++ .../trivial-left-modules-rings.lagda.md | 36 +++++++--- .../trivial-vector-spaces.lagda.md | 63 +++++++++++++++++ 4 files changed, 158 insertions(+), 10 deletions(-) create mode 100644 src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md create mode 100644 src/linear-algebra/trivial-vector-spaces.lagda.md diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index 9140071566d..b75c5dcb482 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -93,7 +93,9 @@ open import linear-algebra.subspaces-vector-spaces public open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces public open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public open import linear-algebra.transposition-matrices public +open import linear-algebra.trivial-left-modules-commutative-rings public open import linear-algebra.trivial-left-modules-rings public +open import linear-algebra.trivial-vector-spaces public open import linear-algebra.tuples-on-commutative-monoids public open import linear-algebra.tuples-on-commutative-rings public open import linear-algebra.tuples-on-commutative-semirings public diff --git a/src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md b/src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md new file mode 100644 index 00000000000..d6810576d6a --- /dev/null +++ b/src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md @@ -0,0 +1,67 @@ +# Trivial left modules over commutative rings + +```agda +module linear-algebra.trivial-left-modules-commutative-rings where +``` + +
Imports + +```agda +open import commutative-algebra.commutative-rings + +open import foundation.propositions +open import foundation.universe-levels + +open import linear-algebra.left-modules-commutative-rings +open import linear-algebra.trivial-left-modules-rings +``` + +
+ +## Idea + +The +{{#concept "trivial module" Disambiguation="over a commutative ring" Agda=trivial-left-module-Commutative-Commutative-Ring}} +over a [commutative ring](commutative-algebra.commutative-rings.md) `R` is the +[left module](linear-algebra.left-modules-commutative-rings.md) over `R` +consisting of exactly one element, `0`. + +## Definition + +### The property of being a trivial module + +```agda +module _ + {l1 l2 : Level} + (R : Commutative-Ring l1) + (M : left-module-Commutative-Ring l2 R) + where + + is-trivial-prop-left-module-Commutative-Ring : Prop l2 + is-trivial-prop-left-module-Commutative-Ring = + is-trivial-prop-left-module-Ring (ring-Commutative-Ring R) M + + is-trivial-left-module-Commutative-Ring : UU l2 + is-trivial-left-module-Commutative-Ring = + type-Prop is-trivial-prop-left-module-Commutative-Ring +``` + +### The trivial module + +```agda +module _ + {l : Level} + (R : Commutative-Ring l) + where + + trivial-left-module-Commutative-Ring : left-module-Commutative-Ring lzero R + trivial-left-module-Commutative-Ring = + trivial-left-module-Ring (ring-Commutative-Ring R) + + is-trivial-trivial-left-module-Commutative-Ring : + is-trivial-left-module-Commutative-Ring + ( R) + ( trivial-left-module-Commutative-Ring) + is-trivial-trivial-left-module-Commutative-Ring = + is-trivial-trivial-left-module-Ring (ring-Commutative-Ring R) +``` diff --git a/src/linear-algebra/trivial-left-modules-rings.lagda.md b/src/linear-algebra/trivial-left-modules-rings.lagda.md index b3e99d83edd..e89ead4c310 100644 --- a/src/linear-algebra/trivial-left-modules-rings.lagda.md +++ b/src/linear-algebra/trivial-left-modules-rings.lagda.md @@ -11,6 +11,7 @@ open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositions +open import foundation.subuniverse-of-contractible-types open import foundation.unit-type open import foundation.universe-levels @@ -25,6 +26,12 @@ open import ring-theory.rings ## Idea +The +{{#concept "trivial module" Disambiguation="over a ring" Agda=trivial-left-module-Ring}} +over a [ring](ring-theory.rings.md) `R` is the +[left module](linear-algebra.left-modules-rings.md) over `R` consisting of +exactly one element, `0`. + ## Definition ### The property of being a trivial module @@ -46,14 +53,23 @@ module _ ### The trivial module ```agda -trivial-left-module-Ring : {l : Level} (R : Ring l) → left-module-Ring lzero R -trivial-left-module-Ring R = - make-left-module-Ring - ( R) - ( trivial-Ab) - ( λ _ _ → star) - ( λ _ _ _ → refl) - ( λ _ _ _ → refl) - ( λ _ → refl) - ( λ _ _ _ → refl) +module _ + {l : Level} + (R : Ring l) + where + + trivial-left-module-Ring : left-module-Ring lzero R + trivial-left-module-Ring = + make-left-module-Ring + ( R) + ( trivial-Ab) + ( λ _ _ → star) + ( λ _ _ _ → refl) + ( λ _ _ _ → refl) + ( λ _ → refl) + ( λ _ _ _ → refl) + + is-trivial-trivial-left-module-Ring : + is-trivial-left-module-Ring R trivial-left-module-Ring + is-trivial-trivial-left-module-Ring = is-contr-unit ``` diff --git a/src/linear-algebra/trivial-vector-spaces.lagda.md b/src/linear-algebra/trivial-vector-spaces.lagda.md new file mode 100644 index 00000000000..e019fc1bf23 --- /dev/null +++ b/src/linear-algebra/trivial-vector-spaces.lagda.md @@ -0,0 +1,63 @@ +# Trivial vector spaces + +```agda +module linear-algebra.trivial-vector-spaces where +``` + +
Imports + +```agda +open import commutative-algebra.heyting-fields + +open import foundation.propositions +open import foundation.universe-levels + +open import linear-algebra.trivial-left-modules-rings +open import linear-algebra.vector-spaces +``` + +
+ +## Idea + +The +{{#concept "trivial vector space" Disambiguation="over a Heyting field" Agda=trivial-Vector-Space}} +over a [Heyting field](commutative-algebra.heyting-fields.md) `K` is the +[vector space](linear-algebra.vector-spaces.md) over `K` consisting of exactly +one element, `0`. + +## Definition + +### The property of being a trivial vector space + +```agda +module _ + {l1 l2 : Level} + (K : Heyting-Field l1) + (V : Vector-Space l2 K) + where + + is-trivial-prop-Vector-Space : Prop l2 + is-trivial-prop-Vector-Space = + is-trivial-prop-left-module-Ring (ring-Heyting-Field K) V + + is-trivial-Vector-Space : UU l2 + is-trivial-Vector-Space = type-Prop is-trivial-prop-Vector-Space +``` + +### The trivial vector space + +```agda +module _ + {l : Level} + (K : Heyting-Field l) + where + + trivial-Vector-Space : Vector-Space lzero K + trivial-Vector-Space = trivial-left-module-Ring (ring-Heyting-Field K) + + is-trivial-trivial-Vector-Space : + is-trivial-Vector-Space K trivial-Vector-Space + is-trivial-trivial-Vector-Space = + is-trivial-trivial-left-module-Ring (ring-Heyting-Field K) +``` From e1a0f80c00b2f58c53003d8c47a2c12482a0e0a1 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 5 Jun 2026 16:39:24 -0700 Subject: [PATCH 3/6] Fix concept link --- .../trivial-left-modules-commutative-rings.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md b/src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md index d6810576d6a..559393b76ca 100644 --- a/src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md +++ b/src/linear-algebra/trivial-left-modules-commutative-rings.lagda.md @@ -21,7 +21,7 @@ open import linear-algebra.trivial-left-modules-rings ## Idea The -{{#concept "trivial module" Disambiguation="over a commutative ring" Agda=trivial-left-module-Commutative-Commutative-Ring}} +{{#concept "trivial module" Disambiguation="over a commutative ring" Agda=trivial-left-module-Commutative-Ring}} over a [commutative ring](commutative-algebra.commutative-rings.md) `R` is the [left module](linear-algebra.left-modules-commutative-rings.md) over `R` consisting of exactly one element, `0`. From e5e40d1dfa1e99eefd64c3cd860452a896a30683 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 6 Jun 2026 16:39:23 -0700 Subject: [PATCH 4/6] Progress --- src/foundation/binary-relations.lagda.md | 5 +- src/linear-algebra.lagda.md | 2 + ...artness-normed-real-vector-spaces.lagda.md | 168 ++++++++++++++++++ ...trivial-normed-real-vector-spaces.lagda.md | 16 ++ .../normed-real-vector-spaces.lagda.md | 6 + src/metric-spaces.lagda.md | 1 + .../perfect-metric-spaces.lagda.md | 42 +++++ .../positive-real-numbers.lagda.md | 59 +++++- 8 files changed, 293 insertions(+), 6 deletions(-) create mode 100644 src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md create mode 100644 src/linear-algebra/nontrivial-normed-real-vector-spaces.lagda.md create mode 100644 src/metric-spaces/perfect-metric-spaces.lagda.md diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md index ff2658c47c6..120e7fa65af 100644 --- a/src/foundation/binary-relations.lagda.md +++ b/src/foundation/binary-relations.lagda.md @@ -32,8 +32,9 @@ open import foundation-core.torsorial-type-families ## Idea -A **binary relation** on a type `A` is a family of types `R x y` depending on -two variables `x y : A`. In the special case where each `R x y` is a +A {{#concept "binary relation" WDID=Q130901 WD="binary relation" Agda=Relation}} +on a type `A` is a family of types `R x y` depending on two variables `x y : A`. +In the special case where each `R x y` is a [proposition](foundation-core.propositions.md), we say that the relation is valued in propositions. Thus, we take a general relation to mean a _proof-relevant_ relation. diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index dfe35b96461..1da8c3b682d 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -7,6 +7,7 @@ module linear-algebra where open import linear-algebra.addition-linear-maps-left-modules-commutative-rings public open import linear-algebra.addition-linear-maps-left-modules-rings public +open import linear-algebra.apartness-normed-real-vector-spaces public open import linear-algebra.bilinear-forms-real-vector-spaces public open import linear-algebra.bilinear-maps-left-modules-commutative-rings public open import linear-algebra.bilinear-maps-left-modules-rings public @@ -64,6 +65,7 @@ open import linear-algebra.matrices public open import linear-algebra.matrices-on-rings public open import linear-algebra.multiplication-matrices public open import linear-algebra.negation-linear-maps-left-modules-rings public +open import linear-algebra.nontrivial-normed-real-vector-spaces public open import linear-algebra.normed-complex-vector-spaces public open import linear-algebra.normed-real-vector-spaces public open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public diff --git a/src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md b/src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md new file mode 100644 index 00000000000..910f2a31bd4 --- /dev/null +++ b/src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md @@ -0,0 +1,168 @@ +# Apartness in normed real vector spaces + +```agda +module linear-algebra.apartness-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import foundation.apartness-relations +open import foundation.binary-relations +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.functoriality-disjunction +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.negation +open import foundation.tight-apartness-relations +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import linear-algebra.normed-real-vector-spaces + +open import metric-spaces.apartness-located-metric-spaces + +open import real-numbers.inequality-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.zero-real-numbers +``` + +
+ +## Idea + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + apart-prop-Normed-ℝ-Vector-Space : + Relation-Prop l1 (type-Normed-ℝ-Vector-Space V) + apart-prop-Normed-ℝ-Vector-Space v w = + is-positive-prop-ℝ (dist-Normed-ℝ-Vector-Space V v w) + + apart-Normed-ℝ-Vector-Space : + Relation l1 (type-Normed-ℝ-Vector-Space V) + apart-Normed-ℝ-Vector-Space = + type-Relation-Prop apart-prop-Normed-ℝ-Vector-Space +``` + +## Properties + +### Two elements are apart in a normed real vector space if and only if they are apart in the corresponding located metric space + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (v w : type-Normed-ℝ-Vector-Space V) + where abstract + + apart-located-metric-space-apart-Normed-ℝ-Vector-Space : + apart-Normed-ℝ-Vector-Space V v w → + apart-Located-Metric-Space + ( located-metric-space-Normed-ℝ-Vector-Space V) + ( v) + ( w) + apart-located-metric-space-apart-Normed-ℝ-Vector-Space = + exists-not-le-positive-rational-is-positive-ℝ + ( dist-Normed-ℝ-Vector-Space V v w) + + apart-apart-located-metric-space-Normed-ℝ-Vector-Space : + apart-Located-Metric-Space + ( located-metric-space-Normed-ℝ-Vector-Space V) + ( v) + ( w) → + apart-Normed-ℝ-Vector-Space V v w + apart-apart-located-metric-space-Normed-ℝ-Vector-Space = + is-positive-exists-not-le-positive-rational-ℝ + ( dist-Normed-ℝ-Vector-Space V v w) +``` + +### Apartness in a normed real vector space is an apartness relation + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + abstract + antirefl-apart-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + ¬ (apart-Normed-ℝ-Vector-Space V v v) + antirefl-apart-Normed-ℝ-Vector-Space v = + is-not-positive-is-zero-ℝ + ( dist-Normed-ℝ-Vector-Space V v v) + ( refl-dist-Normed-ℝ-Vector-Space V v) + + symmetric-apart-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space V) → + apart-Normed-ℝ-Vector-Space V v w → apart-Normed-ℝ-Vector-Space V w v + symmetric-apart-Normed-ℝ-Vector-Space v w = + tr is-positive-ℝ (symmetric-dist-Normed-ℝ-Vector-Space V v w) + + cotransitive-apart-Normed-ℝ-Vector-Space : + (v w x : type-Normed-ℝ-Vector-Space V) → + apart-Normed-ℝ-Vector-Space V v x → + disjunction-type + ( apart-Normed-ℝ-Vector-Space V v w) + ( apart-Normed-ℝ-Vector-Space V w x) + cotransitive-apart-Normed-ℝ-Vector-Space v w x 0Imports + +```agda +open import foundation.universe-levels + +open import linear-algebra.apartness-normed-real-vector-spaces +open import linear-algebra.normed-real-vector-spaces +``` + + diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md index 53a58db9b70..531d6189c3c 100644 --- a/src/linear-algebra/normed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md @@ -211,6 +211,12 @@ module _ nonnegative-dist-Seminormed-ℝ-Vector-Space ( seminormed-vector-space-Normed-ℝ-Vector-Space) + is-nonnegative-dist-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space) → + is-nonnegative-ℝ (dist-Normed-ℝ-Vector-Space v w) + is-nonnegative-dist-Normed-ℝ-Vector-Space v w = + is-nonnegative-real-ℝ⁰⁺ (nonnegative-dist-Normed-ℝ-Vector-Space v w) + abstract is-extensional-norm-Normed-ℝ-Vector-Space : (v : type-Normed-ℝ-Vector-Space) → diff --git a/src/metric-spaces.lagda.md b/src/metric-spaces.lagda.md index 89f28adc578..616b3953625 100644 --- a/src/metric-spaces.lagda.md +++ b/src/metric-spaces.lagda.md @@ -157,6 +157,7 @@ open import metric-spaces.nets-located-metric-spaces public open import metric-spaces.nets-metric-spaces public open import metric-spaces.open-subsets-located-metric-spaces public open import metric-spaces.open-subsets-metric-spaces public +open import metric-spaces.perfect-metric-spaces public open import metric-spaces.pointwise-continuous-maps-metric-spaces public open import metric-spaces.pointwise-epsilon-delta-continuous-maps-metric-spaces public open import metric-spaces.poset-of-rational-neighborhood-relations public diff --git a/src/metric-spaces/perfect-metric-spaces.lagda.md b/src/metric-spaces/perfect-metric-spaces.lagda.md new file mode 100644 index 00000000000..fa27df14cf7 --- /dev/null +++ b/src/metric-spaces/perfect-metric-spaces.lagda.md @@ -0,0 +1,42 @@ +# Perfect metric spaces + +```agda +module metric-spaces.perfect-metric-spaces where +``` + +
Imports + +```agda +open import foundation.full-subtypes +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.accumulation-points-subsets-located-metric-spaces +open import metric-spaces.located-metric-spaces +``` + +
+ +## Idea + +## Definition + +```agda +is-perfect-prop-Located-Metric-Space : + {l1 l2 : Level} → subtype (l1 ⊔ l2) (Located-Metric-Space l1 l2) +is-perfect-prop-Located-Metric-Space X = + is-full-subtype-Prop + ( is-accumulation-point-prop-subset-Located-Metric-Space + ( X) + ( full-subtype lzero (type-Located-Metric-Space X))) + +is-perfect-Located-Metric-Space : + {l1 l2 : Level} → Located-Metric-Space l1 l2 → UU (l1 ⊔ l2) +is-perfect-Located-Metric-Space = + is-in-subtype is-perfect-prop-Located-Metric-Space + +Perfect-Metric-Space : (l1 l2 : Level) → UU (lsuc (l1 ⊔ l2)) +Perfect-Metric-Space l1 l2 = + type-subtype (is-perfect-prop-Located-Metric-Space {l1} {l2}) +``` diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md index 3673dcb021c..a123f1d658a 100644 --- a/src/real-numbers/positive-real-numbers.lagda.md +++ b/src/real-numbers/positive-real-numbers.lagda.md @@ -35,6 +35,8 @@ open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels +open import logic.functoriality-existential-quantification + open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers @@ -45,6 +47,7 @@ open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers +open import real-numbers.zero-real-numbers ``` @@ -216,6 +219,31 @@ exists-ℚ⁺-in-lower-cut-ℝ⁺ : exists-ℚ⁺-in-lower-cut-ℝ⁺ = ind-Σ exists-ℚ⁺-in-lower-cut-is-positive-ℝ ``` +### A real number is positive if and only if there exists a lesser positive rational number + +```agda +module _ + {l : Level} + (x : ℝ l) + where abstract + + exists-lesser-positive-rational-is-positive-ℝ : + is-positive-ℝ x → exists ℚ⁺ (λ q → le-prop-ℝ (real-ℚ⁺ q) x) + exists-lesser-positive-rational-is-positive-ℝ 0 Date: Sun, 7 Jun 2026 15:55:51 -0700 Subject: [PATCH 5/6] Progress --- src/group-theory/abelian-groups.lagda.md | 20 ++ src/group-theory/groups.lagda.md | 20 ++ src/linear-algebra.lagda.md | 3 + ...artness-normed-real-vector-spaces.lagda.md | 6 + ...trivial-normed-real-vector-spaces.lagda.md | 242 ++++++++++++++++++ ...vectors-normed-real-vector-spaces.lagda.md | 170 ++++++++++++ .../normed-real-vector-spaces.lagda.md | 157 +++++++++++- .../seminormed-real-vector-spaces.lagda.md | 11 + .../trivial-real-vector-spaces.lagda.md | 62 +++++ ...vectors-normed-real-vector-spaces.lagda.md | 121 +++++++++ .../perfect-metric-spaces.lagda.md | 9 + .../large-ring-of-real-numbers.lagda.md | 4 + ...ositive-and-negative-real-numbers.lagda.md | 21 ++ .../positive-real-numbers.lagda.md | 3 + .../rational-real-numbers.lagda.md | 3 + 15 files changed, 844 insertions(+), 8 deletions(-) create mode 100644 src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md create mode 100644 src/linear-algebra/trivial-real-vector-spaces.lagda.md create mode 100644 src/linear-algebra/unit-vectors-normed-real-vector-spaces.lagda.md diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md index 962f85ee6ef..18de2e76071 100644 --- a/src/group-theory/abelian-groups.lagda.md +++ b/src/group-theory/abelian-groups.lagda.md @@ -1042,6 +1042,26 @@ module _ ( nullifies-commutator-normal-subgroup-hom-group-Ab) ``` +### Unit laws of right subtraction + +```agda +module _ + {l : Level} + (G : Ab l) + (g : type-Ab G) + where abstract + + right-unit-law-right-subtraction-Ab : + right-subtraction-Ab G g (zero-Ab G) ＝ g + right-unit-law-right-subtraction-Ab = + right-unit-law-right-div-Group (group-Ab G) g + + left-unit-law-right-subtraction-Ab : + right-subtraction-Ab G (zero-Ab G) g ＝ neg-Ab G g + left-unit-law-right-subtraction-Ab = + left-unit-law-right-div-Group (group-Ab G) g +``` + ## See also - [Large abelian groups](group-theory.large-abelian-groups.md), which span diff --git a/src/group-theory/groups.lagda.md b/src/group-theory/groups.lagda.md index 85bfdc1f958..a4bef5b40f1 100644 --- a/src/group-theory/groups.lagda.md +++ b/src/group-theory/groups.lagda.md @@ -681,3 +681,23 @@ module _ pr1 pointed-type-with-aut-Group = pointed-type-Group G pr2 pointed-type-with-aut-Group = equiv-mul-Group G g ``` + +### Unit laws of right division + +```agda +module _ + {l : Level} + (G : Group l) + (g : type-Group G) + where abstract + + right-unit-law-right-div-Group : + right-div-Group G g (unit-Group G) ＝ g + right-unit-law-right-div-Group = + ap-mul-Group G refl (inv-unit-Group G) ∙ right-unit-law-mul-Group G g + + left-unit-law-right-div-Group : + right-div-Group G (unit-Group G) g ＝ inv-Group G g + left-unit-law-right-div-Group = + left-unit-law-mul-Group G (inv-Group G g) +``` diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index 94896ccbc6f..d2aaa5de0d7 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -66,6 +66,7 @@ open import linear-algebra.matrices-on-rings public open import linear-algebra.multiplication-matrices public open import linear-algebra.negation-linear-maps-left-modules-rings public open import linear-algebra.nontrivial-normed-real-vector-spaces public +open import linear-algebra.nonzero-vectors-normed-real-vector-spaces public open import linear-algebra.normed-complex-vector-spaces public open import linear-algebra.normed-real-vector-spaces public open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public @@ -97,6 +98,7 @@ open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public open import linear-algebra.transposition-matrices public open import linear-algebra.trivial-left-modules-commutative-rings public open import linear-algebra.trivial-left-modules-rings public +open import linear-algebra.trivial-real-vector-spaces public open import linear-algebra.trivial-vector-spaces public open import linear-algebra.tuples-on-commutative-monoids public open import linear-algebra.tuples-on-commutative-rings public @@ -105,5 +107,6 @@ 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.unit-vectors-normed-real-vector-spaces public open import linear-algebra.vector-spaces public ``` diff --git a/src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md b/src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md index 910f2a31bd4..c3266e4920b 100644 --- a/src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/apartness-normed-real-vector-spaces.lagda.md @@ -36,6 +36,12 @@ open import real-numbers.zero-real-numbers ## Idea +Two points in a +[normed real vector space](linear-algebra.normed-real-vector-spaces.md) are +{{#concept "apart" Disambiguation="in a normed real vector space" Agda=apart-Normed-ℝ-Vector-Space}} +if the distance between them is +[positive](real-numbers.positive-real-numbers.md). + ## Definition ```agda diff --git a/src/linear-algebra/nontrivial-normed-real-vector-spaces.lagda.md b/src/linear-algebra/nontrivial-normed-real-vector-spaces.lagda.md index e041ca12c1c..326ca7c0082 100644 --- a/src/linear-algebra/nontrivial-normed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/nontrivial-normed-real-vector-spaces.lagda.md @@ -1,16 +1,258 @@ # Nontrivial normed real vector spaces ```agda +{-# OPTIONS --lossy-unification #-} + module linear-algebra.nontrivial-normed-real-vector-spaces where ```
Imports ```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.full-subtypes +open import foundation.function-types +open import foundation.functoriality-propositional-truncation +open import foundation.identity-types +open import foundation.inhabited-types +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.raising-universe-levels-unit-type +open import foundation.transport-along-identifications open import foundation.universe-levels open import linear-algebra.apartness-normed-real-vector-spaces +open import linear-algebra.nonzero-vectors-normed-real-vector-spaces open import linear-algebra.normed-real-vector-spaces +open import linear-algebra.trivial-real-vector-spaces +open import linear-algebra.unit-vectors-normed-real-vector-spaces + +open import metric-spaces.accumulation-points-subsets-located-metric-spaces +open import metric-spaces.perfect-metric-spaces + +open import order-theory.large-posets + +open import real-numbers.addition-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.zero-real-numbers ```
+ +## Idea + +A [normed real vector space](linear-algebra.normed-real-vector-spaces.md) `V` is +{{#concept "nontrivial" Disambiguation="normed real vector space" Agda=is-nontrivial-Normed-ℝ-Vector-Space}} +if there [exists](foundation.existential-quantification.md) a +[nonzero vector](linear-algebra.nonzero-vectors-normed-real-vector-spaces.md) in +`V`. + +A normed real vector space is nontrivial +[if and only if](foundation.logical-equivalences.md) it is +[perfect](metric-spaces.perfect-metric-spaces.md) as a +[located metric space](metric-spaces.located-metric-spaces.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + is-nontrivial-prop-Normed-ℝ-Vector-Space : Prop (l1 ⊔ l2) + is-nontrivial-prop-Normed-ℝ-Vector-Space = + ∃ ( type-Normed-ℝ-Vector-Space V) + ( is-nonzero-prop-Normed-ℝ-Vector-Space V) + + is-nontrivial-Normed-ℝ-Vector-Space : UU (l1 ⊔ l2) + is-nontrivial-Normed-ℝ-Vector-Space = + type-Prop is-nontrivial-prop-Normed-ℝ-Vector-Space +``` + +## Properties + +### A normed real vector space is not nontrivial if and only if it is trivial + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + is-trivial-is-not-nontrivial-Normed-ℝ-Vector-Space : + ¬ is-nontrivial-Normed-ℝ-Vector-Space V → + is-trivial-ℝ-Vector-Space (vector-space-Normed-ℝ-Vector-Space V) + is-trivial-is-not-nontrivial-Normed-ℝ-Vector-Space ¬|v|>0 = + ( zero-Normed-ℝ-Vector-Space V , + λ w → + inv + ( is-zero-is-not-nonzero-Normed-ℝ-Vector-Space V w + ( map-neg (intro-exists w) ¬|v|>0))) + + is-not-nontrivial-is-trivial-Normed-ℝ-Vector-Space : + is-trivial-ℝ-Vector-Space (vector-space-Normed-ℝ-Vector-Space V) → + ¬ is-nontrivial-Normed-ℝ-Vector-Space V + is-not-nontrivial-is-trivial-Normed-ℝ-Vector-Space is-contr-V = + elim-exists + ( empty-Prop) + ( λ v → + is-not-positive-is-zero-ℝ + ( map-norm-Normed-ℝ-Vector-Space V v) + ( tr + ( is-zero-ℝ ∘ map-norm-Normed-ℝ-Vector-Space V) + ( eq-is-contr is-contr-V) + ( is-zero-map-norm-zero-Normed-ℝ-Vector-Space V))) +``` + +### If a normed real vector space is nontrivial, it contains a unit vector + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + contains-unit-is-nontrivial-Normed-ℝ-Vector-Space : + is-nontrivial-Normed-ℝ-Vector-Space V → + is-inhabited (unit-Normed-ℝ-Vector-Space V) + contains-unit-is-nontrivial-Normed-ℝ-Vector-Space = + map-trunc-Prop (unit-nonzero-vector-Normed-ℝ-Vector-Space V) +``` + +### If a normed real vector space is nontrivial, it has vectors of every nonnegative length + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (d : ℝ⁰⁺ l1) + where abstract + + exists-vector-with-norm-is-nontrivial-Normed-ℝ-Vector-Space : + is-nontrivial-Normed-ℝ-Vector-Space V → + exists + ( type-Normed-ℝ-Vector-Space V) + ( has-norm-prop-Normed-ℝ-Vector-Space V d) + exists-vector-with-norm-is-nontrivial-Normed-ℝ-Vector-Space = + map-trunc-Prop + ( λ v → + ( normalized-to-norm-nonzero-vector-Normed-ℝ-Vector-Space V d v , + has-norm-normalized-to-norm-nonzero-vector-Normed-ℝ-Vector-Space V + ( d) + ( v))) +``` + +### If a normed real vector space is nontrivial, it is perfect + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + open inequality-reasoning-Large-Poset ℝ-Large-Poset + + is-perfect-is-nontrivial-Normed-ℝ-Vector-Space : + is-nontrivial-Normed-ℝ-Vector-Space V → + is-perfect-Located-Metric-Space + ( located-metric-space-Normed-ℝ-Vector-Space V) + is-perfect-is-nontrivial-Normed-ℝ-Vector-Space NT v = + map-trunc-Prop + ( λ uŵ@(ŵ , |ŵ|=1) → + let + _+V_ = add-Normed-ℝ-Vector-Space V + _*V_ = mul-Normed-ℝ-Vector-Space V + w ε = v +V (raise-real-ℚ⁺ l1 ε *V ŵ) + |wε-v|=ε ε = + ( dist-add-Normed-ℝ-Vector-Space V _ _) ∙ + ( map-norm-mul-positive-unit-Normed-ℝ-Vector-Space V + ( positive-raise-real-ℚ⁺ l1 ε) + ( uŵ)) + |wε-v|≤ε ε = + transitive-leq-ℝ _ _ _ + ( leq-sim-ℝ (sim-raise-ℝ' l1 (real-ℚ⁺ ε))) + ( leq-eq-ℝ (|wε-v|=ε ε)) + is-cauchy-w : + (δ ε : ℚ⁺) → + neighborhood-Normed-ℝ-Metric-Space V (δ +ℚ⁺ ε) (w δ) (w ε) + is-cauchy-w δ ε = + chain-of-inequalities + dist-Normed-ℝ-Vector-Space V (w δ) (w ε) + ≤ dist-Normed-ℝ-Vector-Space V (w δ) v +ℝ + dist-Normed-ℝ-Vector-Space V v (w ε) + by triangular-dist-Normed-ℝ-Vector-Space V (w δ) v (w ε) + ≤ dist-Normed-ℝ-Vector-Space V (w δ) v +ℝ + dist-Normed-ℝ-Vector-Space V (w ε) v + by + leq-eq-ℝ + ( ap-add-ℝ + ( refl) + ( symmetric-dist-Normed-ℝ-Vector-Space V _ _)) + ≤ real-ℚ⁺ δ +ℝ real-ℚ⁺ ε + by preserves-leq-add-ℝ (|wε-v|≤ε δ) (|wε-v|≤ε ε) + ≤ real-ℚ⁺ (δ +ℚ⁺ ε) + by leq-eq-ℝ (add-real-ℚ _ _) + apart-w ε = + apart-located-metric-space-apart-Normed-ℝ-Vector-Space + ( V) + ( w ε) + ( v) + ( inv-tr + ( is-positive-ℝ) + ( |wε-v|=ε ε) + ( is-positive-real-ℝ⁺ (positive-raise-real-ℚ⁺ l1 ε))) + is-limit-w-v δ ε = + transitive-leq-ℝ _ _ _ + ( preserves-leq-real-ℚ + ( leq-right-add-rational-ℚ⁺ (rational-ℚ⁺ δ) ε)) + ( |wε-v|≤ε δ) + in + ( ( ( λ ε → (w ε , raise-star)) , + is-cauchy-w) , + apart-w , + is-limit-w-v)) + ( contains-unit-is-nontrivial-Normed-ℝ-Vector-Space V NT) +``` + +### If a normed real vector space is perfect, it is nontrivial + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + is-nontrivial-is-perfect-Normed-ℝ-Vector-Space : + is-perfect-Located-Metric-Space + ( located-metric-space-Normed-ℝ-Vector-Space V) → + is-nontrivial-Normed-ℝ-Vector-Space V + is-nontrivial-is-perfect-Normed-ℝ-Vector-Space P = + let open do-syntax-trunc-Prop (is-nontrivial-prop-Normed-ℝ-Vector-Space V) + in do + ((approx-0 , _) , apart-approx-0 , _) ← P (zero-Normed-ℝ-Vector-Space V) + let (v , _) = approx-0 one-ℚ⁺ + intro-exists + ( v) + ( is-nonzero-is-apart-zero-Normed-ℝ-Vector-Space V + ( v) + ( apart-apart-located-metric-space-Normed-ℝ-Vector-Space + ( V) + ( v) + ( zero-Normed-ℝ-Vector-Space V) + ( apart-approx-0 one-ℚ⁺))) +``` diff --git a/src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md b/src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md new file mode 100644 index 00000000000..e2eb1222c0b --- /dev/null +++ b/src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md @@ -0,0 +1,170 @@ +# Nonzero vectors of normed real vector spaces + +```agda +module linear-algebra.nonzero-vectors-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.negation +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import linear-algebra.apartness-normed-real-vector-spaces +open import linear-algebra.normed-real-vector-spaces +open import linear-algebra.unit-vectors-normed-real-vector-spaces + +open import real-numbers.multiplicative-inverses-positive-real-numbers +open import real-numbers.nonnegative-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.similarity-real-numbers +``` + +
+ +## Idea + +A +{{#concept "nonzero element" Disambiguation="of a normed real vector space" Agda=nonzero-type-Normed-ℝ-Vector-Space}} +of a [normed real vector space](linear-algebra.normed-real-vector-spaces.md) is +a vector with [positive](real-numbers.positive-real-numbers.md) norm. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + is-nonzero-prop-Normed-ℝ-Vector-Space : + subtype l1 (type-Normed-ℝ-Vector-Space V) + is-nonzero-prop-Normed-ℝ-Vector-Space v = + is-positive-prop-ℝ (map-norm-Normed-ℝ-Vector-Space V v) + + is-nonzero-Normed-ℝ-Vector-Space : + type-Normed-ℝ-Vector-Space V → UU l1 + is-nonzero-Normed-ℝ-Vector-Space = + is-in-subtype is-nonzero-prop-Normed-ℝ-Vector-Space + + nonzero-vector-Normed-ℝ-Vector-Space : UU (l1 ⊔ l2) + nonzero-vector-Normed-ℝ-Vector-Space = + type-subtype is-nonzero-prop-Normed-ℝ-Vector-Space +``` + +## Properties + +### A vector is not nonzero if and only if it is zero + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (v : type-Normed-ℝ-Vector-Space V) + where abstract + + is-zero-is-not-nonzero-Normed-ℝ-Vector-Space : + ¬ is-nonzero-Normed-ℝ-Vector-Space V v → + is-zero-Normed-ℝ-Vector-Space V v + is-zero-is-not-nonzero-Normed-ℝ-Vector-Space ¬|v|>0 = + is-extensional-norm-Normed-ℝ-Vector-Space V + ( v) + ( is-zero-is-nonnegative-is-nonpositive-ℝ + ( is-nonpositive-is-not-positive-ℝ ¬|v|>0) + ( is-nonnegative-map-norm-Normed-ℝ-Vector-Space V v)) + + is-not-nonzero-is-zero-Normed-ℝ-Vector-Space : + is-zero-Normed-ℝ-Vector-Space V v → + ¬ is-nonzero-Normed-ℝ-Vector-Space V v + is-not-nonzero-is-zero-Normed-ℝ-Vector-Space refl = + is-not-positive-is-zero-ℝ + ( _) + ( is-zero-map-norm-zero-Normed-ℝ-Vector-Space V) +``` + +### Normalization of a nonzero vector to a unit vector + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ((v , |v|>0) : nonzero-vector-Normed-ℝ-Vector-Space V) + (let |v|⁺ = (map-norm-Normed-ℝ-Vector-Space V v , |v|>0)) + where + + type-unit-nonzero-vector-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space V + type-unit-nonzero-vector-Normed-ℝ-Vector-Space = + mul-Normed-ℝ-Vector-Space V (real-inv-ℝ⁺ |v|⁺) v + + abstract + is-unit-type-unit-nonzero-vector-Normed-ℝ-Vector-Space : + is-unit-Normed-ℝ-Vector-Space V + ( type-unit-nonzero-vector-Normed-ℝ-Vector-Space) + is-unit-type-unit-nonzero-vector-Normed-ℝ-Vector-Space = + inv-tr + ( λ n → sim-ℝ n one-ℝ) + ( map-norm-mul-positive-Normed-ℝ-Vector-Space V (inv-ℝ⁺ |v|⁺) v) + ( left-inverse-law-mul-ℝ⁺ |v|⁺) + + unit-nonzero-vector-Normed-ℝ-Vector-Space : unit-Normed-ℝ-Vector-Space V + unit-nonzero-vector-Normed-ℝ-Vector-Space = + ( type-unit-nonzero-vector-Normed-ℝ-Vector-Space , + is-unit-type-unit-nonzero-vector-Normed-ℝ-Vector-Space) +``` + +### Normalization of a nonzero vector to a target nonnegative norm + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (c : ℝ⁰⁺ l1) + (v : nonzero-vector-Normed-ℝ-Vector-Space V) + (let (v̂ , |v̂|=1) = unit-nonzero-vector-Normed-ℝ-Vector-Space V v) + where + + normalized-to-norm-nonzero-vector-Normed-ℝ-Vector-Space : + type-Normed-ℝ-Vector-Space V + normalized-to-norm-nonzero-vector-Normed-ℝ-Vector-Space = + mul-Normed-ℝ-Vector-Space V (real-ℝ⁰⁺ c) v̂ + + abstract + has-norm-normalized-to-norm-nonzero-vector-Normed-ℝ-Vector-Space : + has-norm-Normed-ℝ-Vector-Space V + ( c) + ( normalized-to-norm-nonzero-vector-Normed-ℝ-Vector-Space) + has-norm-normalized-to-norm-nonzero-vector-Normed-ℝ-Vector-Space = + map-norm-mul-nonnegative-unit-Normed-ℝ-Vector-Space V c (v̂ , |v̂|=1) +``` + +### A vector is nonzero if and only if it is apart from zero + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (v : type-Normed-ℝ-Vector-Space V) + where abstract + + is-apart-zero-is-nonzero-Normed-ℝ-Vector-Space : + is-nonzero-Normed-ℝ-Vector-Space V v → + apart-Normed-ℝ-Vector-Space V v (zero-Normed-ℝ-Vector-Space V) + is-apart-zero-is-nonzero-Normed-ℝ-Vector-Space = + inv-tr + ( is-positive-ℝ) + ( right-zero-law-dist-Normed-ℝ-Vector-Space V v) + + is-nonzero-is-apart-zero-Normed-ℝ-Vector-Space : + apart-Normed-ℝ-Vector-Space V v (zero-Normed-ℝ-Vector-Space V) → + is-nonzero-Normed-ℝ-Vector-Space V v + is-nonzero-is-apart-zero-Normed-ℝ-Vector-Space = + tr + ( is-positive-ℝ) + ( right-zero-law-dist-Normed-ℝ-Vector-Space V v) +``` diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md index 531d6189c3c..5796b7e1e8f 100644 --- a/src/linear-algebra/normed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md @@ -9,7 +9,10 @@ module linear-algebra.normed-real-vector-spaces where
Imports ```agda +open import elementary-number-theory.positive-rational-numbers + open import foundation.action-on-identifications-functions +open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.dependent-products-propositions open import foundation.identity-types @@ -31,6 +34,7 @@ open import metric-spaces.located-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.metrics open import metric-spaces.metrics-of-metric-spaces +open import metric-spaces.rational-neighborhood-relations open import real-numbers.absolute-value-real-numbers open import real-numbers.addition-real-numbers @@ -38,7 +42,10 @@ open import real-numbers.dedekind-real-numbers open import real-numbers.distance-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.metric-space-of-real-numbers +open import real-numbers.multiplication-real-numbers open import real-numbers.nonnegative-real-numbers +open import real-numbers.positive-and-negative-real-numbers +open import real-numbers.positive-real-numbers open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.saturation-inequality-nonnegative-real-numbers @@ -180,6 +187,12 @@ module _ zero-Normed-ℝ-Vector-Space = zero-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space + right-zero-law-diff-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space) → + diff-Normed-ℝ-Vector-Space v zero-Normed-ℝ-Vector-Space ＝ v + right-zero-law-diff-Normed-ℝ-Vector-Space = + right-unit-law-right-subtraction-Ab ab-Normed-ℝ-Vector-Space + left-unit-law-add-Normed-ℝ-Vector-Space : (v : type-Normed-ℝ-Vector-Space) → add-Normed-ℝ-Vector-Space zero-Normed-ℝ-Vector-Space v ＝ v @@ -192,6 +205,21 @@ module _ right-inverse-law-add-Normed-ℝ-Vector-Space = right-inverse-law-add-Ab ab-Normed-ℝ-Vector-Space + is-zero-prop-Normed-ℝ-Vector-Space : subtype l2 type-Normed-ℝ-Vector-Space + is-zero-prop-Normed-ℝ-Vector-Space = + is-zero-prop-ℝ-Vector-Space + ( vector-space-Normed-ℝ-Vector-Space) + + is-zero-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → UU l2 + is-zero-Normed-ℝ-Vector-Space = + is-zero-ℝ-Vector-Space + ( vector-space-Normed-ℝ-Vector-Space) + + mul-Normed-ℝ-Vector-Space : + ℝ l1 → type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space + mul-Normed-ℝ-Vector-Space = + mul-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space + map-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → ℝ l1 map-norm-Normed-ℝ-Vector-Space = pr1 (pr1 norm-Normed-ℝ-Vector-Space) @@ -200,6 +228,33 @@ module _ nonnegative-seminorm-Seminormed-ℝ-Vector-Space ( seminormed-vector-space-Normed-ℝ-Vector-Space) + is-nonnegative-map-norm-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space) → + is-nonnegative-ℝ (map-norm-Normed-ℝ-Vector-Space v) + is-nonnegative-map-norm-Normed-ℝ-Vector-Space v = + is-nonnegative-real-ℝ⁰⁺ (nonnegative-norm-Normed-ℝ-Vector-Space v) + + is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space : + (c : ℝ l1) (v : type-Normed-ℝ-Vector-Space) → + map-norm-Normed-ℝ-Vector-Space (mul-Normed-ℝ-Vector-Space c v) ＝ + abs-ℝ c *ℝ map-norm-Normed-ℝ-Vector-Space v + is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space = + is-absolutely-homogeneous-seminorm-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space) + + has-norm-prop-Normed-ℝ-Vector-Space : + ℝ⁰⁺ l1 → subtype (lsuc l1) type-Normed-ℝ-Vector-Space + has-norm-prop-Normed-ℝ-Vector-Space d v = + Id-Prop + ( ℝ-Set l1) + ( map-norm-Normed-ℝ-Vector-Space v) + ( real-ℝ⁰⁺ d) + + has-norm-Normed-ℝ-Vector-Space : + ℝ⁰⁺ l1 → type-Normed-ℝ-Vector-Space → UU (lsuc l1) + has-norm-Normed-ℝ-Vector-Space d = + is-in-subtype (has-norm-prop-Normed-ℝ-Vector-Space d) + dist-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → ℝ l1 dist-Normed-ℝ-Vector-Space = @@ -302,6 +357,16 @@ module _ located-metric-space-Metric ( set-Normed-ℝ-Vector-Space V) ( metric-Normed-ℝ-Vector-Space) + + neighborhood-prop-Normed-ℝ-Vector-Space : + Rational-Neighborhood-Relation l1 (type-Normed-ℝ-Vector-Space V) + neighborhood-prop-Normed-ℝ-Vector-Space = + neighborhood-prop-Metric-Space metric-space-Normed-ℝ-Vector-Space + + neighborhood-Normed-ℝ-Metric-Space : + ℚ⁺ → Relation l1 (type-Normed-ℝ-Vector-Space V) + neighborhood-Normed-ℝ-Metric-Space = + neighborhood-Metric-Space metric-space-Normed-ℝ-Vector-Space ``` ## Properties @@ -417,15 +482,91 @@ module _ module _ {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) - where + where abstract + + eq-zero-norm-zero-Normed-ℝ-Vector-Space : + map-norm-Normed-ℝ-Vector-Space V (zero-Normed-ℝ-Vector-Space V) ＝ + raise-ℝ l1 zero-ℝ + eq-zero-norm-zero-Normed-ℝ-Vector-Space = + eq-zero-seminorm-zero-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + + is-zero-map-norm-zero-Normed-ℝ-Vector-Space : + is-zero-ℝ (map-norm-Normed-ℝ-Vector-Space V (zero-Normed-ℝ-Vector-Space V)) + is-zero-map-norm-zero-Normed-ℝ-Vector-Space = + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) +``` - abstract - eq-zero-norm-zero-Normed-ℝ-Vector-Space : - map-norm-Normed-ℝ-Vector-Space V (zero-Normed-ℝ-Vector-Space V) ＝ - raise-ℝ l1 zero-ℝ - eq-zero-norm-zero-Normed-ℝ-Vector-Space = - eq-zero-seminorm-zero-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space V) +### If `c` is nonnegative, `|cv| = c|v|` + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + map-norm-mul-nonnegative-Normed-ℝ-Vector-Space : + (c : ℝ⁰⁺ l1) (v : type-Normed-ℝ-Vector-Space V) → + map-norm-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space V (real-ℝ⁰⁺ c) v) ＝ + real-ℝ⁰⁺ c *ℝ map-norm-Normed-ℝ-Vector-Space V v + map-norm-mul-nonnegative-Normed-ℝ-Vector-Space c v = + ( is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space V (real-ℝ⁰⁺ c) v) ∙ + ( ap-mul-ℝ (abs-real-ℝ⁰⁺ c) refl) + + map-norm-mul-positive-Normed-ℝ-Vector-Space : + (c : ℝ⁺ l1) (v : type-Normed-ℝ-Vector-Space V) → + map-norm-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space V (real-ℝ⁺ c) v) ＝ + real-ℝ⁺ c *ℝ map-norm-Normed-ℝ-Vector-Space V v + map-norm-mul-positive-Normed-ℝ-Vector-Space c = + map-norm-mul-nonnegative-Normed-ℝ-Vector-Space + ( nonnegative-ℝ⁺ c) +``` + +### The distance between `v + w` and `v` is `|w|` + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + dist-add-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space V) → + dist-Normed-ℝ-Vector-Space V (add-Normed-ℝ-Vector-Space V v w) v ＝ + map-norm-Normed-ℝ-Vector-Space V w + dist-add-Normed-ℝ-Vector-Space v w = + ap + ( map-norm-Normed-ℝ-Vector-Space V) + ( is-identity-left-conjugation-Ab (ab-Normed-ℝ-Vector-Space V) v w) + + dist-add-Normed-ℝ-Vector-Space' : + (v w : type-Normed-ℝ-Vector-Space V) → + dist-Normed-ℝ-Vector-Space V v (add-Normed-ℝ-Vector-Space V v w) ＝ + map-norm-Normed-ℝ-Vector-Space V w + dist-add-Normed-ℝ-Vector-Space' v w = + ( symmetric-dist-Normed-ℝ-Vector-Space V _ _) ∙ + ( dist-add-Normed-ℝ-Vector-Space v w) +``` + +### Zero laws of distance + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (v : type-Normed-ℝ-Vector-Space V) + where abstract + + right-zero-law-dist-Normed-ℝ-Vector-Space : + dist-Normed-ℝ-Vector-Space V v (zero-Normed-ℝ-Vector-Space V) ＝ + map-norm-Normed-ℝ-Vector-Space V v + right-zero-law-dist-Normed-ℝ-Vector-Space = + ap + ( map-norm-Normed-ℝ-Vector-Space V) + ( right-zero-law-diff-Normed-ℝ-Vector-Space V v) ``` ## See also diff --git a/src/linear-algebra/seminormed-real-vector-spaces.lagda.md b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md index 065ed1fba7f..e804355162b 100644 --- a/src/linear-algebra/seminormed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md @@ -323,6 +323,17 @@ module _ ＝ raise-zero-ℝ l1 by left-raise-zero-law-mul-ℝ _ + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space : + is-zero-ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V)) + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space = + inv-tr + ( is-zero-ℝ) + ( eq-zero-seminorm-zero-Seminormed-ℝ-Vector-Space) + ( is-zero-raise-zero-ℝ l1) + eq-zero-diagonal-dist-Seminormed-ℝ-Vector-Space : (v : type-Seminormed-ℝ-Vector-Space V) → dist-Seminormed-ℝ-Vector-Space V v v ＝ raise-ℝ l1 zero-ℝ diff --git a/src/linear-algebra/trivial-real-vector-spaces.lagda.md b/src/linear-algebra/trivial-real-vector-spaces.lagda.md new file mode 100644 index 00000000000..58683fa2774 --- /dev/null +++ b/src/linear-algebra/trivial-real-vector-spaces.lagda.md @@ -0,0 +1,62 @@ +# Trivial real vector spaces + +```agda +module linear-algebra.trivial-real-vector-spaces where +``` + +
Imports + +```agda +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import linear-algebra.real-vector-spaces +open import linear-algebra.trivial-left-modules-rings + +open import real-numbers.large-ring-of-real-numbers +``` + +
+ +## Idea + +The +{{#concept "trivial vector space" Disambiguation="over ℝ" Agda=trivial-ℝ-Vector-Space}} +over the [real numbers](real-numbers.dedekind-real-numbers.md) is the +[real vector space](linear-algebra.real-vector-spaces.md) consisting of exactly +one element, `0`. + +## Properties + +### The property of being a trivial vector space + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Vector-Space l1 l2) + where + + is-trivial-prop-ℝ-Vector-Space : Prop l2 + is-trivial-prop-ℝ-Vector-Space = + is-trivial-prop-left-module-Ring (ring-ℝ l1) V + + is-trivial-ℝ-Vector-Space : UU l2 + is-trivial-ℝ-Vector-Space = type-Prop is-trivial-prop-ℝ-Vector-Space +``` + +### The trivial real vector space + +```agda +module _ + (l : Level) + where + + trivial-ℝ-Vector-Space : ℝ-Vector-Space l lzero + trivial-ℝ-Vector-Space = trivial-left-module-Ring (ring-ℝ l) + + is-trivial-trivial-ℝ-Vector-Space : + is-trivial-ℝ-Vector-Space trivial-ℝ-Vector-Space + is-trivial-trivial-ℝ-Vector-Space = + is-trivial-trivial-left-module-Ring (ring-ℝ l) +``` diff --git a/src/linear-algebra/unit-vectors-normed-real-vector-spaces.lagda.md b/src/linear-algebra/unit-vectors-normed-real-vector-spaces.lagda.md new file mode 100644 index 00000000000..d1efc7217e5 --- /dev/null +++ b/src/linear-algebra/unit-vectors-normed-real-vector-spaces.lagda.md @@ -0,0 +1,121 @@ +# Unit vectors in normed real vector spaces + +```agda +module linear-algebra.unit-vectors-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.large-monoids + +open import linear-algebra.normed-real-vector-spaces + +open import real-numbers.absolute-value-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.large-multiplicative-monoid-of-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.nonnegative-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.similarity-real-numbers +``` + +
+ +## Idea + +A +{{#concept "unit vector" WDID=Q36255 WD="unit vector" Agda=unit-Normed-ℝ-Vector-Space}} +in a [normed real vector space](linear-algebra.normed-real-vector-spaces.md) `V` +is a vector `v : V` with norm [similar](real-numbers.similarity-real-numbers.md) +to [one](real-numbers.rational-real-numbers.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + is-unit-prop-Normed-ℝ-Vector-Space : + subtype l1 (type-Normed-ℝ-Vector-Space V) + is-unit-prop-Normed-ℝ-Vector-Space v = + sim-prop-ℝ (map-norm-Normed-ℝ-Vector-Space V v) one-ℝ + + is-unit-Normed-ℝ-Vector-Space : + type-Normed-ℝ-Vector-Space V → UU l1 + is-unit-Normed-ℝ-Vector-Space = + is-in-subtype is-unit-prop-Normed-ℝ-Vector-Space + + unit-Normed-ℝ-Vector-Space : UU (l1 ⊔ l2) + unit-Normed-ℝ-Vector-Space = + type-subtype is-unit-prop-Normed-ℝ-Vector-Space + + type-unit-Normed-ℝ-Vector-Space : + unit-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space V + type-unit-Normed-ℝ-Vector-Space = + inclusion-subtype is-unit-prop-Normed-ℝ-Vector-Space +``` + +## Properties + +### Multiplying a unit vector by a scalar `c` produces a vector with norm `|c|` + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + map-norm-mul-unit-Normed-ℝ-Vector-Space : + (c : ℝ l1) (v : unit-Normed-ℝ-Vector-Space V) → + has-norm-Normed-ℝ-Vector-Space V + ( nonnegative-abs-ℝ c) + ( mul-Normed-ℝ-Vector-Space V c (type-unit-Normed-ℝ-Vector-Space V v)) + map-norm-mul-unit-Normed-ℝ-Vector-Space c (v , |v|~1) = + equational-reasoning + map-norm-Normed-ℝ-Vector-Space V (mul-Normed-ℝ-Vector-Space V c v) + ＝ abs-ℝ c *ℝ map-norm-Normed-ℝ-Vector-Space V v + by is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space V c v + ＝ abs-ℝ c + by + eq-sim-ℝ + ( sim-right-is-unit-law-mul-Large-Monoid + ( large-monoid-mul-ℝ) + ( abs-ℝ c) + ( map-norm-Normed-ℝ-Vector-Space V v) + ( |v|~1)) + + map-norm-mul-nonnegative-unit-Normed-ℝ-Vector-Space : + (c : ℝ⁰⁺ l1) (v : unit-Normed-ℝ-Vector-Space V) → + has-norm-Normed-ℝ-Vector-Space V + ( c) + ( mul-Normed-ℝ-Vector-Space V + ( real-ℝ⁰⁺ c) + ( type-unit-Normed-ℝ-Vector-Space V v)) + map-norm-mul-nonnegative-unit-Normed-ℝ-Vector-Space c v = + ( map-norm-mul-unit-Normed-ℝ-Vector-Space (real-ℝ⁰⁺ c) v) ∙ + ( abs-real-ℝ⁰⁺ c) + + map-norm-mul-positive-unit-Normed-ℝ-Vector-Space : + (c : ℝ⁺ l1) (v : unit-Normed-ℝ-Vector-Space V) → + has-norm-Normed-ℝ-Vector-Space V + ( nonnegative-ℝ⁺ c) + ( mul-Normed-ℝ-Vector-Space V + ( real-ℝ⁺ c) + ( type-unit-Normed-ℝ-Vector-Space V v)) + map-norm-mul-positive-unit-Normed-ℝ-Vector-Space c = + map-norm-mul-nonnegative-unit-Normed-ℝ-Vector-Space (nonnegative-ℝ⁺ c) +``` + +## External links + +- [Unit vector](https://en.wikipedia.org/wiki/Unit_vector) on Wikipedia diff --git a/src/metric-spaces/perfect-metric-spaces.lagda.md b/src/metric-spaces/perfect-metric-spaces.lagda.md index fa27df14cf7..565640c76a8 100644 --- a/src/metric-spaces/perfect-metric-spaces.lagda.md +++ b/src/metric-spaces/perfect-metric-spaces.lagda.md @@ -20,6 +20,11 @@ open import metric-spaces.located-metric-spaces ## Idea +A [located metric space](metric-spaces.located-metric-spaces.md) is +{{#concept "perfect" Disambiguation="located metric space" Agda=is-perfect-Located-Metric-Space}} +if every one of its points is an +[accumulation point](metric-spaces.accumulation-points-subsets-located-metric-spaces.md). + ## Definition ```agda @@ -40,3 +45,7 @@ Perfect-Metric-Space : (l1 l2 : Level) → UU (lsuc (l1 ⊔ l2)) Perfect-Metric-Space l1 l2 = type-subtype (is-perfect-prop-Located-Metric-Space {l1} {l2}) ``` + +## External links + +- [Perfect set](https://en.wikipedia.org/wiki/Perfect_set) on Wikipedia diff --git a/src/real-numbers/large-ring-of-real-numbers.lagda.md b/src/real-numbers/large-ring-of-real-numbers.lagda.md index d1d3b2b5eef..69a7cb817f7 100644 --- a/src/real-numbers/large-ring-of-real-numbers.lagda.md +++ b/src/real-numbers/large-ring-of-real-numbers.lagda.md @@ -25,6 +25,7 @@ open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers open import ring-theory.large-rings +open import ring-theory.rings ```
@@ -64,6 +65,9 @@ large-commutative-ring-ℝ = ### The small commutative ring of real numbers at a universe level ```agda +ring-ℝ : (l : Level) → Ring (lsuc l) +ring-ℝ = ring-Large-Ring large-ring-ℝ + commutative-ring-ℝ : (l : Level) → Commutative-Ring (lsuc l) commutative-ring-ℝ = commutative-ring-Large-Commutative-Ring large-commutative-ring-ℝ 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 e02e5c5fa0b..ebed3789934 100644 --- a/src/real-numbers/positive-and-negative-real-numbers.lagda.md +++ b/src/real-numbers/positive-and-negative-real-numbers.lagda.md @@ -25,6 +25,7 @@ open import real-numbers.nonpositive-real-numbers open import real-numbers.positive-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.strict-inequality-real-numbers +open import real-numbers.zero-real-numbers ``` @@ -185,3 +186,23 @@ abstract {l : Level} {x : ℝ l} → ¬ (is-negative-ℝ x × is-positive-ℝ x) is-not-negative-and-positive-ℝ (x<0 , 0 Date: Sun, 7 Jun 2026 15:59:46 -0700 Subject: [PATCH 6/6] Fix concept link --- .../nonzero-vectors-normed-real-vector-spaces.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md b/src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md index e2eb1222c0b..e8f20788844 100644 --- a/src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/nonzero-vectors-normed-real-vector-spaces.lagda.md @@ -31,7 +31,7 @@ open import real-numbers.similarity-real-numbers ## Idea A -{{#concept "nonzero element" Disambiguation="of a normed real vector space" Agda=nonzero-type-Normed-ℝ-Vector-Space}} +{{#concept "nonzero element" Disambiguation="of a normed real vector space" Agda=nonzero-vector-Normed-ℝ-Vector-Space}} of a [normed real vector space](linear-algebra.normed-real-vector-spaces.md) is a vector with [positive](real-numbers.positive-real-numbers.md) norm.