amethyst
/
rubin-lean4
1
0
Fork 1
Code Issues Pull Requests 1 Packages Projects Releases Wiki Activity

📝 Refactor RegularSupportBasis

Browse Source
laurent-lost-commits
Shad Amethyst 5 months ago
parent 60111656b8
commit 65e1ab7fc8
2 changed files with 180 additions and 412 deletions
Show Stats Download Patch File Download Diff File

211
Rubin.lean
Unescape View File

@ -741,8 +741,6 @@ open Topology
variable {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α]
variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α]
example : TopologicalSpace G := TopologicalSpace.generateFrom (RigidStabilizerBasis.asSets G α)
theorem proposition_3_4_2 {α : Type _} [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] (F : Ultrafilter α):
(∃ p : α, ClusterPt p F) ↔ ∃ S ∈ F, IsCompact (closure S) :=
by
@ -775,8 +773,8 @@ variable [Group G]
variable [TopologicalSpace α] [T2Space α]
variable [MulAction G α] [ContinuousConstSMul G α] [FaithfulSMul G α] [LocallyMoving G α]
def RSuppSubsets {α : Type _} [TopologicalSpace α] (V : Set α) : Set (Set α) :=
{W ∈ RegularSupportBasis.asSet α | W ⊆ V}
def RSuppSubsets (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] (V : Set α) : Set (Set α) :=
{W ∈ RegularSupportBasis G α | W ⊆ V}
def RSuppOrbit {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] (F : Filter α) (H : Subgroup G) : Set (Set α) :=
{ g •'' W | (g ∈ H) (W ∈ F) }
@ -804,12 +802,14 @@ lemma compact_subset_of_rsupp_basis (G : Type _) {α : Type _}
[Group G] [TopologicalSpace α] [T2Space α]
[MulAction G α] [ContinuousConstSMul G α]
[LocallyCompactSpace α] [HasNoIsolatedPoints α] [LocallyDense G α]
(U : RegularSupportBasis α):
∃ V : RegularSupportBasis α, (closure V.val) ⊆ U.val ∧ IsCompact (closure V.val) :=
{U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α):
∃ V : RegularSupportBasis G α, (closure V.val) ⊆ U ∧ IsCompact (closure V.val) :=
by
let ⟨x, x_in_U⟩ := U.nonempty
let ⟨W, W_compact, x_in_intW, W_ss_U⟩ := exists_compact_subset U.regular.isOpen x_in_U
have ⟨V, V_in_basis, x_in_V, V_ss_intW⟩ := (RegularSupportBasis.isBasis G α).exists_subset_of_mem_open x_in_intW isOpen_interior
let ⟨⟨x, x_in_U⟩, _⟩ := (RegularSupportBasis.mem_iff U).mp U_in_basis
have U_regular : Regular U := RegularSupportBasis.regular U_in_basis
let ⟨W, W_compact, x_in_intW, W_ss_U⟩ := exists_compact_subset U_regular.isOpen x_in_U
have ⟨V, V_in_basis, _, V_ss_intW⟩ := (RegularSupportBasis.isBasis G α).exists_subset_of_mem_open x_in_intW isOpen_interior
have clV_ss_W : closure V ⊆ W := by
calc
@ -823,10 +823,8 @@ by
apply IsClosed.closure_eq
exact W_compact.isClosed
rw [RegularSupportBasis.mem_asSet] at V_in_basis
let ⟨V', V'_val⟩ := V_in_basis
use V'
rw [V'_val]
use ⟨V, V_in_basis⟩
simp
constructor
· exact subset_trans clV_ss_W W_ss_U
@ -839,18 +837,18 @@ This proposition gives an alternative definition for an ultrafilter to converge
This alternative definition should be reconstructible entirely from the algebraic structure of `G`.
--/
theorem proposition_3_5 [LocallyDense G α] [LocallyCompactSpace α] [HasNoIsolatedPoints α]
(U : RegularSupportBasis α) (F: Ultrafilter α):
(∃ p ∈ U.val, ClusterPt p F)
↔ ∃ V : RegularSupportBasis α, V ≤ U ∧ RSuppSubsets V.val ⊆ RSuppOrbit F G•[U.val] :=
{U : Set α} (U_in_basis : U ∈ RegularSupportBasis G α) (F: Ultrafilter α):
(∃ p ∈ U, ClusterPt p F)
↔ ∃ V : RegularSupportBasis G α, V.val ⊆ U ∧ RSuppSubsets G V.val ⊆ RSuppOrbit F G•[U] :=
by
constructor
{
simp
intro p p_in_U p_clusterPt
have U_open : IsOpen U.val := U.regular.isOpen
have U_regular : Regular U := RegularSupportBasis.regular U_in_basis
-- First, get a neighborhood of p that is a subset of the closure of the orbit of G_U
have clOrbit_in_nhds := LocallyDense.rigidStabilizer_in_nhds G α U_open p_in_U
have clOrbit_in_nhds := LocallyDense.rigidStabilizer_in_nhds G α U_regular.isOpen p_in_U
rw [mem_nhds_iff] at clOrbit_in_nhds
let ⟨V, V_ss_clOrbit, V_open, p_in_V⟩ := clOrbit_in_nhds
clear clOrbit_in_nhds
@ -858,57 +856,50 @@ by
-- Then, get a nontrivial element from that set
let ⟨g, g_in_rist, g_ne_one⟩ := LocallyMoving.get_nontrivial_rist_elem (G := G) V_open ⟨p, p_in_V⟩
have V_ss_clU : V ⊆ closure U.val := by
have V_ss_clU : V ⊆ closure U := by
apply subset_trans
exact V_ss_clOrbit
apply closure_mono
exact orbit_rigidStabilizer_subset p_in_U
-- The regular support of g is within U
have rsupp_ss_U : RegularSupport α g ⊆ U.val := by
have rsupp_ss_U : RegularSupport α g ⊆ U := by
rw [RegularSupport]
rw [rigidStabilizer_support] at g_in_rist
calc
InteriorClosure (Support α g) ⊆ InteriorClosure V := by
apply interiorClosure_mono
assumption
_ ⊆ InteriorClosure (closure U.val) := by
_ ⊆ InteriorClosure (closure U) := by
apply interiorClosure_mono
assumption
_ ⊆ InteriorClosure U.val := by
_ ⊆ InteriorClosure U := by
simp
rfl
_ ⊆ _ := by
apply subset_of_eq
exact U.regular
exact U_regular
-- Use as the chosen set RegularSupport g
let g' : HomeoGroup α := HomeoGroup.fromContinuous α g
have g'_ne_one : g' ≠ 1 := by
simp
rw [<-HomeoGroup.fromContinuous_one (G := G)]
rw [HomeoGroup.fromContinuous_eq_iff]
exact g_ne_one
use RegularSupportBasis.fromSingleton g' g'_ne_one
let T := RegularSupportBasis.fromSingleton (α := α) g g_ne_one
have T_eq : T.val = RegularSupport α g := by
unfold_let
rw [RegularSupportBasis.fromSingleton_val]
use T.val
constructor
repeat' apply And.intro
· -- This statement is equivalent to rsupp(g) ⊆ U
rw [RegularSupportBasis.le_def]
rw [RegularSupportBasis.fromSingleton_val]
unfold RegularSupportInter₀
simp
rw [T_eq]
exact rsupp_ss_U
· exact T.prop.left
· exact T.prop.right
· intro W W_in_subsets
rw [RegularSupportBasis.fromSingleton_val] at W_in_subsets
unfold RSuppSubsets RegularSupportInter₀ at W_in_subsets
simp at W_in_subsets
let ⟨W_in_basis, W_subset_rsupp⟩ := W_in_subsets
clear W_in_subsets g' g'_ne_one
simp [RSuppSubsets, T_eq] at W_in_subsets
let ⟨W_in_basis, W_ss_W⟩ := W_in_subsets
unfold RSuppOrbit
simp
-- We have that W is a subset of the closure of the orbit of G_U
have W_ss_clOrbit : W ⊆ closure (MulAction.orbit (↥(RigidStabilizer G U.val)) p) := by
have W_ss_clOrbit : W ⊆ closure (MulAction.orbit G•[U] p) := by
rw [rigidStabilizer_support] at g_in_rist
calc
W ⊆ RegularSupport α g := by assumption
@ -921,18 +912,11 @@ by
apply closure_mono
assumption
-- W is also open and nonempty...
have W_open : IsOpen W := by
let ⟨W', W'_eq⟩ := (RegularSupportBasis.mem_asSet _).mp W_in_basis
rw [<-W'_eq]
exact W'.regular.isOpen
have W_nonempty : Set.Nonempty W := by
let ⟨W', W'_eq⟩ := (RegularSupportBasis.mem_asSet _).mp W_in_basis
rw [<-W'_eq]
exact W'.nonempty
let ⟨W_nonempty, ⟨W_seed, W_eq⟩⟩ := W_in_basis
have W_regular := RegularSupportBasis.regular W_in_basis
-- So we can get an element `h` such that `h • p ∈ W` and `h ∈ G_U`
let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_nonempty W_ss_clOrbit
let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_regular.isOpen W_nonempty W_ss_clOrbit
use h
constructor
@ -954,30 +938,33 @@ by
rw [basis.mem_iff]
use h⁻¹ •'' W
repeat' apply And.intro
· rw [RegularSupportBasis.mem_asSet]
rw [RegularSupportBasis.mem_asSet] at W_in_basis
let ⟨W', W'_eq⟩ := W_in_basis
have dec_eq : DecidableEq (HomeoGroup α) := Classical.decEq _
use (HomeoGroup.fromContinuous α h⁻¹) • W'
rw [RegularSupportBasis.smul_val, W'_eq]
simp
· rw [smulImage_nonempty]
assumption
· simp only [smulImage_inv, inv_inv]
have dec_eq : DecidableEq G := Classical.typeDecidableEq G
use Finset.image (fun g => h⁻¹ * g * h) W_seed
rw [<-RegularSupport.FiniteInter_conj, Finset.image_image]
have fn_eq_id : (fun g => h * g * h⁻¹) ∘ (fun g => h⁻¹ * g * h) = id := by
ext x
simp
group
rw [fn_eq_id, Finset.image_id]
exact W_eq
· rw [mem_smulImage, inv_inv]
exact hp_in_W
· exact Eq.subset rfl
}
{
intro ⟨V, ⟨V_ss_U, subsets_ss_orbit⟩⟩
rw [RegularSupportBasis.le_def] at V_ss_U
intro ⟨⟨V, V_in_basis⟩, ⟨V_ss_U, subsets_ss_orbit⟩⟩
simp only at V_ss_U
simp only at subsets_ss_orbit
-- Obtain a compact subset of V' in the basis
let ⟨V', clV'_ss_V, clV'_compact⟩ := compact_subset_of_rsupp_basis G V
let ⟨V', clV'_ss_V, clV'_compact⟩ := compact_subset_of_rsupp_basis G V_in_basis
have V'_in_subsets : V'.val ∈ RSuppSubsets V.val := by
have V'_in_subsets : V'.val ∈ RSuppSubsets G V := by
unfold RSuppSubsets
simp
constructor
unfold RegularSupportBasis.asSet
simp
exact subset_trans subset_closure clV'_ss_V
-- V' is in the orbit, so there exists a value `g ∈ G_U` such that `gV ∈ F`
@ -1090,36 +1077,36 @@ variable [TopologicalSpace α] [MulAction G α] [ContinuousConstSMul G α]
variable [FaithfulSMul G α] [T2Space α] [LocallyMoving G α]
theorem IsRigidSubgroup.has_regularSupportBasis {S : Set G} (S_rigid : IsRigidSubgroup S) :
∃ (U : RegularSupportBasis α), G•[U.val] = S :=
∃ (U : RegularSupportBasis G α), G•[U.val] = S :=
by
let ⟨S_ne_bot, ⟨T, S_eq⟩⟩ := S_rigid
rw [S_eq]
simp only [Subgroup.coe_eq]
rw [S_eq, <-Subgroup.coe_bot, ne_eq, Subgroup.coe_eq, <-ne_eq] at S_ne_bot
let T' : Finset (HomeoGroup α) := Finset.map (HomeoGroup.fromContinuous_embedding α) T
have T'_rsupp_nonempty : Set.Nonempty (RegularSupportInter₀ T') := by
unfold RegularSupportInter₀
simp only [proposition_2_1 (G := G) (α := α)] at S_ne_bot
-- let T' : Finset (HomeoGroup α) := Finset.map (HomeoGroup.fromContinuous_embedding α) T
let T' := RegularSupport.FiniteInter α T
have T'_nonempty : Set.Nonempty T' := by
simp only [RegularSupport.FiniteInter, proposition_2_1 (G := G) (α := α)] at S_ne_bot
rw [ne_eq, <-rigidStabilizer_iInter_regularSupport', <-ne_eq] at S_ne_bot
let ⟨x, x_in_iInter⟩ := rigidStabilizer_neBot S_ne_bot
use x
simp
simp at x_in_iInter
exact x_in_iInter
let T'' := RegularSupportBasis.fromSeed ⟨T', T'_rsupp_nonempty⟩
have T''_val : T''.val = RegularSupportInter₀ T' := rfl
use T''
rw [T''_val]
unfold RegularSupportInter₀
simp
exact rigidStabilizer_neBot S_ne_bot
have T'_in_basis : T' ∈ RegularSupportBasis G α := by
constructor
assumption
use T
use ⟨T', T'_in_basis⟩
simp [RegularSupport.FiniteInter]
rw [rigidStabilizer_iInter_regularSupport']
simp only [<-proposition_2_1]
noncomputable def IsRigidSubgroup.toRegularSupportBasis {S : Set G} (S_rigid : IsRigidSubgroup S) :
RegularSupportBasis α
RegularSupportBasis G α
:= Exists.choose (IsRigidSubgroup.has_regularSupportBasis α S_rigid)
theorem IsRigidSubgroup.toRegularSupportBasis_eq {S : Set G} (S_rigid : IsRigidSubgroup S):
@ -1127,20 +1114,29 @@ theorem IsRigidSubgroup.toRegularSupportBasis_eq {S : Set G} (S_rigid : IsRigidS
by
exact Exists.choose_spec (IsRigidSubgroup.has_regularSupportBasis α S_rigid)
theorem IsRigidSubgroup.toRegularSupportBasis_regular {S : Set G} (S_rigid : IsRigidSubgroup S):
Regular (S_rigid.toRegularSupportBasis α).val :=
by
apply RegularSupportBasis.regular (G := G)
exact (toRegularSupportBasis α S_rigid).prop
theorem IsRigidSubgroup.toRegularSupportBasis_nonempty {S : Set G} (S_rigid : IsRigidSubgroup S):
Set.Nonempty (S_rigid.toRegularSupportBasis α).val :=
by
exact (Subtype.prop (S_rigid.toRegularSupportBasis α)).left
theorem IsRigidSubgroup.toRegularSupportBasis_mono {S T : Set G} (S_rigid : IsRigidSubgroup S)
(T_rigid : IsRigidSubgroup T) :
S ⊆ T ↔ S_rigid.toRegularSupportBasis α ≤ T_rigid.toRegularSupportBasis α :=
S ⊆ T ↔ (S_rigid.toRegularSupportBasis α : Set α) ⊆ T_rigid.toRegularSupportBasis α :=
by
rw [RegularSupportBasis.le_def]
rw [rigidStabilizer_subset_iff G (toRegularSupportBasis_regular _ S_rigid) (toRegularSupportBasis_regular _ T_rigid)]
constructor
· intro S_ss_T
rw [<-IsRigidSubgroup.toRegularSupportBasis_eq (α := α) S_rigid] at S_ss_T
rw [<-IsRigidSubgroup.toRegularSupportBasis_eq (α := α) T_rigid] at S_ss_T
simp at S_ss_T
rw [<-rigidStabilizer_subset_iff G (RegularSupportBasis.regular _) (RegularSupportBasis.regular _)] at S_ss_T
exact S_ss_T
· intro Sr_ss_Tr
rw [rigidStabilizer_subset_iff G (RegularSupportBasis.regular _) (RegularSupportBasis.regular _)] at Sr_ss_Tr
-- TODO: clean that up
have Sr_ss_Tr' : (G•[(toRegularSupportBasis α S_rigid).val] : Set G)
⊆ G•[(toRegularSupportBasis α T_rigid).val] :=
@ -1155,7 +1151,6 @@ theorem IsRigidSubgroup.toRegularSupportBasis_mono' {S T : Set G} (S_rigid : IsR
(T_rigid : IsRigidSubgroup T) :
S ⊆ T ↔ (S_rigid.toRegularSupportBasis α : Set α) ⊆ (T_rigid.toRegularSupportBasis α : Set α) :=
by
rw [<-RegularSupportBasis.le_def]
rw [<-IsRigidSubgroup.toRegularSupportBasis_mono]
end toRegularSupportBasis
@ -1219,6 +1214,7 @@ instance RubinFilter.to_action_filter_neBot {F : RubinFilter G} [Nonempty α] :
rw [Filter.iInf_neBot_iff_of_directed]
· intro ⟨S, S_in_F, S_rigid⟩
simp
apply IsRigidSubgroup.toRegularSupportBasis_nonempty
· intro ⟨S, S_in_F, S_rigid⟩ ⟨T, T_in_F, T_rigid⟩
simp
use S ∩ T
@ -1270,6 +1266,10 @@ theorem RubinFilter.to_action_ultrafilter_converges (F : RubinFilter G) [Nonempt
∃ p ∈ (U_rigid.toRegularSupportBasis α).val, ClusterPt p (F.to_action_ultrafilter α) :=
by
rw [proposition_3_5 (G := G)]
swap
{
apply Subtype.prop (IsRigidSubgroup.toRegularSupportBasis α U_rigid)
}
let ⟨V, V_rigid, V_ss_U, algsubs_ss_algorb⟩ := F.converges U U_in_F U_rigid
let V' := V_rigid.toSubgroup
@ -1284,22 +1284,17 @@ by
unfold RSuppSubsets RSuppOrbit
simp
intro S S_rsupp_basis S_ss_V
intro S S_in_basis S_ss_V
-- let ⟨S', S'_eq⟩ := S_in_basis.right
have S_regular : Regular S := by
let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis
rw [<-S'_eq]
exact S'.regular
have S_regular : Regular S := RegularSupportBasis.regular S_in_basis
have S_nonempty : Set.Nonempty S := by
let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis
rw [<-S'_eq]
exact S'.nonempty
have S_nonempty : Set.Nonempty S := S_in_basis.left
have GS_ss_V : G•[S] ≤ V := by
rw [<-V_rigid.toRegularSupportBasis_eq (α := α)]
simp
rw [<-rigidStabilizer_subset_iff G (α := α) S_regular (RegularSupportBasis.regular _)]
rw [<-rigidStabilizer_subset_iff G (α := α) S_regular (IsRigidSubgroup.toRegularSupportBasis_regular _ _)]
assumption
-- TODO: show that G•[S] ∈ AlgebraicSubsets V
@ -1308,11 +1303,10 @@ by
simp
constructor
· rw [rigidStabilizerBasis_eq_algebraicCentralizerBasis (α := α)]
let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis
rw [<-S'_eq]
rw [RigidStabilizerBasis.mem_iff' _ (LocallyMoving.locally_moving _ S'.regular.isOpen S'.nonempty)]
sorry
let ⟨S', S'_eq⟩ := S_in_basis.right
rw [RigidStabilizerBasis.mem_iff' _ (LocallyMoving.locally_moving _ S_regular.isOpen S_nonempty)]
use S'
rw [RigidStabilizerInter₀, S'_eq, RegularSupport.FiniteInter, rigidStabilizer_iInter_regularSupport']
· exact GS_ss_V
let ⟨g, g_in_U, W, W_in_F, W_rigid, Wconj_eq_GS⟩ := algsubs_ss_algorb GS_in_algsubs_V
@ -1334,14 +1328,11 @@ by
swap
{
rw [<-smulImage_regular (G := G)]
apply RegularSupportBasis.regular
apply IsRigidSubgroup.toRegularSupportBasis_regular
}
swap
{
let ⟨S', S'_eq⟩ := (RegularSupportBasis.mem_asSet S).mp S_rsupp_basis
rw [<-S'_eq]
exact S'.regular
}
exact S_regular
ext i
rw [rigidStabilizer_smulImage, <-Wconj_eq_GS, <-IsRigidSubgroup.mem_subgroup, <-SetLike.mem_coe, IsRigidSubgroup.toRegularSupportBasis_eq]
simp

381
Rubin/RegularSupportBasis.lean
Unescape View File

@ -1,6 +1,6 @@
/-
This files defines `RegularSupportBasis`, which is a basis of the topological space α,
made up of finite intersections of `RegularSupport α g` for `g : HomeoGroup α`.
made up of finite intersections of `RegularSupport α g` for `g : G`.
-/
import Mathlib.Topology.Basic
@ -14,52 +14,43 @@ import Rubin.RegularSupport
import Rubin.HomeoGroup
namespace Rubin
section RegularSupportBasis.Prelude
variable {α : Type _}
variable [TopologicalSpace α]
variable [DecidableEq α]
/--
Maps a "seed" of homeorphisms in α to the intersection of their regular support in α.
Note that the condition that the resulting set is non-empty is introduced later in `RegularSupportBasis₀`
--/
def RegularSupportInter₀ (S : Finset (HomeoGroup α)): Set α :=
def RegularSupport.FiniteInter {G : Type _} [Group G] (α : Type _) [TopologicalSpace α] [MulAction G α] (S : Finset G): Set α :=
⋂ (g ∈ S), RegularSupport α g
theorem RegularSupportInter₀.eq_sInter (S : Finset (HomeoGroup α)) :
RegularSupportInter₀ S = ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) :=
def RegularSupportBasis (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] : Set (Set α) :=
{ S : Set α | S.Nonempty ∧ ∃ (seed : Finset G), S = RegularSupport.FiniteInter α seed }
variable {G : Type _}
variable {α : Type _}
variable [Group G]
variable [TopologicalSpace α]
variable [MulAction G α]
theorem RegularSupport.FiniteInter_sInter (S : Finset G) :
RegularSupport.FiniteInter α S = ⋂₀ ((fun (g : G) => RegularSupport α g) '' S) :=
by
rw [Set.sInter_image]
rfl
/--
This is a predecessor type to `RegularSupportBasis`, where equality is defined on the `seed` used, rather than the `val`.
--/
structure RegularSupportBasis₀ (α : Type _) [TopologicalSpace α] where
seed : Finset (HomeoGroup α)
val_nonempty : Set.Nonempty (RegularSupportInter₀ seed)
theorem RegularSupportBasis₀.eq_iff_seed_eq (S T : RegularSupportBasis₀ α) : S = T ↔ S.seed = T.seed := by
-- Spooky :3c
rw [mk.injEq]
def RegularSupportBasis₀.val (S : RegularSupportBasis₀ α) : Set α := RegularSupportInter₀ S.seed
theorem RegularSupportBasis₀.val_def (S : RegularSupportBasis₀ α) : S.val = RegularSupportInter₀ S.seed := rfl
@[simp]
theorem RegularSupportBasis₀.nonempty (S : RegularSupportBasis₀ α) : Set.Nonempty S.val := S.val_nonempty
theorem RegularSupportBasis.mem_iff (S : Set α) :
S ∈ RegularSupportBasis G α ↔ S.Nonempty ∧ ∃ (seed : Finset G), S = RegularSupport.FiniteInter α seed :=
by
simp only [RegularSupportBasis, Set.mem_setOf_eq]
@[simp]
theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular S.val := by
rw [S.val_def]
rw [RegularSupportInter₀.eq_sInter]
theorem RegularSupportBasis.regular {S : Set α} (S_mem_basis : S ∈ RegularSupportBasis G α) : Regular S := by
let ⟨_, ⟨seed, S_eq_inter⟩⟩ := (RegularSupportBasis.mem_iff S).mp S_mem_basis
rw [S_eq_inter, RegularSupport.FiniteInter_sInter]
apply regular_sInter
· have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α)
let fin : Finset (Set α) := S.seed.image ((fun g => RegularSupport α g))
let fin : Finset (Set α) := seed.image ((fun g => RegularSupport α g))
apply Set.Finite.ofFinset fin
simp
@ -69,10 +60,12 @@ theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular
rw [<-Heq]
exact regularSupport_regular α g
lemma RegularSupportInter₀.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α):
RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupportInter₀ seed :=
variable [ContinuousConstSMul G α] [DecidableEq G]
lemma RegularSupport.FiniteInter_conj (seed : Finset G) (f : G):
RegularSupport.FiniteInter α (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupport.FiniteInter α seed :=
by
unfold RegularSupportInter₀
unfold RegularSupport.FiniteInter
simp
conv => {
rhs
@ -81,85 +74,46 @@ by
rw [regularSupport_smulImage]
}
variable [DecidableEq (HomeoGroup α)]
/--
A `HomeoGroup α` group element `f` acts on an `RegularSupportBasis₀ α` set `S`,
A group element `f` acts on sets of `RegularSupportBasis G α`,
by mapping each element `g` of `S.seed` to `f * g * f⁻¹`
--/
instance homeoGroup_smul₂ : SMul (HomeoGroup α) (RegularSupportBasis₀ α) where
smul := fun f S => ⟨
(Finset.image (fun g => f * g * f⁻¹) S.seed),
by
rw [RegularSupportInter₀.mul_seed]
simp
exact S.val_nonempty
⟩
theorem RegularSupportBasis₀.smul_seed (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
(f • S).seed = (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
theorem RegularSupportBasis₀.smul_val (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
(f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
theorem RegularSupportBasis₀.smul_val' (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
noncomputable instance RegularSupportBasis.instSmul : SMul G (RegularSupportBasis G α) where
smul := fun f S =>
let new_seed := (Finset.image (fun g => f * g * f⁻¹) S.prop.right.choose)
⟨
RegularSupport.FiniteInter α new_seed,
by
rw [RegularSupportBasis.mem_iff]
nth_rw 1 [RegularSupport.FiniteInter_conj, smulImage_nonempty]
rw [<-S.prop.right.choose_spec]
constructor
· exact S.prop.left
· use new_seed
⟩
theorem RegularSupportBasis.smul_eq' (f : G) (S : RegularSupportBasis G α) :
(f • S).val
= RegularSupport.FiniteInter α (Finset.image (fun g => f * g * f⁻¹) S.prop.right.choose) := rfl
theorem RegularSupportBasis.smul_eq (f : G) (S : RegularSupportBasis G α) :
(f • S).val = f •'' S.val :=
by
unfold val
rw [<-RegularSupportInter₀.mul_seed]
rw [RegularSupportBasis₀.smul_seed]
-- We define a "preliminary" group action from `HomeoGroup α` to `RegularSupportBasis₀`
instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (RegularSupportBasis₀ α) where
one_smul := by
intro S
rw [RegularSupportBasis₀.eq_iff_seed_eq]
rw [RegularSupportBasis₀.smul_seed]
simp
mul_smul := by
intro f g S
rw [RegularSupportBasis₀.eq_iff_seed_eq]
repeat rw [RegularSupportBasis₀.smul_seed]
rw [Finset.image_image]
ext x
simp
group
end RegularSupportBasis.Prelude
-- TODO: define RegularSupportBasis as a Set directly?
/--
A partially-ordered set, associated to Rubin's proof.
Any element in that set is made up of a `seed`,
such that `val = RegularSupportInter₀ seed` and `Set.Nonempty val`.
Actions on this set are first defined in terms of `RegularSupportBasis₀`,
as the proofs otherwise get hairy with a bunch of `Exists.choose` appearing.
--/
structure RegularSupportBasis (α : Type _) [TopologicalSpace α] where
val : Set α
val_has_seed : ∃ po_seed : RegularSupportBasis₀ α, po_seed.val = val
namespace RegularSupportBasis
variable {α : Type _}
variable [TopologicalSpace α]
variable [DecidableEq α]
theorem eq_iff_val_eq (S T : RegularSupportBasis α) : S = T ↔ S.val = T.val := by
rw [mk.injEq]
def fromSeed (seed : RegularSupportBasis₀ α) : RegularSupportBasis α := ⟨
seed.val,
⟨seed, seed.val_def⟩
⟩
def fromSingleton [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) : RegularSupportBasis α :=
let seed : RegularSupportBasis₀ α := ⟨
{g},
rw [RegularSupportBasis.smul_eq']
rw [RegularSupport.FiniteInter_conj]
rw [<-S.prop.right.choose_spec]
def RegularSupportBasis.fromSingleton [T2Space α] [FaithfulSMul G α] (g : G) (g_ne_one : g ≠ 1) : { S : Set α // S ∈ RegularSupportBasis G α } :=
let seed : Finset G := {g}
⟨
RegularSupport.FiniteInter α seed,
by
unfold RegularSupportInter₀
simp
rw [RegularSupportBasis.mem_iff]
constructor
swap
use seed
rw [Set.nonempty_iff_ne_empty]
intro rsupp_empty
apply g_ne_one
@ -169,181 +123,34 @@ def fromSingleton [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) : Regula
rw [<-not_mem_support]
apply Set.not_mem_subset
· apply support_subset_regularSupport
· rw [rsupp_empty]
· simp [RegularSupport.FiniteInter] at rsupp_empty
rw [rsupp_empty]
exact Set.not_mem_empty x
⟩
fromSeed seed
theorem fromSingleton_val [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) :
(fromSingleton g g_ne_one).val = RegularSupportInter₀ {g} := rfl
noncomputable def full_seed (S : RegularSupportBasis α) : RegularSupportBasis₀ α :=
(Exists.choose S.val_has_seed)
noncomputable def seed (S : RegularSupportBasis α) : Finset (HomeoGroup α) :=
S.full_seed.seed
instance : Coe (RegularSupportBasis₀ α) (RegularSupportBasis α) where
coe := fromSeed
@[simp]
theorem full_seed_seed (S : RegularSupportBasis α) : S.full_seed.seed = S.seed := rfl
@[simp]
theorem fromSeed_val (seed : RegularSupportBasis₀ α) :
(seed : RegularSupportBasis α).val = seed.val :=
by
unfold fromSeed
simp
@[simp]
theorem val_from_seed (S : RegularSupportBasis α) : RegularSupportInter₀ S.seed = S.val := by
unfold seed full_seed
rw [<-RegularSupportBasis₀.val_def]
rw [Exists.choose_spec S.val_has_seed]
@[simp]
theorem val_from_seed₂ (S : RegularSupportBasis α) : S.full_seed.val = S.val := by
unfold full_seed
rw [RegularSupportBasis₀.val_def]
nth_rw 2 [<-val_from_seed]
unfold seed full_seed
rfl
-- Allows one to prove properties of RegularSupportBasis without jumping through `Exists.choose`-shaped hoops
theorem prop_from_val {p : Set α → Prop}
(any_seed : ∀ po_seed : RegularSupportBasis₀ α, p po_seed.val) :
∀ (S : RegularSupportBasis α), p S.val :=
by
intro S
rw [<-val_from_seed]
have res := any_seed S.full_seed
rw [val_from_seed₂] at res
rw [val_from_seed]
exact res
@[simp]
theorem nonempty : ∀ (S : RegularSupportBasis α), Set.Nonempty S.val :=
prop_from_val RegularSupportBasis₀.nonempty
@[simp]
theorem regular : ∀ (S : RegularSupportBasis α), Regular S.val :=
prop_from_val RegularSupportBasis₀.regular
variable [DecidableEq (HomeoGroup α)]
instance homeoGroup_smul₃ : SMul (HomeoGroup α) (RegularSupportBasis α) where
smul := fun f S => ⟨
f •'' S.val,
by
use f • S.full_seed
rw [RegularSupportBasis₀.smul_val']
simp
⟩
theorem smul_val (f : HomeoGroup α) (S : RegularSupportBasis α) :
(f • S).val = f •'' S.val := rfl
theorem smul_seed' (f : HomeoGroup α) (S : RegularSupportBasis α) (seed : Finset (HomeoGroup α)) :
S.val = RegularSupportInter₀ seed →
(f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) :=
by
intro S_val_eq
rw [smul_val]
rw [RegularSupportInter₀.mul_seed]
rw [S_val_eq]
theorem smul_seed (f : HomeoGroup α) (S : RegularSupportBasis α) :
(f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) :=
by
apply smul_seed'
symm
exact val_from_seed S
theorem RegularSupportBasis.fromSingleton_val [T2Space α] [FaithfulSMul G α] (g : G) (g_ne_one : g ≠ 1) :
(fromSingleton g g_ne_one).val = RegularSupport α g := by simp [fromSingleton, RegularSupport.FiniteInter]
-- Note: we could potentially implement MulActionHom
instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (RegularSupportBasis α) where
noncomputable instance RegularSupportBasis.instMulAction : MulAction G (RegularSupportBasis G α) where
one_smul := by
intro S
rw [eq_iff_val_eq]
repeat rw [smul_val]
apply Subtype.eq
rw [RegularSupportBasis.smul_eq]
rw [one_smulImage]
mul_smul := by
intro S f g
rw [eq_iff_val_eq]
repeat rw [smul_val]
apply Subtype.eq
repeat rw [RegularSupportBasis.smul_eq]
rw [smulImage_mul]
instance associatedPoset_le : LE (RegularSupportBasis α) where
le := fun S T => S.val ⊆ T.val
theorem le_def (S T : RegularSupportBasis α) : S ≤ T ↔ S.val ⊆ T.val := by
rw [iff_eq_eq]
rfl
instance associatedPoset_partialOrder : PartialOrder (RegularSupportBasis α) where
le_refl := fun S => (le_def S S).mpr (le_refl S.val)
le_trans := fun S T U S_le_T S_le_U => (le_def S U).mpr (le_trans
((le_def _ _).mp S_le_T)
((le_def _ _).mp S_le_U)
)
le_antisymm := by
intro S T S_le_T T_le_S
rw [le_def] at S_le_T
rw [le_def] at T_le_S
rw [eq_iff_val_eq]
apply le_antisymm <;> assumption
theorem smul_mono {S T : RegularSupportBasis α} (f : HomeoGroup α) (S_le_T : S ≤ T) :
f • S ≤ f • T :=
theorem RegularSupportBasis.smul_mono {S T : RegularSupportBasis G α} (f : G) (S_le_T : S.val ⊆ T.val) :
(f • S).val ⊆ (f • T).val :=
by
rw [le_def]
repeat rw [smul_val]
repeat rw [RegularSupportBasis.smul_eq]
apply smulImage_mono
assumption
instance associatedPoset_coeSet : Coe (RegularSupportBasis α) (Set α) where
coe := RegularSupportBasis.val
def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) :=
{ S : Set α | ∃ T : RegularSupportBasis α, T.val = S }
theorem asSet_def :
RegularSupportBasis.asSet α = { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } := rfl
theorem mem_asSet (S : Set α) :
S ∈ RegularSupportBasis.asSet α ↔ ∃ T : RegularSupportBasis α, T.val = S :=
by
rw [asSet_def]
simp
theorem mem_asSet' (S : Set α) :
S ∈ RegularSupportBasis.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = RegularSupportInter₀ seed :=
by
rw [asSet_def]
simp
constructor
· intro ⟨T, T_eq⟩
rw [<-T_eq]
constructor
simp
let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed
rw [RegularSupportBasis₀.val_def] at eq
simp at eq
use seed
exact eq.symm
· intro ⟨S_nonempty, ⟨seed, val_from_seed⟩⟩
rw [val_from_seed] at S_nonempty
use fromSeed ⟨seed, S_nonempty⟩
rw [val_from_seed]
simp
rw [RegularSupportBasis₀.val_def]
instance membership : Membership α (RegularSupportBasis α) where
mem := fun x S => x ∈ S.val
theorem mem_iff (x : α) (S : RegularSupportBasis α) : x ∈ S ↔ x ∈ (S : Set α) := iff_eq_eq ▸ rfl
section Basis
open Topology
@ -408,56 +215,26 @@ by
/--
## Proposition 3.2 : RegularSupportBasis is a topological basis of `α`
-/
theorem isBasis :
TopologicalSpace.IsTopologicalBasis (RegularSupportBasis.asSet α) :=
theorem RegularSupportBasis.isBasis :
TopologicalSpace.IsTopologicalBasis (RegularSupportBasis G α) :=
by
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
{
intro U U_in_poset
rw [RegularSupportBasis.mem_asSet] at U_in_poset
let ⟨T, T_val⟩ := U_in_poset
rw [<-T_val]
exact T.regular.isOpen
exact (RegularSupportBasis.regular U_in_poset).isOpen
}
intro p U p_in_U U_open
let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G α U_open p_in_U
use RegularSupport α g
repeat' apply And.intro
· rw [RegularSupportBasis.mem_asSet']
constructor
exact ⟨p, p_in_rsupp⟩
use {HomeoGroup.fromContinuous α g}
unfold RegularSupportInter₀
simp
· exact p_in_rsupp
· exact ⟨p, p_in_rsupp⟩
· use {g}
simp [RegularSupport.FiniteInter]
· assumption
· apply subset_trans
exact rsupp_ss_clW
exact clW_ss_U
-- example (p : α): ∃ (S : Set α), S ∈ (RegularSupportBasis.asSet α) ∧ IsCompact (closure S) ∧ p ∈ S :=
-- by
-- have h₁ := TopologicalSpace.IsTopologicalBasis.nhds_hasBasis (isBasis G α) (a := p)
-- have h₂ := compact_basis_nhds p
-- rw [Filter.hasBasis_iff] at h₁
-- rw [Filter.hasBasis_iff] at h₂
-- have T : Set α := sorry
-- have T_in_nhds : T ∈ 𝓝 p := sorry
-- let ⟨U, ⟨⟨U_in_nhds, U_compact⟩, U_ss_T⟩⟩ := (h₂ T).mp T_in_nhds
-- let ⟨V, ⟨⟨V_in_basis, p_in_V⟩, V_ss_T⟩⟩ := (h₁ U).mp U_in_nhds
-- use V
-- (repeat' apply And.intro) <;> try assumption
-- -- apply IsCompact.of_isClosed_subset
-- -- · assumption
-- -- · sorry
-- -- · assumption
-- sorry
end Basis
end RegularSupportBasis
end Rubin

Write Preview
Loading…
Cancel
Save