From 346e0c114821392d6de84bc7efc2ed52cf3d928a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 17 Oct 2024 18:05:54 +0200 Subject: [PATCH] 100 Theorems (#1201) Adds a page about our progress on [_Formalizing 100 Theorems_](https://www.cs.ru.nl/~freek/100/). --- HOWTO-INSTALL.md | 4 +- references.bib | 12 ++ .../integer-fractions.lagda.md | 23 +++- .../positive-integers.lagda.md | 20 ++++ .../rational-numbers.lagda.md | 30 ++++- ...cantor-schroder-bernstein-escardo.lagda.md | 18 ++- src/foundation/injective-maps.lagda.md | 6 + src/foundation/maybe.lagda.md | 61 ++++++++-- src/literature.lagda.md | 16 +-- src/literature/100-theorems.lagda.md | 104 ++++++++++++++++++ src/set-theory/countable-sets.lagda.md | 88 +++++++++++++++ 11 files changed, 360 insertions(+), 22 deletions(-) create mode 100644 src/literature/100-theorems.lagda.md diff --git a/HOWTO-INSTALL.md b/HOWTO-INSTALL.md index 546f092848..eb157e170d 100644 --- a/HOWTO-INSTALL.md +++ b/HOWTO-INSTALL.md @@ -303,7 +303,7 @@ below to ensure a smooth setup and workflow. Also, please make sure to follow our [coding style](CODINGSTYLE.md) and [design principles](DESIGN-PRINCIPLES.md). -### Pre-commit hooks and Python dependencies +### Pre-commit hooks and Python dependencies {#pre-commit-hooks} The agda-unimath library includes [pre-commit](https://pre-commit.com/) hooks that enforce [basic formatting rules](CONTRIBUTING.md). These will inform you of @@ -333,7 +333,7 @@ Keep in mind that `pre-commit` is also a part of the Continuous Integration (CI), so any PR that violates the enforced conventions will be automatically blocked from merging. -### Building and viewing the website locally +### Building and viewing the website locally {#build-website} The build process for the website uses the [Rust language](https://www.rust-lang.org/)'s package manager `cargo`. To diff --git a/references.bib b/references.bib index 8e6c24919d..4422049d7d 100644 --- a/references.bib +++ b/references.bib @@ -1,3 +1,15 @@ +@online{1000+theorems, + title = {1000+ theorems}, + author = {Freek Wiedijk}, + url = {https://1000-plus.github.io/} +} + +@online{100theorems, + title = {Formalizing 100 Theorems}, + author = {Freek Wiedijk}, + url = {https://www.cs.ru.nl/~freek/100/} +} + @article{AKS15, title = {Univalent Categories and the {{Rezk}} Completion}, author = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael}, diff --git a/src/elementary-number-theory/integer-fractions.lagda.md b/src/elementary-number-theory/integer-fractions.lagda.md index eacb3714e8..dea0da34e6 100644 --- a/src/elementary-number-theory/integer-fractions.lagda.md +++ b/src/elementary-number-theory/integer-fractions.lagda.md @@ -24,15 +24,17 @@ open import foundation.negation open import foundation.propositions open import foundation.sets open import foundation.universe-levels + +open import set-theory.countable-sets ``` ## Idea -The type of integer fractions is the type of pairs `n/m` consisting of an -integer `n` and a positive integer `m`. The type of rational numbers is a -retract of the type of fractions. +The type of {{#concept "integer fractions" Agda=fraction-ℤ}} is the type of +pairs `n/m` consisting of an integer `n` and a positive integer `m`. The type of +rational numbers is a retract of the type of fractions. ## Definitions @@ -122,6 +124,9 @@ abstract abstract is-set-fraction-ℤ : is-set fraction-ℤ is-set-fraction-ℤ = is-set-Σ is-set-ℤ (λ _ → is-set-positive-ℤ) + +fraction-ℤ-Set : Set lzero +fraction-ℤ-Set = fraction-ℤ , is-set-fraction-ℤ ``` ```agda @@ -260,3 +265,15 @@ abstract is-nonzero-is-positive-ℤ ( is-positive-gcd-numerator-denominator-fraction-ℤ x) ``` + +### The set of integer fractions is countable + +```agda +is-countable-fraction-ℤ : is-countable fraction-ℤ-Set +is-countable-fraction-ℤ = + is-countable-product + ( ℤ-Set) + ( positive-ℤ-Set) + ( is-countable-ℤ) + ( is-countable-positive-ℤ) +``` diff --git a/src/elementary-number-theory/positive-integers.lagda.md b/src/elementary-number-theory/positive-integers.lagda.md index 5b25d4a0e2..5ac772e16d 100644 --- a/src/elementary-number-theory/positive-integers.lagda.md +++ b/src/elementary-number-theory/positive-integers.lagda.md @@ -18,6 +18,7 @@ open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equivalences +open import foundation.existential-quantification open import foundation.function-types open import foundation.identity-types open import foundation.propositions @@ -25,9 +26,12 @@ open import foundation.retractions open import foundation.sections open import foundation.sets open import foundation.subtypes +open import foundation.surjective-maps open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels + +open import set-theory.countable-sets ``` @@ -122,6 +126,9 @@ is-nonzero-is-positive-ℤ {inr (inr x)} H () is-set-positive-ℤ : is-set positive-ℤ is-set-positive-ℤ = is-set-type-subtype subtype-positive-ℤ is-set-ℤ + +positive-ℤ-Set : Set lzero +positive-ℤ-Set = positive-ℤ , is-set-positive-ℤ ``` ### The successor of a positive integer is positive @@ -182,6 +189,19 @@ pr1 equiv-positive-int-ℕ = positive-int-ℕ pr2 equiv-positive-int-ℕ = is-equiv-positive-int-ℕ ``` +### The set of positive integers is countable + +```agda +is-countable-positive-ℤ : is-countable positive-ℤ-Set +is-countable-positive-ℤ = + is-countable-is-directly-countable + ( positive-ℤ-Set) + ( one-positive-ℤ) + ( intro-exists + ( positive-int-ℕ) + ( is-surjective-is-equiv is-equiv-positive-int-ℕ)) +``` + ## See also - The relations between positive and nonnegative, negative and nonnpositive diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index 0e730f26eb..d10100c71a 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/src/elementary-number-theory/rational-numbers.lagda.md @@ -25,9 +25,14 @@ open import foundation.identity-types open import foundation.negation open import foundation.propositions open import foundation.reflecting-maps-equivalence-relations +open import foundation.retracts-of-types +open import foundation.sections open import foundation.sets open import foundation.subtypes +open import foundation.surjective-maps open import foundation.universe-levels + +open import set-theory.countable-sets ``` @@ -157,11 +162,15 @@ abstract ℚ-Set : Set lzero pr1 ℚ-Set = ℚ pr2 ℚ-Set = is-set-ℚ +``` + +### The rationals are a retract of the integer fractions +```agda abstract is-retraction-rational-fraction-ℚ : (x : ℚ) → rational-fraction-ℤ (fraction-ℚ x) ＝ x - is-retraction-rational-fraction-ℚ (pair (pair m (pair n n-pos)) p) = + is-retraction-rational-fraction-ℚ ((m , n , n-pos) , p) = eq-pair-Σ ( eq-pair ( eq-quotient-div-is-one-ℤ _ _ p (div-left-gcd-ℤ m n)) @@ -169,6 +178,25 @@ abstract ( eq-quotient-div-is-one-ℤ _ _ p (div-right-gcd-ℤ m n)) ( eq-is-prop (is-prop-is-positive-ℤ n)))) ( eq-is-prop (is-prop-is-reduced-fraction-ℤ (m , n , n-pos))) + +section-rational-fraction-ℤ : section rational-fraction-ℤ +section-rational-fraction-ℤ = (fraction-ℚ , is-retraction-rational-fraction-ℚ) + +retract-integer-fraction-ℚ : ℚ retract-of fraction-ℤ +retract-integer-fraction-ℚ = + ( fraction-ℚ , rational-fraction-ℤ , is-retraction-rational-fraction-ℚ) +``` + +### The rationals are countable + +```agda +is-countable-ℚ : is-countable ℚ-Set +is-countable-ℚ = + is-countable-retract-of + ( fraction-ℤ-Set) + ( ℚ-Set) + ( retract-integer-fraction-ℚ) + ( is-countable-fraction-ℤ) ``` ### Two fractions with the same numerator and same denominator are equal diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md index 70bdbea7f6..0b731f760f 100644 --- a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md +++ b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md @@ -10,6 +10,7 @@ module foundation.cantor-schroder-bernstein-escardo where open import foundation.action-on-identifications-functions open import foundation.decidable-types open import foundation.dependent-pair-types +open import foundation.injective-maps open import foundation.law-of-excluded-middle open import foundation.perfect-images open import foundation.split-surjective-maps @@ -21,8 +22,8 @@ open import foundation-core.empty-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.identity-types -open import foundation-core.injective-maps open import foundation-core.negation +open import foundation-core.sets ``` @@ -172,6 +173,21 @@ module _ is-equiv-map-Cantor-Schröder-Bernstein-Escardó f g ``` +## Corollaries + +### The Cantor–Schröder–Bernstein theorem + +```agda +Cantor-Schröder-Bernstein : + {l1 l2 : Level} (lem : LEM (l1 ⊔ l2)) + (A : Set l1) (B : Set l2) → + injection (type-Set A) (type-Set B) → + injection (type-Set B) (type-Set A) → + (type-Set A) ≃ (type-Set B) +Cantor-Schröder-Bernstein lem A B f g = + Cantor-Schröder-Bernstein-Escardó lem (emb-injection B f) (emb-injection A g) +``` + ## References - Escardó's formalizations regarding this theorem can be found at diff --git a/src/foundation/injective-maps.lagda.md b/src/foundation/injective-maps.lagda.md index 4b410f44c8..8114a8e0f3 100644 --- a/src/foundation/injective-maps.lagda.md +++ b/src/foundation/injective-maps.lagda.md @@ -15,6 +15,7 @@ open import foundation.universe-levels open import foundation-core.embeddings open import foundation-core.empty-types +open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.negation open import foundation-core.propositional-maps @@ -83,6 +84,11 @@ module _ {f : A → B} → is-set B → is-injective f → is-prop-map f is-prop-map-is-injective {f} H I = is-prop-map-is-emb (is-emb-is-injective H I) + +emb-injection : + {l1 l2 : Level} {A : UU l1} (B : Set l2) → + injection A (type-Set B) → A ↪ (type-Set B) +emb-injection B = tot (λ f → is-emb-is-injective (is-set-type-Set B)) ``` ### For a map between sets, being injective is a property diff --git a/src/foundation/maybe.lagda.md b/src/foundation/maybe.lagda.md index fea3515ce4..bd7e15b923 100644 --- a/src/foundation/maybe.lagda.md +++ b/src/foundation/maybe.lagda.md @@ -7,11 +7,13 @@ module foundation.maybe where
Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.coproduct-types open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.equality-coproduct-types +open import foundation.existential-quantification open import foundation.propositional-truncations open import foundation.surjective-maps open import foundation.type-arithmetic-empty-type @@ -49,6 +51,22 @@ not [idempotent](foundation.idempotent-maps.md). ```agda Maybe : {l : Level} → UU l → UU l Maybe X = X + unit + +unit-Maybe : {l : Level} {X : UU l} → X → Maybe X +unit-Maybe = inl + +exception-Maybe : {l : Level} {X : UU l} → Maybe X +exception-Maybe = inr star + +extend-Maybe : + {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (X → Maybe Y) → Maybe X → Maybe Y +extend-Maybe f (inl x) = f x +extend-Maybe f (inr *) = inr * + +map-Maybe : + {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (X → Y) → Maybe X → Maybe Y +map-Maybe f (inl x) = inl (f x) +map-Maybe f (inr *) = inr * ``` ### The inductive definition of the maybe monad @@ -59,12 +77,6 @@ data Maybe' {l : Level} (X : UU l) : UU l where exception-Maybe' : Maybe' X {-# BUILTIN MAYBE Maybe' #-} - -unit-Maybe : {l : Level} {X : UU l} → X → Maybe X -unit-Maybe = inl - -exception-Maybe : {l : Level} {X : UU l} → Maybe X -exception-Maybe {l} {X} = inr star ``` ### The predicate of being an exception @@ -148,7 +160,7 @@ abstract ```agda decide-Maybe : {l : Level} {X : UU l} (x : Maybe X) → is-value-Maybe x + is-exception-Maybe x -decide-Maybe (inl x) = inl (pair x refl) +decide-Maybe (inl x) = inl (x , refl) decide-Maybe (inr star) = inr refl ``` @@ -159,7 +171,7 @@ abstract is-not-exception-is-value-Maybe : {l1 : Level} {X : UU l1} (x : Maybe X) → is-value-Maybe x → is-not-exception-Maybe x - is-not-exception-is-value-Maybe {l1} {X} .(inl x) (pair x refl) = + is-not-exception-is-value-Maybe {l1} {X} .(inl x) (x , refl) = is-not-exception-unit-Maybe x ``` @@ -224,6 +236,39 @@ module _ equiv-Maybe-Maybe' = (map-Maybe-Maybe' , is-equiv-map-Maybe-Maybe') ``` +### The extension of surjective maps is surjective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-surjective-extend-is-surjective-Maybe : + {f : A → Maybe B} → is-surjective f → is-surjective (extend-Maybe f) + is-surjective-extend-is-surjective-Maybe {f} F y = + elim-exists + ( exists-structure-Prop (Maybe A) (λ z → extend-Maybe f z ＝ y)) + ( λ x p → intro-exists (inl x) p) + ( F y) +``` + +### The functorial action of `Maybe` preserves surjective maps + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-surjective-map-is-surjective-Maybe : + {f : A → B} → is-surjective f → is-surjective (map-Maybe f) + is-surjective-map-is-surjective-Maybe {f} F (inl y) = + elim-exists + ( exists-structure-Prop (Maybe A) (λ z → map-Maybe f z ＝ inl y)) + ( λ x p → intro-exists (inl x) (ap inl p)) + ( F y) + is-surjective-map-is-surjective-Maybe F (inr *) = intro-exists (inr *) refl +``` + ### There is a surjection from `Maybe A + Maybe B` to `Maybe (A + B)` ```agda diff --git a/src/literature.lagda.md b/src/literature.lagda.md index 2731009799..2127b478fa 100644 --- a/src/literature.lagda.md +++ b/src/literature.lagda.md @@ -1,18 +1,20 @@ # Formalization of results from the literature -> This page is a work in early progress. To see what's happening behind the -> scenes, you can have a look at the associated GitHub issue +> This page is currently under construction. To see what's happening behind the +> scenes, see the associated GitHub issue > [#1055](https://github.com/UniMath/agda-unimath/issues/1055). -## References - -{{#bibliography}} {{#reference SvDR20}} {{#reference Shu17}} - -## Files in the namespace +## Modules in the literature namespace ```agda module literature where +open import literature.100-theorems public open import literature.idempotents-in-intensional-type-theory public open import literature.sequential-colimits-in-homotopy-type-theory public ``` + +## References + +{{#bibliography}} {{#reference SvDR20}} {{#reference Shu17}} +{{#reference 100theorems}} diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md new file mode 100644 index 0000000000..7c4f1b1958 --- /dev/null +++ b/src/literature/100-theorems.lagda.md @@ -0,0 +1,104 @@ +# Formalizing 100 Theorems + +This file records formalized results from Freek Wiedijk's +[_Formalizing 100 Theorems_](https://www.cs.ru.nl/~freek/100/). +{{#cite 100theorems}} + +```agda +module literature.100-theorems where +``` + +## The list + +### [3. The Denumerability of the Rational Numbers](https://www.cs.ru.nl/~freek/100/#3) {#3} + +```agda +open import elementary-number-theory.rational-numbers using + ( is-countable-ℚ) +``` + +### [11. The Infinitude of Primes](https://www.cs.ru.nl/~freek/100/#11) {#11} + +```agda +open import elementary-number-theory.infinitude-of-primes using + ( infinitude-of-primes-ℕ) +``` + +### [22. The Non-Denumerability of the Continuum](https://www.cs.ru.nl/~freek/100/#22) {#22} + +> This is not yet formalized. + +### [25. Schröder–Bernstein Theorem](https://www.cs.ru.nl/~freek/100/#25) {#25} + +```agda +open import foundation.cantor-schroder-bernstein-escardo using + ( Cantor-Schröder-Bernstein) +``` + +### [44. The Binomial Theorem](https://www.cs.ru.nl/~freek/100/#44) {#44} + +```agda +open import commutative-algebra.binomial-theorem-commutative-semirings using + ( binomial-theorem-Commutative-Semiring) +open import ring-theory.binomial-theorem-rings using + ( binomial-theorem-Ring) +open import ring-theory.binomial-theorem-semirings using + ( binomial-theorem-Semiring) +open import elementary-number-theory.binomial-theorem-integers using + ( binomial-theorem-ℤ) +open import elementary-number-theory.binomial-theorem-natural-numbers using + ( binomial-theorem-ℕ) +``` + +### [52. The Number of Subsets of a Set](https://www.cs.ru.nl/~freek/100/#52) {#52} + +> This is not yet formalized. + +### [63. Cantor's Theorem](https://www.cs.ru.nl/~freek/100/#63) {#63} + +```agda +open import foundation.cantors-theorem using + ( theorem-Cantor) +``` + +### [69. Greatest Common Divisor Algorithm](https://www.cs.ru.nl/~freek/100/#69) {#69} + +```agda +open import + elementary-number-theory.greatest-common-divisor-natural-numbers using + ( GCD-ℕ) +``` + +### [74. The Principle of Mathematical Induction](https://www.cs.ru.nl/~freek/100/#74) {#74} + +```agda +open import elementary-number-theory.natural-numbers using + ( ind-ℕ) +``` + +### [80. The Fundamental Theorem of Arithmetic](https://www.cs.ru.nl/~freek/100/#80) {#80} + +```agda +open import elementary-number-theory.fundamental-theorem-of-arithmetic using + ( fundamental-theorem-arithmetic-list-ℕ) +``` + +### [91. The Triangle Inequality](https://www.cs.ru.nl/~freek/100/#91) {#91} + +```agda +open import real-numbers.metric-space-of-real-numbers using + ( is-triangular-premetric-leq-ℝ) +``` + +### [96. Principle of Inclusion/Exclusion](https://www.cs.ru.nl/~freek/100/#96) {#96} + +> This is not yet formalized. + +## References + +{{#bibliography}} + +## External links + +- The spiritual successor to _Formalizing 100 Theorems_ is + [_1000+ theorems_](https://1000-plus.github.io/), also due to Freek Wiedijk. diff --git a/src/set-theory/countable-sets.lagda.md b/src/set-theory/countable-sets.lagda.md index 80127b00c6..023911e269 100644 --- a/src/set-theory/countable-sets.lagda.md +++ b/src/set-theory/countable-sets.lagda.md @@ -20,6 +20,7 @@ open import foundation.decidable-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equality-coproduct-types +open import foundation.equivalences open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-cartesian-product-types @@ -30,6 +31,7 @@ open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions open import foundation.raising-universe-levels +open import foundation.retracts-of-types open import foundation.sets open import foundation.shifting-sequences open import foundation.surjective-maps @@ -291,6 +293,92 @@ module _ ( unit-trunc-Prop (enumeration-decidable-subprojection-ℕ D))) ``` +### If a countable set surjects onto a set, then the set is countable + +```agda +module _ + {l1 l2 : Level} (A : Set l1) (B : Set l2) + where + + is-directly-countable-is-directly-countably-indexed' : + {f : type-Set A → type-Set B} → is-surjective f → + is-directly-countable A → is-directly-countable B + is-directly-countable-is-directly-countably-indexed' {f} F = + elim-exists + ( is-directly-countable-Prop B) + ( λ g G → intro-exists (f ∘ g) (is-surjective-comp F G)) + + is-directly-countable-is-directly-countably-indexed : + (type-Set A ↠ type-Set B) → + is-directly-countable A → + is-directly-countable B + is-directly-countable-is-directly-countably-indexed (f , F) = + is-directly-countable-is-directly-countably-indexed' F + + is-countable-is-countably-indexed' : + {f : type-Set A → type-Set B} → + is-surjective f → + is-countable A → + is-countable B + is-countable-is-countably-indexed' {f} F = + elim-exists + ( is-countable-Prop B) + ( λ g G → + intro-exists + ( map-Maybe f ∘ g) + ( is-surjective-comp (is-surjective-map-is-surjective-Maybe F) G)) + + is-countable-is-countably-indexed : + (type-Set A ↠ type-Set B) → + is-countable A → + is-countable B + is-countable-is-countably-indexed (f , F) = + is-countable-is-countably-indexed' F +``` + +### Retracts of countable sets are countable + +```agda +module _ + {l1 l2 : Level} (A : Set l1) (B : Set l2) + (R : (type-Set B) retract-of (type-Set A)) + where + + is-directly-countable-retract-of : + is-directly-countable A → is-directly-countable B + is-directly-countable-retract-of = + is-directly-countable-is-directly-countably-indexed' A B + { map-retraction-retract R} + ( is-surjective-has-section + ( inclusion-retract R , is-retraction-map-retraction-retract R)) + + is-countable-retract-of : + is-countable A → is-countable B + is-countable-retract-of = + is-countable-is-countably-indexed' A B + { map-retraction-retract R} + ( is-surjective-has-section + ( inclusion-retract R , is-retraction-map-retraction-retract R)) +``` + +### Countable sets are closed under equivalences + +```agda +module _ + {l1 l2 : Level} (A : Set l1) (B : Set l2) (e : type-Set B ≃ type-Set A) + where + + is-directly-countable-equiv : + is-directly-countable A → is-directly-countable B + is-directly-countable-equiv = + is-directly-countable-retract-of A B (retract-equiv e) + + is-countable-equiv : + is-countable A → is-countable B + is-countable-equiv = + is-countable-retract-of A B (retract-equiv e) +``` + ### The set of natural numbers ℕ is itself countable ```agda