Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Restructure cardinals, finiteness and homeomorphisms #45

Merged
merged 16 commits into from
Aug 18, 2024
Merged

Restructure cardinals, finiteness and homeomorphisms #45

merged 16 commits into from
Aug 18, 2024

Conversation

Columbus240
Copy link
Collaborator

@Columbus240 Columbus240 commented Sep 16, 2023 •
edited
Loading

This branch does:

  • Introduce a notion of inverse_map f g which holds for maps f : X → Y, g : Y → X if they are inverses of eachother.
  • Redefine invertible, homeomorphism, FiniteT and eq_cardinal in terms of inverse_map. This allows for more better reuse of statements.
  • Change the def. of topological_property to use homeomorphic instead of homeomorphism. This makes it easier to apply proofs of topological_property. Use Build_topological_property as boilerplate when proving something is a topological_property.
  • Change the order of imports, so that FiniteTypes includes Cardinals instead of the other way around. This way we can prove general statements about eq_cardinal and le_cardinal and then use them for Finite and FiniteT. Previously the proofs would've been duplicated.
  • Split the theory of eq_cardinal and le_cardinal into multiple files in the folder Cardinals. They are all exported in the file Cardinals.v

Left to do:

  • Adapt meta.yml and the README.md to reflect the new structure of the files.
  • Can Finite_as_lt_cardinal_ens and injective_finite_inverse_image be proven in a way such that they can be moved to Finite_sets? That is, without using FiniteT or nat_unbounded_impl_countably_infinite.

This big restructuring of the library comes from some Yak shaving.

  1. I wanted to characterize some spaces up to homeomorphism, so I wanted to have appropriate definitions of homeomorphism, homeomorphic and topological_property.
  2. I started by redefining homeomorphisms, noting that a property inverse_map would be useful in proofs about it.
  3. But then it makes sense to redefine invertible in terms of inverse_map, instead of doing its own thing with Inductive.
  4. This leads to many changes in proofs about FiniteT.
  5. By noting that bij_finite uses something like eq_cardinal, by redefining eq_cardinal to use invertible as well, we can extract the lemmas of eq_cardinal _ _ from FiniteTypes and state them separately.

@Columbus240 Columbus240 force-pushed the cardinals branch 2 times, most recently from 515c142 to 443e6fb Compare September 16, 2023 16:17
@Columbus240 Columbus240 marked this pull request as ready for review October 8, 2023 08:49
@Columbus240 Columbus240 force-pushed the cardinals branch 2 times, most recently from 7118d34 to 427ad66 Compare October 15, 2023 08:12
@Columbus240
Add a list of references to the README
eb0d943
@Columbus240
[B] Use explicit localities and change some
8ab12af 
Smaller changes:
- Reorders and reduces the imports in some files.
- In `_CoqProject`: re-enable the warnings about missing hint/instance
  localities
- Add hint/instance localities where they were missing. Use `#[export]`
  if possible.
- Changed some hint/instance localities to `#[export]`. This is a
  breaking change depending on the circumstances of the user code.
@Columbus240
Introduce a notion inverse_map
1610eaa 
Having this definition will simplify the redefinition of homeomorphism.
Using `inverse_map` in the def. of homeomorphism will make the proofs
more conceptual (fewer hypotheses to juggle around), but this will need
a lot of changes.

It would make sense to use `inverse_map` in the definition of
`invertible`, but there's a lot that would need to be changed. That's
why I postpone doing so.
@Columbus240
[B] Rework definition of homeo. and topo. prop.
36ac9fb 
Rework definition of `homeomorphism`, `homeomorphic` and
`topological_property`. First, use `Definition` and `exists` instead of
`Inductive`. Second, for `topological_property` require the spaces to be
`homeomorphic` instead of requiring a `homeomorphism` between them (using the
`Proper` typeclass).
The former facilitates proving these properties and the latter facilitates
using proofs of `topological_property`, since in practice one rarely wants to
know the explicit homeomorphism between two spaces if one only wants to
transfer a topological property.

Then use the typeclass `Equivalence` to state that `homeomorphic` is an
equivalence relation. This will simplify proofs.
@Columbus240
[B] Redefine eq_cardinal, invertible, FiniteT
4b7692e 
Use `inverse_map` throughout, instead of `bijective`. This makes it
easier to re-use lemmas.

