Shad Amethyst
ee3cdfe13b
:up_arrow: Upgrade mathlib
4 months ago
Shad Amethyst
253c33035d
🎉 Finished the proof of rubin's theorem
5 months ago
Shad Amethyst
8737257190
🎉 Construct the equivariant homeomorphism to the rubin space
5 months ago
Shad Amethyst
7d92d98b60
🎉 Finally reached the homeomorph stage!
...
All that remains is to define the conjugation action on RubinSpace,
and prove that the canonical homeomorph (lim/fromPoint) preserves that action.
The tools should be in place to prove most of this, and I don't have to deal with open sets ever again.
5 months ago
Shad Amethyst
7c5ce7e631
✨ Working equiv for RubinSpace
5 months ago
Shad Amethyst
6b2f21fec8
✨ Fix all sorries
5 months ago
Shad Amethyst
6a2f4960d7
✨ Construct ultrafilters in the topolical space and rubinfilters from one another
5 months ago
Shad Amethyst
5fb9162950
✨ Prove that UltrafilterInBasis is a sufficient condition for convergence
5 months ago
Shad Amethyst
431a2931d7
✨ Implement UltrafilterInBasis.map_basis
5 months ago
Shad Amethyst
e84ff177bd
✨ Start working on Filter.InBasis
5 months ago
Shad Amethyst
7b4307d76c
✨ Split apart the implications of theorem 3.5 to be able to use ultraprefilters
5 months ago
Shad Amethyst
ec9587c7e9
🔥 Draft out the end of the proof
...
There seems to be a lot of details still missing, especially around how to exactly define RubinFilter,
so that any RubinFilter maps to at least one value in α, while allowing me to create a new RubinFilter from
an Ultrafilter α.
5 months ago
Shad Amethyst
65e1ab7fc8
📝 Refactor RegularSupportBasis
5 months ago
Shad Amethyst
60111656b8
✨ Replace ContinuousMulAction with ContinuousConstSMul
5 months ago
Shad Amethyst
a87dc079d6
💩 Messy draft code to work towards the end of the proof
...
I need to change a bunch of things kind of everywhere and clean everything up before continuing
5 months ago
Shad Amethyst
50b4b49932
✨ Fully prove proposition 3.5
5 months ago
Shad Amethyst
24dd2c4f0a
🔥 New notation for RigidStabilizer and prove first lemma for proposition 3.5
5 months ago
Shad Amethyst
522f345f34
✨ Implement SMul on filters, prove compactness of smulImage and that orbit is a subset of support
5 months ago
Shad Amethyst
23d0821290
✨ Almost complete proof of proposition 3.5
5 months ago
Shad Amethyst
55d674e96a
✨ Implement RigidStabilizerBasis and AlgebraicCentralizerBasis
5 months ago
Shad Amethyst
5d81de14d4
🚚 Move RegularSupportBasis to its own file
5 months ago
Shad Amethyst
9e6258bf5c
🚚 Rename AssociatedPoset to RegularSupportBasis
5 months ago
Laurent Bartholdi
cfb341daeb
Added rubin
6 months ago
Shad Amethyst
52b5b5523b
📝 Add installation instructions and push to github
6 months ago
Shad Amethyst
7afc87d0f9
⬆️ Upgrade mathlib and lean version to latest
6 months ago
Shad Amethyst
69ad593f4b
✨ Prove proposition 3.2
6 months ago
Shad Amethyst
a09187c7fa
✨ Start proving proposition 3.2
6 months ago
Shad Amethyst
29fc8990a8
✨ Prove the two-way monotonicity of rigid stabilizers in group homeomorphisms
...
I knew this proof that group homeomorphisms are faithful would come in handy :3
6 months ago
Shad Amethyst
3b0b8a8a65
✨ Define group action from HomeoGroup to AssociatedPoset
6 months ago
Shad Amethyst
652e1a0773
🚚 Move a bunch of definitions around, making Topology importable from more files
6 months ago
Shad Amethyst
18912139ec
Rename smulImage_subset to smulImage_mono
6 months ago
Shad Amethyst
03cec8913a
✨ Start working on homeomorphic groups
6 months ago
Shad Amethyst
d5cd873cf6
✨ Implement remark 2.3
6 months ago
Shad Amethyst
7a8184548b
🚚 Move proofs of Rubin's theorem to Rubin.lean
6 months ago
Shad Amethyst
6ce7127efe
🎨 Small renames for consistency
6 months ago
Shad Amethyst
4b4a719d40
✨ Working proof of proposition 2.1
6 months ago
Shad Amethyst
fc12acb37b
✨ Implement most of proposition 2.1
6 months ago
Shad Amethyst
4d8a4d0f1a
✨ Transition over RegularSupport
6 months ago
Shad Amethyst
9df983f476
✨ Clean up algebraic disjointness
6 months ago
Shad Amethyst
43784b1210
✨ Translate and clean up up to remark 1.2
6 months ago
Shad Amethyst
cd9ad02e1d
✨ Prove disjoint_nbhd_fin
6 months ago
Shad Amethyst
d96318acc8
✨ Translate proposition 1.1.1 to lean4
6 months ago
Shad Amethyst
171caae2d3
✨ Move out toplogical actions and faithful actions
6 months ago
Shad Amethyst
adc7194774
🚚 Start moving more theorems in different files
6 months ago
Shad Amethyst
5fcca86b58
🚚 Move tactic to Rubin/Tactic.lean, wrap everything in a namespace
6 months ago
Shad Amethyst
049434fcd8
✨ Implement the group_action tactic
6 months ago
Shad Amethyst
76ad77cd09
✨ No more compilation errors :)
6 months ago
Shad Amethyst
a8c3cd1aa1
Fix most issues with porting
6 months ago
Shad Amethyst
80349c3496
Remove namespace that conflicted with #aligns
6 months ago
Shad Amethyst
7806ecb35e
✨ Raw port through mathport
6 months ago
