Shad Amethyst
431a2931d7
✨ Implement UltrafilterInBasis.map_basis
10 months ago
Shad Amethyst
e84ff177bd
✨ Start working on Filter.InBasis
10 months ago
Shad Amethyst
7b4307d76c
✨ Split apart the implications of theorem 3.5 to be able to use ultraprefilters
11 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 α.
11 months ago
Shad Amethyst
65e1ab7fc8
📝 Refactor RegularSupportBasis
11 months ago
Shad Amethyst
60111656b8
✨ Replace ContinuousMulAction with ContinuousConstSMul
11 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
11 months ago
Shad Amethyst
50b4b49932
✨ Fully prove proposition 3.5
11 months ago
Shad Amethyst
24dd2c4f0a
🔥 New notation for RigidStabilizer and prove first lemma for proposition 3.5
11 months ago
Shad Amethyst
522f345f34
✨ Implement SMul on filters, prove compactness of smulImage and that orbit is a subset of support
11 months ago
Shad Amethyst
23d0821290
✨ Almost complete proof of proposition 3.5
11 months ago
Shad Amethyst
55d674e96a
✨ Implement RigidStabilizerBasis and AlgebraicCentralizerBasis
11 months ago
Shad Amethyst
5d81de14d4
🚚 Move RegularSupportBasis to its own file
11 months ago
Shad Amethyst
9e6258bf5c
🚚 Rename AssociatedPoset to RegularSupportBasis
11 months ago
Laurent Bartholdi
cfb341daeb
Added rubin
11 months ago
Shad Amethyst
52b5b5523b
📝 Add installation instructions and push to github
11 months ago
Shad Amethyst
7afc87d0f9
⬆️ Upgrade mathlib and lean version to latest
11 months ago
Shad Amethyst
69ad593f4b
✨ Prove proposition 3.2
11 months ago
Shad Amethyst
a09187c7fa
✨ Start proving proposition 3.2
11 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
11 months ago
Shad Amethyst
3b0b8a8a65
✨ Define group action from HomeoGroup to AssociatedPoset
11 months ago
Shad Amethyst
652e1a0773
🚚 Move a bunch of definitions around, making Topology importable from more files
11 months ago
Shad Amethyst
18912139ec
Rename smulImage_subset to smulImage_mono
11 months ago
Shad Amethyst
03cec8913a
✨ Start working on homeomorphic groups
11 months ago
Shad Amethyst
d5cd873cf6
✨ Implement remark 2.3
11 months ago
Shad Amethyst
7a8184548b
🚚 Move proofs of Rubin's theorem to Rubin.lean
11 months ago
Shad Amethyst
6ce7127efe
🎨 Small renames for consistency
11 months ago
Shad Amethyst
4b4a719d40
✨ Working proof of proposition 2.1
11 months ago
Shad Amethyst
fc12acb37b
✨ Implement most of proposition 2.1
11 months ago
Shad Amethyst
4d8a4d0f1a
✨ Transition over RegularSupport
12 months ago
Shad Amethyst
9df983f476
✨ Clean up algebraic disjointness
12 months ago
Shad Amethyst
43784b1210
✨ Translate and clean up up to remark 1.2
12 months ago
Shad Amethyst
cd9ad02e1d
✨ Prove disjoint_nbhd_fin
12 months ago
Shad Amethyst
d96318acc8
✨ Translate proposition 1.1.1 to lean4
12 months ago
Shad Amethyst
171caae2d3
✨ Move out toplogical actions and faithful actions
12 months ago
Shad Amethyst
adc7194774
🚚 Start moving more theorems in different files
12 months ago
Shad Amethyst
5fcca86b58
🚚 Move tactic to Rubin/Tactic.lean, wrap everything in a namespace
12 months ago
Shad Amethyst
049434fcd8
✨ Implement the group_action tactic
12 months ago
Shad Amethyst
76ad77cd09
✨ No more compilation errors :)
12 months ago
Shad Amethyst
a8c3cd1aa1
Fix most issues with porting
12 months ago
Shad Amethyst
80349c3496
Remove namespace that conflicted with #aligns
12 months ago
Shad Amethyst
7806ecb35e
✨ Raw port through mathport
12 months ago
Shad Amethyst
6470249db0
✨ Add lean3 version of rubin's wip proof
12 months ago
