@ -3,52 +3,40 @@ import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.Subgroup.Actions
import Mathlib.GroupTheory.Subgroup.Actions
import Mathlib.GroupTheory.Commutator
import Mathlib.GroupTheory.Commutator
import Mathlib.Topology.Basic
import Mathlib.Topology.Basic
import Mathlib.Topology.Algebra.ConstMulAction
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Perm
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.IntervalCases
import Rubin.RigidStabilizer
import Rubin.RigidStabilizer
import Rubin.SmulImage
import Rubin.SmulImage
import Rubin.Topology
import Rubin.Topological
import Rubin.FaithfulAction
import Rubin.FaithfulAction
import Rubin.Period
import Rubin.Period
import Rubin.LocallyDense
namespace Rubin
namespace Rubin
variable {G : Type _} [Group G]
class LocallyMoving (G α : Type _) [Group G] [TopologicalSpace α ] [MulAction G α ] :=
locally_moving: ∀ U : Set α , IsOpen U → Set.Nonempty U → RigidStabilizer G U ≠ ⊥
theorem Commute.conj (f g h : G) : Commute (f * g * f⁻¹) h ↔ Commute g (f⁻¹ * h * f) := by
#align is_locally_moving Rubin.LocallyMoving
suffices ∀ (f g h : G), Commute (f * g * f⁻¹) h → Commute g (f⁻¹ * h * f) by
constructor
namespace LocallyMoving
· apply this
· intro cg
theorem get_nontrivial_rist_elem {G α : Type _}
symm
[Group G]
nth_rw 1 [<-inv_inv f]
[TopologicalSpace α ]
apply this
[MulAction G α ]
symm
[h_lm : LocallyMoving G α ]
rw [inv_inv]
{U: Set α }
exact cg
(U_open : IsOpen U)
(U_nonempty : U.Nonempty) :
intro f g h fgf_h_comm
∃ x : G, x ∈ RigidStabilizer G U ∧ x ≠ 1 :=
unfold Commute SemiconjBy at *
by
rw [<-mul_assoc, <-mul_assoc]
have rist_ne_bot := h_lm.locally_moving U U_open U_nonempty
rw [<-mul_assoc, <-mul_assoc] at fgf_h_comm
exact (or_iff_right rist_ne_bot).mp (Subgroup.bot_or_exists_ne_one _)
have gfh_eq : g * f⁻¹ * h = f⁻¹ * h * f * g * f⁻¹ := by
repeat rw [mul_assoc f⁻¹]
rw [<-fgf_h_comm]
group
rw [gfh_eq]
group
theorem Commute.conj' (f g h : G) : Commute (f⁻¹ * g * f) h ↔ Commute g (f * h * f⁻¹) := by
nth_rw 2 [<-inv_inv f]
nth_rw 3 [<-inv_inv f]
apply Commute.conj
end LocallyMoving
structure AlgebraicallyDisjointElem (f g h : G) :=
structure AlgebraicallyDisjointElem {G : Type _} [Group G] (f g h : G) :=
non_commute: ¬Commute f h
non_commute: ¬Commute f h
fst : G
fst : G
snd : G
snd : G
@ -59,51 +47,18 @@ structure AlgebraicallyDisjointElem (f g h : G) :=
namespace AlgebraicallyDisjointElem
namespace AlgebraicallyDisjointElem
def comm_elem {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : G :=
def comm_elem {G : Type _} [Group G] { f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) : G :=
⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆
⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆
@[simp]
@[simp]
theorem comm_elem_eq {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) :
theorem comm_elem_eq {G : Type _} [Group G] { f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) :
disj_elem.comm_elem = ⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆ :=
disj_elem.comm_elem = ⁅disj_elem.fst, ⁅disj_elem.snd, h⁆⁆ :=
by
by
unfold comm_elem
unfold comm_elem
simp
simp
lemma comm_elem_conj (f g h i : G) :
⁅i * f * i⁻¹, ⁅i * g * i⁻¹, i * h * i⁻¹⁆⁆ = i * ⁅f, ⁅g, h⁆⁆ * i⁻¹ := by group
theorem conj {f g h : G} (disj_elem : AlgebraicallyDisjointElem f g h) (i : G): AlgebraicallyDisjointElem (i * f * i⁻¹) (i * g * i⁻¹) (i * h * i⁻¹) where
non_commute := by
rw [Commute.conj]
group
exact disj_elem.non_commute
fst := i * disj_elem.fst * i⁻¹
snd := i * disj_elem.snd * i⁻¹
fst_commute := by
rw [Commute.conj]
group
exact disj_elem.fst_commute
snd_commute := by
rw [Commute.conj]
group
exact disj_elem.snd_commute
comm_elem_nontrivial := by
intro eq_one
apply disj_elem.comm_elem_nontrivial
rw [comm_elem_conj, <-mul_right_inv i] at eq_one
apply mul_right_cancel at eq_one
nth_rw 2 [<-mul_one i] at eq_one
apply mul_left_cancel at eq_one
exact eq_one
comm_elem_commute := by
rw [comm_elem_conj, Commute.conj]
rw [(by group : i⁻¹ * (i * g * i⁻¹) * i = g)]
exact disj_elem.comm_elem_commute
end AlgebraicallyDisjointElem
end AlgebraicallyDisjointElem
-- Also known as `η_G(f)`.
/--
/--
A pair (f, g) is said to be "algebraically disjoint" if it can produce an instance of
A pair (f, g) is said to be "algebraically disjoint" if it can produce an instance of
[`AlgebraicallyDisjointElem`] for any element `h ∈ G` such that `f` and `h` don't commute.
[`AlgebraicallyDisjointElem`] for any element `h ∈ G` such that `f` and `h` don't commute.
@ -114,8 +69,7 @@ so that `⁅f₁, ⁅f₂, h⁆⁆` is a nontrivial element of `Centralizer(g, G
Here the definition of `k ∈ Centralizer(g, G)` is directly unrolled as `Commute k g`.
Here the definition of `k ∈ Centralizer(g, G)` is directly unrolled as `Commute k g`.
This is a slightly weaker proposition than plain disjointness,
This is a slightly stronger proposition that plain disjointness, a
but it is easier to derive from the hypothesis of Rubin's theorem.
-/
-/
def AlgebraicallyDisjoint {G : Type _} [Group G] (f g : G) :=
def AlgebraicallyDisjoint {G : Type _} [Group G] (f g : G) :=
∀ (h : G), ¬Commute f h → AlgebraicallyDisjointElem f g h
∀ (h : G), ¬Commute f h → AlgebraicallyDisjointElem f g h
@ -135,18 +89,7 @@ fun (h : G) (nc : ¬Commute f h) => {
exact (mk_thm h nc).choose_spec.choose_spec.right.right.right
exact (mk_thm h nc).choose_spec.choose_spec.right.right.right
}
}
/--
-- This is an idea of having a Prop version of AlgebraicallyDisjoint, but it sounds painful to work with
This definition simply wraps `AlgebraicallyDisjoint` as a `Prop`.
It is equivalent to it, although since `AlgebraicallyDisjoint` isn't a `Prop`,
an `↔` (iff) statement joining the two cannot be written.
You should consider using it when proving `↔`/`∧` kinds of theorems, or when tools like `cases` are needed,
as the base `AlgebraicallyDisjoint` isn't a `Prop` and won't work with those.
The two `Coe` and `CoeFn` instances provided around this type make it essentially transparent —
you can use an instance of `AlgebraicallyDisjoint` in place of a `IsAlgebraicallyDisjoint` and vice-versa.
You might need to add the odd `↑` (coe) operator to make Lean happy.
--/
def IsAlgebraicallyDisjoint {G : Type _} [Group G] (f g : G): Prop :=
def IsAlgebraicallyDisjoint {G : Type _} [Group G] (f g : G): Prop :=
∀ (h : G), ¬Commute f h → ∃ (f₁ f₂ : G), ∃ (elem : AlgebraicallyDisjointElem f g h), elem.fst = f₁ ∧ elem.snd = f₂
∀ (h : G), ¬Commute f h → ∃ (f₁ f₂ : G), ∃ (elem : AlgebraicallyDisjointElem f g h), elem.fst = f₁ ∧ elem.snd = f₂
@ -179,26 +122,95 @@ noncomputable instance coeFnAlgebraicallyDisjoint : CoeFun
instance coeAlgebraicallyDisjoint : Coe (AlgebraicallyDisjoint f g) (IsAlgebraicallyDisjoint f g) where
instance coeAlgebraicallyDisjoint : Coe (AlgebraicallyDisjoint f g) (IsAlgebraicallyDisjoint f g) where
coe := mk
coe := mk
theorem conj (is_alg_disj : IsAlgebraicallyDisjoint f g) (h : G) :
IsAlgebraicallyDisjoint (h * f * h⁻¹) (h * g * h⁻¹) :=
by
apply elim at is_alg_disj
apply mk
intro i nc
rw [Commute.conj] at nc
rw [(by group : i = h * (h⁻¹ * i * h) * h⁻¹)]
exact (is_alg_disj (h⁻¹ * i * h) nc).conj h
end IsAlgebraicallyDisjoint
end IsAlgebraicallyDisjoint
-- TODO: find a better home for these lemmas
@[simp]
theorem orbit_bot (G : Type _) [Group G] [MulAction G α ] (p : α ) :
MulAction.orbit (⊥ : Subgroup G) p = {p} :=
by
ext1
rw [MulAction.mem_orbit_iff]
constructor
· rintro ⟨⟨_, g_bot⟩, g_to_x⟩
rw [← g_to_x, Set.mem_singleton_iff, Subgroup.mk_smul]
exact (Subgroup.mem_bot.mp g_bot).symm ▸ one_smul _ _
exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩
#align orbit_bot Rubin.orbit_bot
variable {G α : Type _}
variable {G α : Type _}
variable [Group G]
variable [Group G]
variable [TopologicalSpace α ]
variable [TopologicalSpace α ]
variable [MulAction G α ]
variable [ContinuousMulAction G α ]
variable [ContinuousConstSMul G α ]
variable [FaithfulSMul G α ]
variable [FaithfulSMul G α ]
instance dense_locally_moving [T2Space α ]
(H_nip : has_no_isolated_points α )
(H_ld : LocallyDense G α ) :
LocallyMoving G α
where
locally_moving := by
intros U _ H_nonempty
by_contra h_rs
have ⟨elem, ⟨_, some_in_orbit⟩⟩ := H_ld.nonEmpty H_nonempty
have H_nebot := has_no_isolated_points_neBot H_nip elem
rw [h_rs] at some_in_orbit
simp at some_in_orbit
lemma disjoint_nbhd [T2Space α ] {g : G} {x : α } (x_moved: g • x ≠ x) :
∃ U: Set α , IsOpen U ∧ x ∈ U ∧ Disjoint U (g •'' U) :=
by
have ⟨V, W, V_open, W_open, gx_in_V, x_in_W, disjoint_V_W⟩ := T2Space.t2 (g • x) x x_moved
let U := (g⁻¹ •'' V) ∩ W
use U
constructor
{
-- NOTE: if this is common, then we should make a tactic for solving IsOpen goals
exact IsOpen.inter (img_open_open g⁻¹ V V_open) W_open
}
constructor
{
simp
rw [mem_inv_smulImage]
trivial
}
{
apply Set.disjoint_of_subset
· apply Set.inter_subset_right
· intro y hy; show y ∈ V
rw [<-smul_inv_smul g y]
rw [<-mem_inv_smulImage]
rw [mem_smulImage] at hy
simp at hy
exact hy.left
· exact disjoint_V_W.symm
}
lemma disjoint_nbhd_in [T2Space α ] {g : G} {x : α } {V : Set α }
(V_open : IsOpen V) (x_in_V : x ∈ V) (x_moved : g • x ≠ x) :
∃ U : Set α , IsOpen U ∧ x ∈ U ∧ U ⊆ V ∧ Disjoint U (g •'' U) :=
by
have ⟨W, W_open, x_in_W, disjoint_W_img⟩ := disjoint_nbhd x_moved
use W ∩ V
simp
constructor
{
apply IsOpen.inter <;> assumption
}
constructor
{
constructor <;> assumption
}
show Disjoint (W ∩ V) (g •'' W ∩ V)
apply Set.disjoint_of_subset
· exact Set.inter_subset_left W V
· show g •'' W ∩ V ⊆ g •'' W
rewrite [smulImage_inter]
exact Set.inter_subset_left _ _
· exact disjoint_W_img
-- Kind of a boring lemma but okay
-- Kind of a boring lemma but okay
lemma rewrite_Union (f : Fin 2 × Fin 2 → Set α ) :
lemma rewrite_Union (f : Fin 2 × Fin 2 → Set α ) :
(⋃ (i : Fin 2 × Fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) :=
(⋃ (i : Fin 2 × Fin 2), f i) = (f (0,0) ∪ f (0,1)) ∪ (f (1,0) ∪ f (1,1)) :=
@ -214,6 +226,97 @@ by
<;> simp only [h, true_or, or_true]
<;> simp only [h, true_or, or_true]
· rintro ((h|h)|(h|h)) <;> exact ⟨_, h⟩
· rintro ((h|h)|(h|h)) <;> exact ⟨_, h⟩
-- TODO: move to Rubin.lean
-- TODO: modify the proof to be less "let everything"-y, especially the first half
-- TODO: use the new class thingy to write a cleaner proof?
lemma proposition_1_1_1 [h_lm : LocallyMoving G α ] [T2Space α ] (f g : G) (supp_disjoint : Disjoint (Support α f) (Support α g)) : AlgebraicallyDisjoint f g := by
apply AlgebraicallyDisjoint_mk
intros h h_not_commute
-- h is not the identity on `Support α f`
have f_h_not_disjoint := (mt (disjoint_commute (G := G) (α := α )) h_not_commute)
have ⟨x, ⟨x_in_supp_f, x_in_supp_h⟩⟩ := Set.not_disjoint_iff.mp f_h_not_disjoint
have hx_ne_x := mem_support.mp x_in_supp_h
-- Since α is Hausdoff, there is a nonempty V ⊆ Support α f, with h •'' V disjoint from V
have ⟨V, V_open, x_in_V, V_in_support, disjoint_img_V⟩ := disjoint_nbhd_in (support_open f) x_in_supp_f hx_ne_x
-- let f₂ be a nontrivial element of the RigidStabilizer G V
let ⟨f₂, f₂_in_rist_V, f₂_ne_one⟩ := h_lm.get_nontrivial_rist_elem V_open (Set.nonempty_of_mem x_in_V)
-- Re-use the Hausdoff property of α again, this time yielding W ⊆ V
let ⟨y, y_moved⟩ := faithful_moves_point' α f₂_ne_one
have y_in_V := (rigidStabilizer_support.mp f₂_in_rist_V) (mem_support.mpr y_moved)
let ⟨W, W_open, y_in_W, W_in_V, disjoint_img_W⟩ := disjoint_nbhd_in V_open y_in_V y_moved
-- Let f₁ be a nontrivial element of RigidStabilizer G W
let ⟨f₁, f₁_in_rist_W, f₁_ne_one⟩ := h_lm.get_nontrivial_rist_elem W_open (Set.nonempty_of_mem y_in_W)
use f₁
use f₂
constructor <;> try constructor
· apply disjoint_commute (α := α )
apply Set.disjoint_of_subset_left _ supp_disjoint
calc
Support α f₁ ⊆ W := rigidStabilizer_support.mp f₁_in_rist_W
W ⊆ V := W_in_V
V ⊆ Support α f := V_in_support
· apply disjoint_commute (α := α )
apply Set.disjoint_of_subset_left _ supp_disjoint
calc
Support α f₂ ⊆ V := rigidStabilizer_support.mp f₂_in_rist_V
V ⊆ Support α f := V_in_support
-- We claim that [f₁, [f₂, h]] is a nontrivial elelement of Centralizer G g
let k := ⁅f₂, h⁆
have h₂ : ∀ z ∈ W, f₂ • z = k • z := by
intro z z_in_W
simp
symm
apply disjoint_support_comm f₂ h _ disjoint_img_V
· exact W_in_V z_in_W
· exact rigidStabilizer_support.mp f₂_in_rist_V
constructor
· -- then `k*f₁⁻¹*k⁻¹` is supported on k W = f₂ W,
-- so [f₁,k] is supported on W ∪ f₂ W ⊆ V ⊆ support f, so commutes with g.
apply disjoint_commute (α := α )
apply Set.disjoint_of_subset_left _ supp_disjoint
have supp_f₁_subset_W := (rigidStabilizer_support.mp f₁_in_rist_W)
show Support α ⁅f₁, ⁅f₂, h⁆⁆ ⊆ Support α f
calc
Support α ⁅f₁, k⁆ = Support α ⁅k, f₁⁆ := by rw [<-commutatorElement_inv, support_inv]
_ ⊆ Support α f₁ ∪ (k •'' Support α f₁) := support_comm α k f₁
_ ⊆ W ∪ (k •'' Support α f₁) := Set.union_subset_union_left _ supp_f₁_subset_W
_ ⊆ W ∪ (k •'' W) := by
apply Set.union_subset_union_right
exact (smulImage_subset k supp_f₁_subset_W)
_ = W ∪ (f₂ •'' W) := by rw [<-smulImage_eq_of_smul_eq h₂]
_ ⊆ V ∪ (f₂ •'' W) := Set.union_subset_union_left _ W_in_V
_ ⊆ V ∪ V := by
apply Set.union_subset_union_right
apply smulImage_subset_in_support f₂ W V W_in_V
exact rigidStabilizer_support.mp f₂_in_rist_V
_ ⊆ V := by rw [Set.union_self]
_ ⊆ Support α f := V_in_support
· -- finally, [f₁,k] agrees with f₁ on W, so is not the identity.
have h₄: ∀ z ∈ W, ⁅f₁, k⁆ • z = f₁ • z := by
apply disjoint_support_comm f₁ k
exact rigidStabilizer_support.mp f₁_in_rist_W
rw [<-smulImage_eq_of_smul_eq h₂]
exact disjoint_img_W
let ⟨z, z_in_W, z_moved⟩ := faithful_rigid_stabilizer_moves_point f₁_in_rist_W f₁_ne_one
by_contra h₅
rw [<-h₄ z z_in_W] at z_moved
have h₆ : ⁅f₁, ⁅f₂, h⁆⁆ • z = z := by rw [h₅, one_smul]
exact z_moved h₆
#align proposition_1_1_1 Rubin.proposition_1_1_1
@[simp] lemma smulImage_mul {g h : G} {U : Set α } : g •'' (h •'' U) = (g*h) •'' U :=
(mul_smulImage g h U)
lemma smul_inj_moves {ι : Type*} [Fintype ι ] [T2Space α ]
lemma smul_inj_moves {ι : Type*} [Fintype ι ] [T2Space α ]
{f : ι → G} {x : α } {i j : ι } (i_ne_j : i ≠ j)
{f : ι → G} {x : α } {i j : ι } (i_ne_j : i ≠ j)
(f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) :
(f_smul_inj : Function.Injective (fun i : ι => (f i) • x)) :
@ -222,7 +325,7 @@ lemma smul_inj_moves {ι : Type*} [Fintype ι ] [T2Space α ]
apply i_ne_j
apply i_ne_j
apply f_smul_inj
apply f_smul_inj
group_action
group_action
group at h
group_action at h
exact h
exact h
def smul_inj_nbhd {ι : Type*} [Fintype ι ] [T2Space α ]
def smul_inj_nbhd {ι : Type*} [Fintype ι ] [T2Space α ]
@ -264,7 +367,11 @@ by
let U := ⋂(p : ι₂), smul_inj_nbhd p.prop f_smul_inj
let U := ⋂(p : ι₂), smul_inj_nbhd p.prop f_smul_inj
use U
use U
repeat' apply And.intro
-- The notations provided afterwards tend to be quite ugly because we used `Exists.choose`,
-- but the idea is that this all boils down to applying `Exists.choose_spec`, except in the disjointness case,
-- where we transform `Disjoint (f i •'' U) (f j •'' U)` into `Disjoint U ((f i)⁻¹ * f j •'' U)`
-- and transform both instances of `U` into `N`, the neighborhood of the chosen `(i, j) ∈ ι₂`
repeat' constructor
· apply isOpen_iInter_of_finite
· apply isOpen_iInter_of_finite
intro ⟨⟨i, j⟩, i_ne_j⟩
intro ⟨⟨i, j⟩, i_ne_j⟩
apply smul_inj_nbhd_open
apply smul_inj_nbhd_open
@ -272,8 +379,6 @@ by
intro ⟨⟨i, j⟩, i_ne_j⟩
intro ⟨⟨i, j⟩, i_ne_j⟩
apply smul_inj_nbhd_mem
apply smul_inj_nbhd_mem
· intro i j i_ne_j
· intro i j i_ne_j
-- We transform `Disjoint (f i •'' U) (f j •'' U)` into `Disjoint N ((f i)⁻¹ * f j •'' N)`
let N := smul_inj_nbhd i_ne_j f_smul_inj
let N := smul_inj_nbhd i_ne_j f_smul_inj
have U_subset_N : U ⊆ N := Set.iInter_subset
have U_subset_N : U ⊆ N := Set.iInter_subset
(fun (⟨⟨i, j⟩, i_ne_j⟩ : ι₂) => (smul_inj_nbhd i_ne_j f_smul_inj))
(fun (⟨⟨i, j⟩, i_ne_j⟩ : ι₂) => (smul_inj_nbhd i_ne_j f_smul_inj))
@ -282,7 +387,7 @@ by
rw [disjoint_comm, smulImage_disjoint_mul]
rw [disjoint_comm, smulImage_disjoint_mul]
apply Set.disjoint_of_subset U_subset_N
apply Set.disjoint_of_subset U_subset_N
· apply smulImage_mono
· apply smulImage_subset
exact U_subset_N
exact U_subset_N
· exact smul_inj_nbhd_disjoint i_ne_j f_smul_inj
· exact smul_inj_nbhd_disjoint i_ne_j f_smul_inj
@ -330,7 +435,7 @@ by
unfold_let
unfold_let
rw [h.1]
rw [h.1]
rw [smul_eq_iff_eq_inv_smul]
rw [smul_eq_iff_eq_inv_smul]
group
group_action
symm
symm
exact same_img
exact same_img
}
}
@ -388,7 +493,10 @@ theorem smul_injective_within_period {g : G} {p : α } {n : ℕ }
(period_eq_n : Period.period p g = n) :
(period_eq_n : Period.period p g = n) :
Function.Injective (fun (i : Fin n) => g ^ (i : ℕ ) • p) :=
Function.Injective (fun (i : Fin n) => g ^ (i : ℕ ) • p) :=
by
by
simp only [<-zpow_coe_nat]
have zpow_fix : (fun (i : Fin n) => g ^ (i : ℕ ) • p) = (fun (i : Fin n) => g ^ (i : ℤ ) • p) := by
ext x
simp
rw [zpow_fix]
apply moves_inj
apply moves_inj
intro k one_le_k k_lt_n
intro k one_le_k k_lt_n
@ -398,235 +506,191 @@ by
exact k_lt_n
exact k_lt_n
#align moves_inj_period Rubin.smul_injective_within_period
#align moves_inj_period Rubin.smul_injective_within_period
-- TODO: move to Rubin.lean
/-
lemma moves_1234_of_moves_12 {g : G} {x : α } (g12_moves : g^12 • x ≠ x) :
The algebraic centralizer (and its associated basis) allow for a purely group-theoretic construction of the
Function.Injective (fun i : Fin 5 => g^(i : ℤ ) • x) :=
`RegularSupport` sets.
They are defined as the centralizers of the subgroups `{g^12 | g ∈ G ∧ AlgebraicallyDisjoint f g}`
-/
section AlgebraicCentralizer
variable {G : Type _}
variable [Group G]
-- TODO: prove this is a subgroup?
-- This is referred to as `ξ_G^12(f)`
def AlgebraicSubgroup (f : G) : Set G :=
(fun g : G => g^12) '' { g : G | IsAlgebraicallyDisjoint f g }
def AlgebraicCentralizer (f : G) : Subgroup G :=
Subgroup.centralizer (AlgebraicSubgroup f)
theorem AlgebraicSubgroup.conj (f g : G) :
(fun h => g * h * g⁻¹) '' AlgebraicSubgroup f = AlgebraicSubgroup (g * f * g⁻¹) :=
by
unfold AlgebraicSubgroup
rw [Set.image_image]
have gxg12_eq : ∀ x : G, g * x^12 * g⁻¹ = (g * x * g⁻¹)^12 := by
simp
simp only [gxg12_eq]
ext x
simp
constructor
· intro ⟨y, y_disj, x_eq⟩
use g * y * g⁻¹
rw [<-gxg12_eq]
exact ⟨y_disj.conj g, x_eq⟩
· intro ⟨y, y_disj, x_eq⟩
use g⁻¹ * y * g
constructor
· convert y_disj.conj g⁻¹ using 1
all_goals group
· nth_rw 3 [<-inv_inv g]
simp only [conj_pow]
rw [x_eq]
group
@[simp]
theorem AlgebraicCentralizer.conj (f g : G) :
(fun h => g * h * g⁻¹) '' AlgebraicCentralizer f = AlgebraicCentralizer (g * f * g⁻¹) :=
by
by
unfold AlgebraicCentralizer
apply moves_inj
intros k k_ge_1 k_lt_5
ext x
simp at k_lt_5
simp [Subgroup.mem_centralizer_iff]
by_contra x_fixed
constructor
have k_div_12 : k ∣ 12 := by
· intro ⟨y, ⟨x_comm, x_eq⟩⟩
-- Note: norm_num does not support ℤ .dvd yet, nor ℤ .mod, nor Int.natAbs, nor Int.div, etc.
intro h h_in_alg
have h: (12 : ℤ ) = (12 : ℕ ) := by norm_num
rw [<-AlgebraicSubgroup.conj] at h_in_alg
rw [h, Int.ofNat_dvd_right]
simp at h_in_alg
apply Nat.dvd_of_mod_eq_zero
let ⟨i, i_in_alg, gig_eq_h⟩ := h_in_alg
specialize x_comm i i_in_alg
interval_cases k
rw [<-gig_eq_h, <-x_eq]
all_goals unfold Int.natAbs
group
all_goals norm_num
rw [mul_assoc _ i, x_comm, <-mul_assoc]
· intro x_comm
have g12_fixed : g^12 • x = x := by
use g⁻¹ * x * g
rw [<-zpow_ofNat]
group
simp
intro h h_in_alg
simp [<-AlgebraicSubgroup.conj] at x_comm
specialize x_comm h h_in_alg
have h₁ : g⁻¹ * x * g * h = g⁻¹ * (g * h * g⁻¹ * x) * g := by
rw [x_comm]
group
rw [h₁]
group
/--
Finite intersections of [`AlgebraicCentralizer`].
--/
def AlgebraicCentralizerInter (S : Finset G) : Subgroup G :=
⨅ (g ∈ S), AlgebraicCentralizer g
def AlgebraicCentralizerBasis (G : Type _) [Group G] : Set (Set G) :=
{ S : Set G | S ≠ {1} ∧ ∃ seed : Finset G,
S = AlgebraicCentralizerInter seed
}
theorem AlgebraicCentralizerBasis.mem_iff (S : Set G) :
S ∈ AlgebraicCentralizerBasis G ↔
S ≠ {1} ∧ ∃ seed : Finset G, S = AlgebraicCentralizerInter seed
:= by rfl
theorem AlgebraicCentralizerBasis.subgroup_mem_iff (S : Subgroup G) :
(S : Set G) ∈ AlgebraicCentralizerBasis G ↔
S ≠ ⊥ ∧ ∃ seed : Finset G, S = AlgebraicCentralizerInter seed :=
by
rw [mem_iff, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq]
simp
simp
rw [<-Int.mul_ediv_cancel' k_div_12]
have res := smul_zpow_eq_of_smul_eq (12/k) x_fixed
group_action at res
exact res
theorem AlgebraicCentralizerBasis.empty_not_mem : ∅ ∉ AlgebraicCentralizerBasis G := by
exact g12_moves g12_fixed
simp [AlgebraicCentralizerBasis]
intro _ _
rw [<-ne_eq]
symm
rw [<-Set.nonempty_iff_ne_empty]
exact Subgroup.coe_nonempty _
theorem AlgebraicCentralizerBasis.to_subgroup {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G):
∃ S' : Subgroup G, S = S' :=
by
rw [mem_iff] at S_in_basis
let ⟨_, ⟨seed, S_eq⟩⟩ := S_in_basis
use AlgebraicCentralizerInter seed
theorem Set.image_equiv_eq {α β : Type _} (S : Set α ) (T : Set β) (f : α ≃ β) :
lemma proposition_1_1_2 [T2Space α ] [h_lm : LocallyMoving G α ]
f '' S = T ↔ S = f.symm '' T :=
(f g : G) (h_disj : AlgebraicallyDisjoint f g) : Disjoint (Support α f) (Support α (g^12)) :=
by
by
constructor
by_contra not_disjoint
· intro fS_eq_T
let U := Support α f ∩ Support α (g^12)
ext x
have U_nonempty : U.Nonempty := by
rw [<-fS_eq_T]
apply Set.not_disjoint_iff_nonempty_inter.mp
simp
exact not_disjoint
· intro S_eq_fT
ext x
-- Since G is Hausdorff, we can find a nonempty set V ⊆ such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint
rw [S_eq_fT]
let x := U_nonempty.some
simp
have x_in_U : x ∈ U := Set.Nonempty.some_mem U_nonempty
have fx_moves : f • x ≠ x := Set.inter_subset_left _ _ x_in_U
theorem AlgebraicCentralizerBasis.univ_mem (ex_non_trivial : ∃ g : G, g ≠ 1): Set.univ ∈ AlgebraicCentralizerBasis G := by
rw [mem_iff]
have five_points : Function.Injective (fun i : Fin 5 => g^(i : ℤ ) • x) := by
constructor
apply moves_1234_of_moves_12
exact (Set.inter_subset_right _ _ x_in_U)
have U_open: IsOpen U := (IsOpen.inter (support_open f) (support_open (g^12)))
let ⟨V₀, V₀_open, x_in_V₀, V₀_in_support, disjoint_img_V₀⟩ := disjoint_nbhd_in U_open x_in_U fx_moves
let ⟨V₁, V₁_open, x_in_V₁, disjoint_img_V₁⟩ := disjoint_nbhd_fin five_points
let V := V₀ ∩ V₁
-- Let h be a nontrivial element of the RigidStabilizer G V
let ⟨h, ⟨h_in_ristV, h_ne_one⟩⟩ := h_lm.get_nontrivial_rist_elem (IsOpen.inter V₀_open V₁_open) (Set.nonempty_of_mem ⟨x_in_V₀, x_in_V₁⟩)
have V_disjoint_smulImage: Disjoint V (f •'' V) := by
apply Set.disjoint_of_subset
· exact Set.inter_subset_left _ _
· apply smulImage_subset
exact Set.inter_subset_left _ _
· exact disjoint_img_V₀
have comm_non_trivial : ¬Commute f h := by
by_contra comm_trivial
let ⟨z, z_in_V, z_moved⟩ := faithful_rigid_stabilizer_moves_point h_in_ristV h_ne_one
apply z_moved
nth_rewrite 2 [<-one_smul G z]
rw [<-commutatorElement_eq_one_iff_commute.mpr comm_trivial.symm]
symm
symm
exact Set.nonempty_compl.mp ex_non_trivial
use ∅
simp [AlgebraicCentralizerInter]
theorem AlgebraicCentralizerBasis.conj_mem {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G)
(h : G) : (fun g => h * g * h⁻¹) '' S ∈ AlgebraicCentralizerBasis G :=
by
let ⟨S', S_eq⟩ := to_subgroup S_in_basis
rw [S_eq]
rw [S_eq, subgroup_mem_iff] at S_in_basis
rw [mem_iff]
have conj_eq : (fun g => h * g * h⁻¹) = (MulAut.conj h).toEquiv := by
ext x
simp
constructor
· rw [conj_eq]
rw [ne_eq, Set.image_equiv_eq]
simp
rw [<-Subgroup.coe_bot, SetLike.coe_set_eq]
exact S_in_basis.left
· let ⟨seed, S'_eq⟩ := S_in_basis.right
have dec_eq : DecidableEq G := Classical.typeDecidableEq _
use Finset.image (fun g => h * g * h⁻¹) seed
rw [S'_eq]
unfold AlgebraicCentralizerInter
ext g
rw [conj_eq]
rw [Set.mem_image_equiv]
simp
conv => {
rhs
intro
intro
rw [<-SetLike.mem_coe, <-AlgebraicCentralizer.conj, conj_eq, Set.mem_image_equiv]
}
theorem AlgebraicCentralizerBasis.inter_closed
{S T : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (T_in_basis : T ∈ AlgebraicCentralizerBasis G)
(ST_ne_bot : S ∩ T ≠ {1}) :
S ∩ T ∈ AlgebraicCentralizerBasis G :=
by
let ⟨S', S_eq⟩ := to_subgroup S_in_basis
rw [S_eq]
rw [S_eq, subgroup_mem_iff] at S_in_basis
let ⟨S'_ne_bot, ⟨S'_seed, S'_eq⟩⟩ := S_in_basis
let ⟨T', T_eq⟩ := to_subgroup T_in_basis
rw [T_eq]
rw [T_eq, subgroup_mem_iff] at T_in_basis
let ⟨T'_ne_bot, ⟨T'_seed, T'_eq⟩⟩ := T_in_basis
rw [<-Subgroup.coe_inf, subgroup_mem_iff]
rw [S_eq, T_eq, <-Subgroup.coe_inf, <-Subgroup.coe_bot, ne_eq, SetLike.coe_set_eq, <-ne_eq] at ST_ne_bot
have dec_eq : DecidableEq G := Classical.typeDecidableEq G
refine ⟨ST_ne_bot, ⟨S'_seed ∪ T'_seed, ?inter_eq⟩⟩
apply disjoint_support_comm h f
· exact rigidStabilizer_support.mp h_in_ristV
unfold AlgebraicCentralizerInter
· exact V_disjoint_smulImage
· exact z_in_V
simp only [<-Finset.mem_coe]
rw [Finset.coe_union, iInf_union]
-- Since g is algebraically disjoint from f, there exist f₁,f₂ ∈ C_G(g) so that the commutator h' = [f1,[f2,h]] is a nontrivial element of C_G(g)
rw [S'_eq, T'_eq]
let alg_disj_elem := h_disj h comm_non_trivial
rfl
let f₁ := alg_disj_elem.fst
let f₂ := alg_disj_elem.snd
let h' := alg_disj_elem.comm_elem
def MulAut.conj_order_iso (g : G) : Set G ≃o Set G := (MulAut.conj g).toEquiv.toOrderIsoSet
have f₁_commutes : Commute f₁ g := alg_disj_elem.fst_commute
have f₂_commutes : Commute f₂ g := alg_disj_elem.snd_commute
theorem AlgebraicCentralizerBasis.eq_conj_self (g : G) :
have h'_commutes : Commute h' g := alg_disj_elem.comm_elem_commute
(MulAut.conj_order_iso g) '' AlgebraicCentralizerBasis G = AlgebraicCentralizerBasis G :=
have h'_nontrivial : h' ≠ 1 := alg_disj_elem.comm_elem_nontrivial
by
ext S
have support_f₂_h : Support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := by
simp [MulAut.conj_order_iso]
calc
conv => {
Support α ⁅f₂, h⁆ ⊆ Support α h ∪ (f₂ •'' Support α h) := support_comm α f₂ h
lhs
_ ⊆ V ∪ (f₂ •'' Support α h) := by
congr; intro x
apply Set.union_subset_union_left
rw [Equiv.toOrderIsoSet_apply]
exact rigidStabilizer_support.mp h_in_ristV
}
_ ⊆ V ∪ (f₂ •'' V) := by
simp
apply Set.union_subset_union_right
constructor
apply smulImage_subset
· intro ⟨T, T_in_basis, T_eq⟩
exact rigidStabilizer_support.mp h_in_ristV
rw [<-T_eq]
have support_h' : Support α h' ⊆ ⋃ (i : Fin 2 × Fin 2), (f₁^(i.1.val) * f₂^(i.2.val)) •'' V := by
exact conj_mem T_in_basis g
rw [rewrite_Union]
· intro S_in_basis
simp (config := {zeta := false})
use (fun h => g⁻¹ * h * g⁻¹⁻¹) '' S
rw [<-smulImage_mul, <-smulImage_union]
refine ⟨conj_mem S_in_basis g⁻¹, ?S_eq⟩
calc
rw [Set.image_image]
Support α h' ⊆ Support α ⁅f₂,h⁆ ∪ (f₁ •'' Support α ⁅f₂, h⁆) := support_comm α f₁ ⁅f₂,h⁆
_ ⊆ V ∪ (f₂ •'' V) ∪ (f₁ •'' Support α ⁅f₂, h⁆) := by
apply Set.union_subset_union_left
exact support_f₂_h
_ ⊆ V ∪ (f₂ •'' V) ∪ (f₁ •'' V ∪ (f₂ •'' V)) := by
apply Set.union_subset_union_right
apply smulImage_subset f₁
exact support_f₂_h
-- Since h' is nontrivial, it has at least one point p in its support
let ⟨p, p_moves⟩ := faithful_moves_point' α h'_nontrivial
-- Since g commutes with h', all five of the points {gi(p):i=0..4} lie in supp(h')
have gi_in_support : ∀ (i: Fin 5), g^(i.val) • p ∈ Support α h' := by
intro i
rw [mem_support]
by_contra p_fixed
rw [<-mul_smul, h'_commutes.pow_right, mul_smul] at p_fixed
group_action at p_fixed
exact p_moves p_fixed
-- The next section gets tricky, so let us clear away some stuff first :3
clear h'_commutes h'_nontrivial
clear V₀_open x_in_V₀ V₀_in_support disjoint_img_V₀
clear V₁_open x_in_V₁
clear five_points h_in_ristV h_ne_one V_disjoint_smulImage
clear support_f₂_h
-- by the pigeonhole principle, one of the four sets V, f₁(V), f₂(V), f₁f₂(V) must contain two of these points,
-- say g^i(p),g^j(p) ∈ k(V) for some 0 ≤ i < j ≤ 4 and k ∈ {1,f₁,f₂,f₁f₂}
let pigeonhole : Fintype.card (Fin 5) > Fintype.card (Fin 2 × Fin 2) := by trivial
let choice_pred := fun (i : Fin 5) => (Set.mem_iUnion.mp (support_h' (gi_in_support i)))
let choice := fun (i : Fin 5) => (choice_pred i).choose
let ⟨i, _, j, _, i_ne_j, same_choice⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to
pigeonhole
(fun (i : Fin 5) _ => Finset.mem_univ (choice i))
let k := f₁^(choice i).1.val * f₂^(choice i).2.val
have same_k : f₁^(choice j).1.val * f₂^(choice j).2.val = k := by rw [<-same_choice]
have gi : g^i.val • p ∈ k •'' V := (choice_pred i).choose_spec
have gk : g^j.val • p ∈ k •'' V := by
have gk' := (choice_pred j).choose_spec
rw [same_k] at gk'
exact gk'
-- Since g^(j-i)(V) is disjoint from V and k commutes with g,
-- we know that g^(j− i)k(V) is disjoint from k(V),
-- which leads to a contradiction since g^i(p) and g^j(p) both lie in k(V).
have g_disjoint : Disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := by
apply smulImage_disjoint_subset (Set.inter_subset_right V₀ V₁)
group
group
rw [Set.image_id']
rw [smulImage_disjoint_inv_pow]
group
theorem AlgebraicCentralizerBasis.conj_mem' {S : Set G} (S_in_basis : S ∈ AlgebraicCentralizerBasis G) (g : G) :
apply disjoint_img_V₁
(MulAut.conj_order_iso g) S ∈ AlgebraicCentralizerBasis G :=
symm; exact i_ne_j
by
show (fun i => g * i * g⁻¹) '' S ∈ AlgebraicCentralizerBasis G
have k_commutes: Commute k g := by
exact conj_mem S_in_basis g
apply Commute.mul_left
· exact f₁_commutes.pow_left _
end AlgebraicCentralizer
· exact f₂_commutes.pow_left _
clear f₁_commutes f₂_commutes
have g_k_disjoint : Disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := by
repeat rw [mul_smulImage]
repeat rw [<-inv_pow]
repeat rw [k_commutes.symm.inv_left.pow_left]
repeat rw [<-mul_smulImage k]
repeat rw [inv_pow]
exact disjoint_smulImage k g_disjoint
apply Set.disjoint_left.mp g_k_disjoint
· rw [mem_inv_smulImage]
exact gi
· rw [mem_inv_smulImage]
exact gk
lemma remark_1_2 (f g : G) (h_disj : AlgebraicallyDisjoint f g): Commute f g := by
by_contra non_commute
let disj_elem := h_disj g non_commute
let nontrivial := disj_elem.comm_elem_nontrivial
rw [commutatorElement_eq_one_iff_commute.mpr disj_elem.snd_commute] at nontrivial
rw [commutatorElement_one_right] at nontrivial
tauto
end Rubin
end Rubin