You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
rubin-lean4/Rubin/HomeoGroup.lean

454 lines
13 KiB

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

import Mathlib.Logic.Equiv.Defs
import Mathlib.Topology.Basic
import Mathlib.Topology.Homeomorph
import Rubin.LocallyDense
import Rubin.Topology
import Rubin.RegularSupport
structure HomeoGroup (α : Type _) [TopologicalSpace α] extends
Homeomorph α α
variable {α : Type _}
variable [TopologicalSpace α]
def HomeoGroup.coe : HomeoGroup α -> Homeomorph α α := HomeoGroup.toHomeomorph
def HomeoGroup.from : Homeomorph α α -> HomeoGroup α := HomeoGroup.mk
instance homeoGroup_coe : Coe (HomeoGroup α) (Homeomorph α α) where
coe := HomeoGroup.coe
instance homeoGroup_coe₂ : Coe (Homeomorph α α) (HomeoGroup α) where
coe := HomeoGroup.from
def HomeoGroup.toPerm : HomeoGroup α → Equiv.Perm α := fun g => g.coe.toEquiv
instance homeoGroup_coe_perm : Coe (HomeoGroup α) (Equiv.Perm α) where
coe := HomeoGroup.toPerm
@[simp]
theorem HomeoGroup.toPerm_def (g : HomeoGroup α) : g.coe.toEquiv = (g : Equiv.Perm α) := rfl
@[simp]
theorem HomeoGroup.mk_coe (g : HomeoGroup α) : HomeoGroup.mk (g.coe) = g := rfl
@[simp]
theorem HomeoGroup.eq_iff_coe_eq {f g : HomeoGroup α} : f.coe = g.coe ↔ f = g := by
constructor
{
intro f_eq_g
rw [<-HomeoGroup.mk_coe f]
rw [f_eq_g]
simp
}
{
intro f_eq_g
unfold HomeoGroup.coe
rw [f_eq_g]
}
@[simp]
theorem HomeoGroup.from_toHomeomorph (m : Homeomorph α α) : (HomeoGroup.from m).toHomeomorph = m := rfl
instance homeoGroup_one : One (HomeoGroup α) where
one := HomeoGroup.from (Homeomorph.refl α)
theorem HomeoGroup.one_def : (1 : HomeoGroup α) = (Homeomorph.refl α : HomeoGroup α) := rfl
instance homeoGroup_inv : Inv (HomeoGroup α) where
inv := fun g => HomeoGroup.from (g.coe.symm)
@[simp]
theorem HomeoGroup.inv_def (g : HomeoGroup α) : (Homeomorph.symm g.coe : HomeoGroup α) = g⁻¹ := rfl
theorem HomeoGroup.coe_inv {g : HomeoGroup α} : HomeoGroup.coe (g⁻¹) = (HomeoGroup.coe g).symm := rfl
instance homeoGroup_mul : Mul (HomeoGroup α) where
mul := fun a b => ⟨b.toHomeomorph.trans a.toHomeomorph⟩
theorem HomeoGroup.coe_mul {f g : HomeoGroup α} : HomeoGroup.coe (f * g) = (HomeoGroup.coe g).trans (HomeoGroup.coe f) := rfl
@[simp]
theorem HomeoGroup.mul_def (f g : HomeoGroup α) : HomeoGroup.from ((HomeoGroup.coe g).trans (HomeoGroup.coe f)) = f * g := rfl
instance homeoGroup_group : Group (HomeoGroup α) where
mul_assoc := by
intro a b c
rw [<-HomeoGroup.eq_iff_coe_eq]
repeat rw [HomeoGroup_coe_mul]
rfl
mul_one := by
intro a
rw [<-HomeoGroup.eq_iff_coe_eq]
rw [HomeoGroup.coe_mul]
rfl
one_mul := by
intro a
rw [<-HomeoGroup.eq_iff_coe_eq]
rw [HomeoGroup.coe_mul]
rfl
mul_left_inv := by
intro a
rw [<-HomeoGroup.eq_iff_coe_eq]
rw [HomeoGroup.coe_mul]
rw [HomeoGroup.coe_inv]
simp
rfl
/--
The HomeoGroup trivially has a continuous and faithful `MulAction` on the underlying topology `α`.
--/
instance homeoGroup_smul₁ : SMul (HomeoGroup α) α where
smul := fun g x => g.toFun x
@[simp]
theorem HomeoGroup.smul₁_def (f : HomeoGroup α) (x : α) : f.toFun x = f • x := rfl
@[simp]
theorem HomeoGroup.smul₁_def' (f : HomeoGroup α) (x : α) : f.toHomeomorph x = f • x := rfl
@[simp]
theorem HomeoGroup.coe_toFun_eq_smul₁ (f : HomeoGroup α) (x : α) : FunLike.coe (HomeoGroup.coe f) x = f • x := rfl
instance homeoGroup_mulAction₁ : MulAction (HomeoGroup α) α where
one_smul := by
intro x
rfl
mul_smul := by
intro f g x
rfl
instance homeoGroup_mulAction₁_continuous : Rubin.ContinuousMulAction (HomeoGroup α) α where
continuous := by
intro h
constructor
intro S S_open
conv => {
congr; ext
congr; ext
rw [<-HomeoGroup.smul₁_def']
}
simp only [Homeomorph.isOpen_preimage]
exact S_open
instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α where
eq_of_smul_eq_smul := by
intro f g hyp
rw [<-HomeoGroup.eq_iff_coe_eq]
ext x
simp
exact hyp x
namespace Rubin
section AssociatedPoset.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 `AssociatedPosetSeed`
--/
def AssociatedPosetElem (S : Finset (HomeoGroup α)): Set α :=
⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S)
/--
This is a predecessor type to `AssociatedPoset`, where equality is defined on the `seed` used, rather than the `val`.
--/
structure AssociatedPosetSeed (α : Type _) [TopologicalSpace α] where
seed : Finset (HomeoGroup α)
val_nonempty : Set.Nonempty (AssociatedPosetElem seed)
theorem AssociatedPosetSeed.eq_iff_seed_eq (S T : AssociatedPosetSeed α) : S = T ↔ S.seed = T.seed := by
-- Spooky :3c
rw [mk.injEq]
def AssociatedPosetSeed.val (S : AssociatedPosetSeed α) : Set α := AssociatedPosetElem S.seed
theorem AssociatedPosetSeed.val_def (S : AssociatedPosetSeed α) : S.val = AssociatedPosetElem S.seed := rfl
@[simp]
theorem AssociatedPosetSeed.nonempty (S : AssociatedPosetSeed α) : Set.Nonempty S.val := S.val_nonempty
@[simp]
theorem AssociatedPosetSeed.regular (S : AssociatedPosetSeed α) : Regular S.val := by
rw [S.val_def]
unfold AssociatedPosetElem
apply regular_sInter
· have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α)
let fin : Finset (Set α) := S.seed.image ((fun g => RegularSupport α g))
apply Set.Finite.ofFinset fin
simp
· intro S S_in_set
simp at S_in_set
let ⟨g, ⟨_, Heq⟩⟩ := S_in_set
rw [<-Heq]
exact regularSupport_regular α g
lemma AssociatedPosetElem.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α):
AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' AssociatedPosetElem seed :=
by
unfold AssociatedPosetElem
simp
conv => {
rhs
ext; lhs; ext x; ext; lhs
ext
rw [regularSupport_smulImage]
}
variable [DecidableEq (HomeoGroup α)]
/--
A `HomeoGroup α` group element `f` acts on an `AssociatedPosetSeed α` set `S`,
by mapping each element `g` of `S.seed` to `f * g * f⁻¹`
--/
instance homeoGroup_smul₂ : SMul (HomeoGroup α) (AssociatedPosetSeed α) where
smul := fun f S => ⟨
(Finset.image (fun g => f * g * f⁻¹) S.seed),
by
rw [AssociatedPosetElem.mul_seed]
simp
exact S.val_nonempty
theorem AssociatedPosetSeed.smul_seed (f : HomeoGroup α) (S : AssociatedPosetSeed α) :
(f • S).seed = (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
theorem AssociatedPosetSeed.smul_val (f : HomeoGroup α) (S : AssociatedPosetSeed α) :
(f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
theorem AssociatedPosetSeed.smul_val' (f : HomeoGroup α) (S : AssociatedPosetSeed α) :
(f • S).val = f •'' S.val :=
by
unfold val
rw [<-AssociatedPosetElem.mul_seed]
rw [AssociatedPosetSeed.smul_seed]
-- We define a "preliminary" group action from `HomeoGroup α` to `AssociatedPosetSeed`
instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (AssociatedPosetSeed α) where
one_smul := by
intro S
rw [AssociatedPosetSeed.eq_iff_seed_eq]
rw [AssociatedPosetSeed.smul_seed]
simp
mul_smul := by
intro f g S
rw [AssociatedPosetSeed.eq_iff_seed_eq]
repeat rw [AssociatedPosetSeed.smul_seed]
rw [Finset.image_image]
ext x
simp
group
end AssociatedPoset.Prelude
/--
A partially-ordered set, associated to Rubin's proof.
Any element in that set is made up of a `seed`,
such that `val = AssociatedPosetElem seed` and `Set.Nonempty val`.
Actions on this set are first defined in terms of `AssociatedPosetSeed`,
as the proofs otherwise get hairy with a bunch of `Exists.choose` appearing.
--/
structure AssociatedPoset (α : Type _) [TopologicalSpace α] where
val : Set α
val_has_seed : ∃ po_seed : AssociatedPosetSeed α, po_seed.val = val
namespace AssociatedPoset
variable {α : Type _}
variable [TopologicalSpace α]
variable [DecidableEq α]
theorem eq_iff_val_eq (S T : AssociatedPoset α) : S = T ↔ S.val = T.val := by
rw [mk.injEq]
def fromSeed (seed : AssociatedPosetSeed α) : AssociatedPoset α := ⟨
seed.val,
⟨seed, seed.val_def⟩
noncomputable def full_seed (S : AssociatedPoset α) : AssociatedPosetSeed α :=
(Exists.choose S.val_has_seed)
noncomputable def seed (S : AssociatedPoset α) : Finset (HomeoGroup α) :=
S.full_seed.seed
@[simp]
theorem full_seed_seed (S : AssociatedPoset α) : S.full_seed.seed = S.seed := rfl
@[simp]
theorem fromSeed_val (seed : AssociatedPosetSeed α) :
(fromSeed seed).val = seed.val :=
by
unfold fromSeed
simp
@[simp]
theorem val_from_seed (S : AssociatedPoset α) : AssociatedPosetElem S.seed = S.val := by
unfold seed full_seed
rw [<-AssociatedPosetSeed.val_def]
rw [Exists.choose_spec S.val_has_seed]
@[simp]
theorem val_from_seed₂ (S : AssociatedPoset α) : S.full_seed.val = S.val := by
unfold full_seed
rw [AssociatedPosetSeed.val_def]
nth_rw 2 [<-val_from_seed]
unfold seed full_seed
rfl
-- Allows one to prove properties of AssociatedPoset without jumping through `Exists.choose`-shaped hoops
theorem prop_from_val {p : Set α → Prop}
(any_seed : ∀ po_seed : AssociatedPosetSeed α, p po_seed.val) :
∀ (S : AssociatedPoset α), 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 : AssociatedPoset α), Set.Nonempty S.val :=
prop_from_val AssociatedPosetSeed.nonempty
@[simp]
theorem regular : ∀ (S : AssociatedPoset α), Regular S.val :=
prop_from_val AssociatedPosetSeed.regular
variable [DecidableEq (HomeoGroup α)]
instance homeoGroup_smul₃ : SMul (HomeoGroup α) (AssociatedPoset α) where
smul := fun f S => ⟨
f •'' S.val,
by
use f • S.full_seed
rw [AssociatedPosetSeed.smul_val']
simp
theorem smul_val (f : HomeoGroup α) (S : AssociatedPoset α) :
(f • S).val = f •'' S.val := rfl
theorem smul_seed' (f : HomeoGroup α) (S : AssociatedPoset α) (seed : Finset (HomeoGroup α)) :
S.val = AssociatedPosetElem seed →
(f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) :=
by
intro S_val_eq
rw [smul_val]
rw [AssociatedPosetElem.mul_seed]
rw [S_val_eq]
theorem smul_seed (f : HomeoGroup α) (S : AssociatedPoset α) :
(f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) S.seed) :=
by
apply smul_seed'
symm
exact val_from_seed S
-- Note: we could potentially implement MulActionHom
instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (AssociatedPoset α) where
one_smul := by
intro S
rw [eq_iff_val_eq]
repeat rw [smul_val]
rw [one_smulImage]
mul_smul := by
intro S f g
rw [eq_iff_val_eq]
repeat rw [smul_val]
rw [smulImage_mul]
instance associatedPoset_le : LE (AssociatedPoset α) where
le := fun S T => S.val ⊆ T.val
theorem le_def (S T : AssociatedPoset α) : S ≤ T ↔ S.val ⊆ T.val := by
rw [iff_eq_eq]
rfl
instance associatedPoset_partialOrder : PartialOrder (AssociatedPoset α) 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 : AssociatedPoset α} (f : HomeoGroup α) (S_le_T : S ≤ T) :
f • S ≤ f • T :=
by
rw [le_def]
repeat rw [smul_val]
apply smulImage_mono
assumption
end AssociatedPoset
section Other
theorem homeoGroup_rigidStabilizer_subset_iff {α : Type _} [TopologicalSpace α]
[h_lm : LocallyMoving (HomeoGroup α) α]
{U V : Set α} (U_reg : Regular U) (V_reg : Regular V):
U ⊆ V ↔ RigidStabilizer (HomeoGroup α) U ≤ RigidStabilizer (HomeoGroup α) V :=
by
constructor
exact rigidStabilizer_mono
intro rist_ss
by_contra U_not_ss_V
let W := U \ closure V
have W_nonempty : Set.Nonempty W := by
by_contra W_empty
apply U_not_ss_V
apply subset_from_diff_closure_eq_empty
· assumption
· exact U_reg.isOpen
· rw [Set.not_nonempty_iff_eq_empty] at W_empty
exact W_empty
have W_ss_U : W ⊆ U := by
simp
exact Set.diff_subset _ _
have W_open : IsOpen W := by
unfold_let
rw [Set.diff_eq_compl_inter]
apply IsOpen.inter
simp
exact U_reg.isOpen
have ⟨f, f_in_ristW, f_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open W_nonempty
have f_in_ristU : f ∈ RigidStabilizer (HomeoGroup α) U := by
exact rigidStabilizer_mono W_ss_U f_in_ristW
have f_notin_ristV : f ∉ RigidStabilizer (HomeoGroup α) V := by
apply rigidStabilizer_compl f_ne_one
apply rigidStabilizer_mono _ f_in_ristW
calc
W = U ∩ (closure V)ᶜ := by unfold_let; rw [Set.diff_eq_compl_inter, Set.inter_comm]
_ ⊆ (closure V)ᶜ := Set.inter_subset_right _ _
_ ⊆ Vᶜ := by
rw [Set.compl_subset_compl]
exact subset_closure
exact f_notin_ristV (rist_ss f_in_ristU)
end Other
end Rubin