rubin-lean4/Rubin/HomeoGroup.lean

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