Use `invertible` instead of `bijective` because it is a slightly
stronger property. In particular `FiniteT` behaves a bit better with
`invertible` than with `bijective`.

Move the definition of `eq_cardinal` from Cardinals to
FiniteTypes, because to do it the the other way around, some lemmas
would need to be moved.
@Columbus240
[B] Change order of Cardinals, Finite, Countable …
8373afa 
Moves the definition of `eq_cardinal` to Cardinals, where it belongs.
But to allow this, the statements `countable_img_inj` and
`FiniteT_cardinality` had to be moved to Countable and FiniteTypes
respectively. In addition, `CountableT_cardinality` was removed, because
`CountableT` could be redefined in terms of `le_cardinal`, making the
lemma even more trivial.

Also, removes the file InfiniteTypes, because it has become empty.

The lemmas `Finite_as_lt_cardinal_ens` and
`injective_finite_inverse_image` currently are in `FiniteTypes.v`,
because their proofs use `FiniteT` in essential ways.
@Columbus240
[B] Move Cardinals etc. into separate folder
9edf338 
The files concerning cardinalities (`eq_cardinal` and `le_cardinal`) in
general are rather large and would be easier to manage if they are split
into multiple files.
This also solves a "practical" problem: the statement of `CSB` could be
formulated using `eq_cardinal`. But this is not possible if the file
`Cardinals.v` depends on the file `CSB.v`.
Another possibility would be, that `CSB` is carefully stated, that it
uses definitions compatible with `Cardinals.v`. But this would break
`Search`, or we'd need to re-state `CSB` in terms of `eq_cardinal` and
`le_cardinal` in `Cardinals.v`.
@Columbus240
Add Cardinals.v, fixing previous commit
484bcad 
To make git happy, the file `ZornsLemma/Cardinals.v` is not included in
the previous commit. This way git can notice, that we moved
`ZornsLemma/Cardinals.v` to `ZornsLemma/Cardinals/Cardinals.v`. Thus
also `git blame` still works.
But the previous commit does not build.
@Columbus240
[B] Cardinals: Move Cantor diag. to separate file
b7e825c
@Columbus240
[B] Cardinals: Extract LeastCardinalsEns.v to file
f9a4c06
@Columbus240
[B] Cardinals: Extract le_cardinal_total to file
d27f586 
Removed the `types_comparable` in favor of `le_cardinal_total`, because
both proved the same thing.
@Columbus240
[B] Cardinals: Make CSB depend on Cardinals
a8c5778 
This moves everything deduced from `CSB` to `CSB.v`.

Also changes the statement of
`CountableT_is_FiniteT_or_countably_infinite` to be more fitting to the
rest of the theory.
@Columbus240
[B] Move nat_unbounded_… to CountableTypes.v
9065143 
The lemma says "unbounded subsets of ℕ are countably infinite", which
does not belong to the general discussion of cardinals.
It is a bit hard to sort this lemma into the existing files, but
CountableTypes.v seems to work best, because it already is concerned
with `nat`.

Also moves `Finite_as_lt_cardinal_ens` and
`injective_finite_inverse_image` to CountableTypes.v, because they
depend on `nat_unbounded_impl_countably_infinite`. This is not ideal.

A bit problematic is `nat_minimal_element_property_dec` and
`nat_minimal_element_property` which are not exactly proofs of
`Classical_Wf.minimal_element_property`. And they are self-contained,
not depending on any theory in CountableTypes.v.
@Columbus240
[B] Cardinals: Remove ge_cardinal and gt_cardinal
b99031b 
These notions are redundant. If they are used in lemmas, they make
it harder to `Search` for results.
@Columbus240
[B] Finite/Cardinals: Extract combinatorial lemmas
fbd613a 
They hold independently of the def. `FiniteT` and are thus better placed
in the Cardinals folder.
@Columbus240 Columbus240 merged commit f890bcf into master Aug 18, 2024
5 checks passed
@Columbus240 Columbus240 deleted the cardinals branch August 18, 2024 15:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@Columbus240