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

Fix most issues with porting

Browse Source
main
Shad Amethyst 11 months ago
parent 80349c3496
commit a8c3cd1aa1
1 changed files with 216 additions and 189 deletions
Show Stats Download Patch File Download Diff File

405
Rubin.lean
Unescape View File

@ -31,94 +31,93 @@ theorem Rubin.GroupActionExt.smul_eq_smul_inv {G α : Type _} [Group G] [MulActi
by by
constructor constructor
· intro hyp · intro hyp
let this.1 := congr_arg ((· • ·) h⁻¹) hyp let res := congr_arg ((· • ·) h⁻¹) hyp
rw [← mul_smul, ← mul_smul, mul_left_inv, one_smul] at this simp at res
exact this rw [← mul_smul] at res
exact res
· intro hyp · intro hyp
let this.1 := congr_arg ((· • ·) h) hyp rw [<-hyp, mul_smul]
rw [← mul_smul, ← mul_assoc, mul_right_inv, one_mul] at this simp
exact this
#align smul_eq_smul Rubin.GroupActionExt.smul_eq_smul_inv #align smul_eq_smul Rubin.GroupActionExt.smul_eq_smul_inv
theorem Rubin.GroupActionExt.smul_succ {G α : Type _} (n : ℕ) [Group G] [MulAction G α] {g : G} theorem Rubin.GroupActionExt.smul_succ {G α : Type _} (n : ℕ) [Group G] [MulAction G α] {g : G}
{x : α} : g ^ n.succ • x = g • g ^ n • x := {x : α} : g ^ n.succ • x = g • g ^ n • x :=
by by
have := Tactic.Ring.pow_add_rev g 1 n rw [pow_succ, mul_smul]
rw [pow_one, ← Nat.succ_eq_one_add] at this
rw [← this, smul_smul]
#align smul_succ Rubin.GroupActionExt.smul_succ #align smul_succ Rubin.GroupActionExt.smul_succ
section GroupActionTactic section GroupActionTactic
namespace Tactic.Interactive -- namespace Tactic.Interactive
/- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/ -- /- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/
open Tactic -- open Tactic
/- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/ -- /- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/
open Tactic.SimpArgType Interactive Tactic.Group -- open Tactic.SimpArgType Interactive Tactic.Group
/-- Auxiliary tactic for the `group_action` tactic. Calls the simplifier only. -/ -- /-- Auxiliary tactic for the `group_action` tactic. Calls the simplifier only. -/
unsafe def aux_group_action (locat : Loc) : tactic Unit := -- unsafe def aux_group_action (locat : Loc) : tactic Unit :=
tactic.interactive.simp_core { failIfUnchanged := false } skip true -- tactic.interactive.simp_core { failIfUnchanged := false } skip true
[expr ``(Rubin.GroupActionExt.smul_smul'), expr ``(Rubin.GroupActionExt.smul_eq_smul_inv), -- [expr ``(Rubin.GroupActionExt.smul_smul'), expr ``(Rubin.GroupActionExt.smul_eq_smul_inv),
expr ``(Rubin.GroupActionExt.smul_succ), expr ``(one_smul), expr ``(commutatorElement_def), -- expr ``(Rubin.GroupActionExt.smul_succ), expr ``(one_smul), expr ``(commutatorElement_def),
expr ``(mul_one), expr ``(one_mul), expr ``(one_pow), expr ``(one_zpow), expr ``(sub_self), -- expr ``(mul_one), expr ``(one_mul), expr ``(one_pow), expr ``(one_zpow), expr ``(sub_self),
expr ``(add_neg_self), expr ``(neg_add_self), expr ``(neg_neg), expr ``(tsub_self), -- expr ``(add_neg_self), expr ``(neg_add_self), expr ``(neg_neg), expr ``(tsub_self),
expr ``(Int.ofNat_add), expr ``(Int.ofNat_mul), expr ``(Int.ofNat_zero), -- expr ``(Int.ofNat_add), expr ``(Int.ofNat_mul), expr ``(Int.ofNat_zero),
expr ``(Int.ofNat_one), expr ``(Int.ofNat_bit0), expr ``(Int.ofNat_bit1), -- expr ``(Int.ofNat_one), expr ``(Int.ofNat_bit0), expr ``(Int.ofNat_bit1),
expr ``(Int.mul_neg_eq_neg_mul_symm), expr ``(Int.neg_mul_eq_neg_mul_symm), -- expr ``(Int.mul_neg_eq_neg_mul_symm), expr ``(Int.neg_mul_eq_neg_mul_symm),
symm_expr ``(zpow_ofNat), symm_expr ``(zpow_neg_one), symm_expr ``(zpow_mul), -- symm_expr ``(zpow_ofNat), symm_expr ``(zpow_neg_one), symm_expr ``(zpow_mul),
symm_expr ``(zpow_add_one), symm_expr ``(zpow_one_add), symm_expr ``(zpow_add), -- symm_expr ``(zpow_add_one), symm_expr ``(zpow_one_add), symm_expr ``(zpow_add),
expr ``(mul_zpow_neg_one), expr ``(zpow_zero), expr ``(mul_zpow), symm_expr ``(mul_assoc), -- expr ``(mul_zpow_neg_one), expr ``(zpow_zero), expr ``(mul_zpow), symm_expr ``(mul_assoc),
expr ``(Mathlib.Tactic.Group.zpow_trick), expr ``(Mathlib.Tactic.Group.zpow_trick_one), -- expr ``(Mathlib.Tactic.Group.zpow_trick), expr ``(Mathlib.Tactic.Group.zpow_trick_one),
expr ``(Mathlib.Tactic.Group.zpow_trick_one'), expr ``(zpow_trick_sub), expr ``(mul_one), -- expr ``(Mathlib.Tactic.Group.zpow_trick_one'), expr ``(zpow_trick_sub), expr ``(mul_one),
expr ``(one_mul), expr ``(one_pow), expr ``(one_zpow), expr ``(sub_self), -- expr ``(one_mul), expr ``(one_pow), expr ``(one_zpow), expr ``(sub_self),
expr ``(add_neg_self), expr ``(neg_add_self), expr ``(neg_neg), expr ``(tsub_self), -- expr ``(add_neg_self), expr ``(neg_add_self), expr ``(neg_neg), expr ``(tsub_self),
expr ``(Int.ofNat_add), expr ``(Int.ofNat_mul), expr ``(Int.ofNat_zero), -- expr ``(Int.ofNat_add), expr ``(Int.ofNat_mul), expr ``(Int.ofNat_zero),
expr ``(Int.ofNat_one), expr ``(Int.ofNat_bit0), expr ``(Int.ofNat_bit1), -- expr ``(Int.ofNat_one), expr ``(Int.ofNat_bit0), expr ``(Int.ofNat_bit1),
expr ``(Int.mul_neg_eq_neg_mul_symm), expr ``(Int.neg_mul_eq_neg_mul_symm), -- expr ``(Int.mul_neg_eq_neg_mul_symm), expr ``(Int.neg_mul_eq_neg_mul_symm),
symm_expr ``(zpow_ofNat), symm_expr ``(zpow_neg_one), symm_expr ``(zpow_mul), -- symm_expr ``(zpow_ofNat), symm_expr ``(zpow_neg_one), symm_expr ``(zpow_mul),
symm_expr ``(zpow_add_one), symm_expr ``(zpow_one_add), symm_expr ``(zpow_add), -- symm_expr ``(zpow_add_one), symm_expr ``(zpow_one_add), symm_expr ``(zpow_add),
expr ``(mul_zpow_neg_one), expr ``(zpow_zero), expr ``(mul_zpow), symm_expr ``(mul_assoc), -- expr ``(mul_zpow_neg_one), expr ``(zpow_zero), expr ``(mul_zpow), symm_expr ``(mul_assoc),
expr ``(Mathlib.Tactic.Group.zpow_trick), expr ``(Mathlib.Tactic.Group.zpow_trick_one), -- expr ``(Mathlib.Tactic.Group.zpow_trick), expr ``(Mathlib.Tactic.Group.zpow_trick_one),
expr ``(Mathlib.Tactic.Group.zpow_trick_one'), expr ``(zpow_trick_sub), -- expr ``(Mathlib.Tactic.Group.zpow_trick_one'), expr ``(zpow_trick_sub),
expr ``(Tactic.Ring.horner)] -- expr ``(Tactic.Ring.horner)]
[] locat >> -- [] locat >>
skip -- skip
#align tactic.interactive.aux_group_action tactic.interactive.aux_group_action -- #align tactic.interactive.aux_group_action tactic.interactive.aux_group_action
/-- Tactic for normalizing expressions in group actions, without assuming -- /-- Tactic for normalizing expressions in group actions, without assuming
commutativity, using only the group axioms without any information about -- commutativity, using only the group axioms without any information about
which group is manipulated. -- which group is manipulated.
Example: -- Example:
```lean -- ```lean
example {G α : Type} [group G] [mul_action G α] (a b : G) (x y : α) (h : a • b • x = a • y) : b⁻¹ • y = x := -- example {G α : Type} [group G] [mul_action G α] (a b : G) (x y : α) (h : a • b • x = a • y) : b⁻¹ • y = x :=
begin -- begin
group_action at h, -- normalizes `h` which becomes `h : c = d` -- group_action at h, -- normalizes `h` which becomes `h : c = d`
rw ← h, -- the goal is now `a*d*d⁻¹ = a` -- rw ← h, -- the goal is now `a*d*d⁻¹ = a`
group_action -- which then normalized and closed -- group_action -- which then normalized and closed
end -- end
``` -- ```
-/ -- -/
unsafe def group_action (locat : parse location) : tactic Unit := do -- unsafe def group_action (locat : parse location) : tactic Unit := do
aux_group_action locat -- aux_group_action locat
repeat (andthen (aux_group₂ locat) (aux_group_action locat)) -- repeat (andthen (aux_group₂ locat) (aux_group_action locat))
#align tactic.interactive.group_action tactic.interactive.group_action -- #align tactic.interactive.group_action tactic.interactive.group_action
end Tactic.Interactive -- end Tactic.Interactive
add_tactic_doc -- add_tactic_doc
{ Name := "group_action" -- { Name := "group_action"
category := DocCategory.tactic -- category := DocCategory.tactic
declNames := [`tactic.interactive.group_action] -- declNames := [`tactic.interactive.group_action]
tags := ["decision procedure", "simplification"] } -- tags := ["decision procedure", "simplification"] }
end GroupActionTactic -- end GroupActionTactic
/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/ /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/
example (G α : Type _) [Group G] (a b c : G) [MulAction G α] (x : α) : example (G α : Type _) [Group G] (a b c : G) [MulAction G α] (x : α) :
⁅a * b, c⁆ • x = (a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆) • x := by ⁅a * b, c⁆ • x = (a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆) • x := by
sorry
trace trace
"./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]" "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]"
@ -135,7 +134,7 @@ theorem Rubin.equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x
theorem Rubin.GroupActionExt.subgroup_mk_smul {G α : Type _} [Group G] [MulAction G α] theorem Rubin.GroupActionExt.subgroup_mk_smul {G α : Type _} [Group G] [MulAction G α]
{S : Subgroup G} {g : G} (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a := {S : Subgroup G} {g : G} (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a :=
rfl rfl
#align subgroup.mk_smul Rubin.GroupActionExt.subgroup_mk_smul #align Subgroup.mk_smul Rubin.GroupActionExt.subgroup_mk_smul
#align add_subgroup.mk_vadd AddSubgroup.mk_vadd #align add_subgroup.mk_vadd AddSubgroup.mk_vadd
---------------------------------------------------------------- ----------------------------------------------------------------
@ -171,12 +170,12 @@ theorem Rubin.orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
constructor constructor
· rintro ⟨⟨_, g_bot⟩, g_to_x⟩ · rintro ⟨⟨_, g_bot⟩, g_to_x⟩
rw [← g_to_x, Set.mem_singleton_iff, Rubin.GroupActionExt.subgroup_mk_smul] rw [← g_to_x, Set.mem_singleton_iff, Rubin.GroupActionExt.subgroup_mk_smul]
exact (subgroup.mem_bot.mp g_bot).symm ▸ one_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⟩ exact fun h => ⟨1, Eq.trans (one_smul _ p) (Set.mem_singleton_iff.mp h).symm⟩
#align orbit_bot Rubin.orbit_bot #align orbit_bot Rubin.orbit_bot
-------------------------------- --------------------------------
section Smul'' section SmulImage
theorem Rubin.GroupActionExt.smul_congr (g : G) {x y : α} (h : x = y) : g • x = g • y := theorem Rubin.GroupActionExt.smul_congr (g : G) {x y : α} (h : x = y) : g • x = g • y :=
congr_arg ((· • ·) g) h congr_arg ((· • ·) g) h
@ -189,9 +188,10 @@ theorem Rubin.GroupActionExt.smul_eq_iff_inv_smul_eq {x : α} {g : G} : g • x
theorem Rubin.GroupActionExt.smul_pow_eq_of_smul_eq {x : α} {g : G} (n : ℕ) : theorem Rubin.GroupActionExt.smul_pow_eq_of_smul_eq {x : α} {g : G} (n : ℕ) :
g • x = x → g ^ n • x = x := by g • x = x → g ^ n • x = x := by
induction n induction n with
simp only [pow_zero, one_smul, eq_self_iff_true, imp_true_iff] | zero => simp only [pow_zero, one_smul, eq_self_iff_true, imp_true_iff]
· intro h | succ n n_ih =>
intro h
nth_rw 2 [← (Rubin.GroupActionExt.smul_congr g (n_ih h)).trans h] nth_rw 2 [← (Rubin.GroupActionExt.smul_congr g (n_ih h)).trans h]
rw [← mul_smul, ← pow_succ] rw [← mul_smul, ← pow_succ]
#align smul_pow_eq_of_smul_eq Rubin.GroupActionExt.smul_pow_eq_of_smul_eq #align smul_pow_eq_of_smul_eq Rubin.GroupActionExt.smul_pow_eq_of_smul_eq
@ -199,12 +199,14 @@ theorem Rubin.GroupActionExt.smul_pow_eq_of_smul_eq {x : α} {g : G} (n : ℕ) :
theorem Rubin.GroupActionExt.smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) : theorem Rubin.GroupActionExt.smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) :
g • x = x → g ^ n • x = x := by g • x = x → g ^ n • x = x := by
intro h intro h
cases n cases n with
· let this.1 := Rubin.GroupActionExt.smul_pow_eq_of_smul_eq n h; finish | ofNat n => let res := Rubin.GroupActionExt.smul_pow_eq_of_smul_eq n h; simp; exact res
· | negSucc n =>
let this.1 := let res :=
smul_eq_iff_inv_smul_eq.mp (Rubin.GroupActionExt.smul_pow_eq_of_smul_eq (1 + n) h); smul_eq_iff_inv_smul_eq.mp (Rubin.GroupActionExt.smul_pow_eq_of_smul_eq (1 + n) h);
finish simp
rw [add_comm]
exact res
#align smul_zpow_eq_of_smul_eq Rubin.GroupActionExt.smul_zpow_eq_of_smul_eq #align smul_zpow_eq_of_smul_eq Rubin.GroupActionExt.smul_zpow_eq_of_smul_eq
def Rubin.GroupActionExt.is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α] def Rubin.GroupActionExt.is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
@ -238,7 +240,7 @@ theorem Rubin.SmulImage.mem_smulImage {x : α} {g : G} {U : Set α} : x ∈ g•
let ygx : y = g⁻¹ • x := inv_smul_smul g y ▸ Rubin.GroupActionExt.smul_congr g⁻¹ gyx let ygx : y = g⁻¹ • x := inv_smul_smul g y ▸ Rubin.GroupActionExt.smul_congr g⁻¹ gyx
exact ygx ▸ yU exact ygx ▸ yU
· intro h · intro h
use⟨g⁻¹ • x, set.mem_preimage.mp h, smul_inv_smul g x⟩ exact ⟨g⁻¹ • x, ⟨Set.mem_preimage.mp h, smul_inv_smul g x⟩⟩
#align mem_smul'' Rubin.SmulImage.mem_smulImage #align mem_smul'' Rubin.SmulImage.mem_smulImage
theorem Rubin.SmulImage.mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹•''U ↔ g • x ∈ U := theorem Rubin.SmulImage.mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹•''U ↔ g • x ∈ U :=
@ -275,7 +277,7 @@ theorem Rubin.SmulImage.disjoint_smulImage (g : G) {U V : Set α} :
rw [Set.disjoint_left] at disjoint_U_V rw [Set.disjoint_left] at disjoint_U_V
intro x x_in_gU intro x x_in_gU
by_contra h by_contra h
exact (disjoint_U_V (mem_smul''.mp x_in_gU)) (mem_smul''.mp h) exact (disjoint_U_V (mem_smulImage.mp x_in_gU)) (mem_smulImage.mp h)
#align disjoint_smul'' Rubin.SmulImage.disjoint_smulImage #align disjoint_smul'' Rubin.SmulImage.disjoint_smulImage
-- TODO: check if this is actually needed -- TODO: check if this is actually needed
@ -308,15 +310,15 @@ theorem Rubin.SmulImage.smulImage_eq_inv_preimage {g : G} {U : Set α} : g•''U
by by
ext ext
constructor constructor
· intro h; rw [Set.mem_preimage]; exact mem_smul''.mp h · intro h; rw [Set.mem_preimage]; exact mem_smulImage.mp h
· intro h; rw [Rubin.SmulImage.mem_smulImage]; exact set.mem_preimage.mp h · intro h; rw [Rubin.SmulImage.mem_smulImage]; exact Set.mem_preimage.mp h
#align smul''_eq_inv_preimage Rubin.SmulImage.smulImage_eq_inv_preimage #align smul''_eq_inv_preimage Rubin.SmulImage.smulImage_eq_inv_preimage
theorem Rubin.SmulImage.smulImage_eq_of_smul_eq {g h : G} {U : Set α} : theorem Rubin.SmulImage.smulImage_eq_of_smul_eq {g h : G} {U : Set α} :
(∀ x ∈ U, g • x = h • x) → g•''U = h•''U := (∀ x ∈ U, g • x = h • x) → g•''U = h•''U :=
by by
intro hU intro hU
ext ext x
rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage] rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage]
constructor constructor
· intro k; let a := congr_arg ((· • ·) h⁻¹) (hU (g⁻¹ • x) k); · intro k; let a := congr_arg ((· • ·) h⁻¹) (hU (g⁻¹ • x) k);
@ -325,10 +327,10 @@ theorem Rubin.SmulImage.smulImage_eq_of_smul_eq {g h : G} {U : Set α} :
simp only [smul_inv_smul, inv_smul_smul] at a ; exact Set.mem_of_eq_of_mem a.symm k simp only [smul_inv_smul, inv_smul_smul] at a ; exact Set.mem_of_eq_of_mem a.symm k
#align smul''_eq_of_smul_eq Rubin.SmulImage.smulImage_eq_of_smul_eq #align smul''_eq_of_smul_eq Rubin.SmulImage.smulImage_eq_of_smul_eq
end Smul'' end SmulImage
-------------------------------- --------------------------------
section Rubin.SmulSupport.Support section Support
def Rubin.SmulSupport.Support (α : Type _) [MulAction G α] (g : G) := def Rubin.SmulSupport.Support (α : Type _) [MulAction G α] (g : G) :=
{x : α | g • x ≠ x} {x : α | g • x ≠ x}
@ -371,8 +373,8 @@ theorem Rubin.SmulSupport.fixed_smulImage_in_support (g : G) {U : Set α} :
cases' @or_not (x ∈ Rubin.SmulSupport.Support α g) with xmoved xfixed cases' @or_not (x ∈ Rubin.SmulSupport.Support α g) with xmoved xfixed
exact exact
⟨fun _ => support_in_U xmoved, fun _ => ⟨fun _ => support_in_U xmoved, fun _ =>
mem_smul''.mpr (support_in_U (Rubin.SmulSupport.inv_smul_mem_support xmoved))⟩ SmulImage.mem_smulImage.mpr (support_in_U (Rubin.SmulSupport.inv_smul_mem_support xmoved))⟩
rw [Rubin.SmulImage.mem_smulImage, smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp xfixed)] rw [Rubin.SmulImage.mem_smulImage, GroupActionExt.smul_eq_iff_inv_smul_eq.mp (not_mem_support.mp xfixed)]
#align fixes_subset_within_support Rubin.SmulSupport.fixed_smulImage_in_support #align fixes_subset_within_support Rubin.SmulSupport.fixed_smulImage_in_support
theorem Rubin.SmulSupport.smulImage_subset_in_support (g : G) (U V : Set α) : theorem Rubin.SmulSupport.smulImage_subset_in_support (g : G) (U V : Set α) :
@ -387,17 +389,18 @@ theorem Rubin.SmulSupport.support_mul (g h : G) (α : Type _) [MulAction G α] :
by by
intro x x_in_support intro x x_in_support
by_contra h_support by_contra h_support
let this.1 := not_or_distrib.mp h_support
let res := not_or.mp h_support
exact exact
x_in_support x_in_support
((mul_smul g h x).trans ((mul_smul g h x).trans
((congr_arg ((· • ·) g) (mem_not_support.mp this.2)).trans <| mem_not_support.mp this.1)) ((congr_arg ((· • ·) g) (not_mem_support.mp res.2)).trans <| not_mem_support.mp res.1))
#align support_mul Rubin.SmulSupport.support_mul #align support_mul Rubin.SmulSupport.support_mul
theorem Rubin.SmulSupport.support_conjugate (α : Type _) [MulAction G α] (g h : G) : theorem Rubin.SmulSupport.support_conjugate (α : Type _) [MulAction G α] (g h : G) :
Rubin.SmulSupport.Support α (h * g * h⁻¹) = h•''Rubin.SmulSupport.Support α g := Rubin.SmulSupport.Support α (h * g * h⁻¹) = h•''Rubin.SmulSupport.Support α g :=
by by
ext ext x
rw [Rubin.SmulSupport.mem_support, Rubin.SmulImage.mem_smulImage, Rubin.SmulSupport.mem_support, rw [Rubin.SmulSupport.mem_support, Rubin.SmulImage.mem_smulImage, Rubin.SmulSupport.mem_support,
mul_smul, mul_smul] mul_smul, mul_smul]
constructor constructor
@ -408,11 +411,11 @@ theorem Rubin.SmulSupport.support_conjugate (α : Type _) [MulAction G α] (g h
theorem Rubin.SmulSupport.support_inv (α : Type _) [MulAction G α] (g : G) : theorem Rubin.SmulSupport.support_inv (α : Type _) [MulAction G α] (g : G) :
Rubin.SmulSupport.Support α g⁻¹ = Rubin.SmulSupport.Support α g := Rubin.SmulSupport.Support α g⁻¹ = Rubin.SmulSupport.Support α g :=
by by
ext ext x
rw [Rubin.SmulSupport.mem_support, Rubin.SmulSupport.mem_support] rw [Rubin.SmulSupport.mem_support, Rubin.SmulSupport.mem_support]
constructor constructor
· intro h1; by_contra h2; exact h1 (smul_eq_iff_inv_smul_eq.mp h2) · intro h1; by_contra h2; exact h1 (GroupActionExt.smul_eq_iff_inv_smul_eq.mp h2)
· intro h1; by_contra h2; exact h1 (smul_eq_iff_inv_smul_eq.mpr h2) · intro h1; by_contra h2; exact h1 (GroupActionExt.smul_eq_iff_inv_smul_eq.mpr h2)
#align support_inv Rubin.SmulSupport.support_inv #align support_inv Rubin.SmulSupport.support_inv
theorem Rubin.SmulSupport.support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) : theorem Rubin.SmulSupport.support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) :
@ -421,10 +424,12 @@ theorem Rubin.SmulSupport.support_pow (α : Type _) [MulAction G α] (g : G) (j
intro x xmoved intro x xmoved
by_contra xfixed by_contra xfixed
rw [Rubin.SmulSupport.mem_support] at xmoved rw [Rubin.SmulSupport.mem_support] at xmoved
induction j induction j with
· apply xmoved; rw [pow_zero g, one_smul] | zero => apply xmoved; rw [pow_zero g, one_smul]
· apply xmoved | succ j j_ih =>
let j_ih := (congr_arg ((· • ·) g) (not_not.mp j_ih)).trans (mem_not_support.mp xfixed) apply xmoved
let j_ih := (congr_arg ((· • ·) g) (not_not.mp j_ih)).trans (not_mem_support.mp xfixed)
simp at j_ih
rw [← mul_smul, ← pow_succ] at j_ih rw [← mul_smul, ← pow_succ] at j_ih
exact j_ih exact j_ih
#align support_pow Rubin.SmulSupport.support_pow #align support_pow Rubin.SmulSupport.support_pow
@ -438,9 +443,9 @@ theorem Rubin.SmulSupport.support_comm (α : Type _) [MulAction G α] (g h : G)
rw [Set.mem_union] at all_fixed rw [Set.mem_union] at all_fixed
cases' @or_not (h • x = x) with xfixed xmoved cases' @or_not (h • x = x) with xfixed xmoved
· rw [Rubin.SmulSupport.mem_support, Rubin.bracket_mul, mul_smul, · rw [Rubin.SmulSupport.mem_support, Rubin.bracket_mul, mul_smul,
smul_eq_iff_inv_smul_eq.mp xfixed, ← Rubin.SmulSupport.mem_support] at x_in_support GroupActionExt.smul_eq_iff_inv_smul_eq.mp xfixed, ← Rubin.SmulSupport.mem_support] at x_in_support
exact exact
((Rubin.SmulSupport.support_conjugate α h g).symm ▸ (not_or_distrib.mp all_fixed).2) ((Rubin.SmulSupport.support_conjugate α h g).symm ▸ (not_or.mp all_fixed).2)
x_in_support x_in_support
· exact all_fixed (Or.inl xmoved) · exact all_fixed (Or.inl xmoved)
#align support_comm Rubin.SmulSupport.support_comm #align support_comm Rubin.SmulSupport.support_comm
@ -457,11 +462,14 @@ theorem Rubin.SmulSupport.disjoint_support_comm (f g : G) {U : Set α} :
(congr_arg ((· • ·) f) (congr_arg ((· • ·) f)
(Rubin.SmulSupport.fixed_of_disjoint x_in_U (Rubin.SmulSupport.fixed_of_disjoint x_in_U
(Set.disjoint_of_subset_right support_conj disjoint_U))).symm (Set.disjoint_of_subset_right support_conj disjoint_U))).symm
rw [← mul_smul, ← mul_assoc, ← mul_assoc] at goal simp at goal
exact goal.symm sorry
-- rw [mul_smul, mul_smul] at goal
-- exact goal.symm
#align disjoint_support_comm Rubin.SmulSupport.disjoint_support_comm #align disjoint_support_comm Rubin.SmulSupport.disjoint_support_comm
end Rubin.SmulSupport.Support end Support
-- comment by Cedric: would be nicer to define just a subset, and then show it is a subgroup -- comment by Cedric: would be nicer to define just a subset, and then show it is a subgroup
def rigidStabilizer' (G : Type _) [Group G] [MulAction G α] (U : Set α) : Set G := def rigidStabilizer' (G : Type _) [Group G] [MulAction G α] (U : Set α) : Set G :=
@ -499,12 +507,12 @@ variable [TopologicalSpace α] [TopologicalSpace β]
class Rubin.Topological.ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends class Rubin.Topological.ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends
MulAction G α where MulAction G α where
Continuous : ∀ g : G, Continuous (@SMul.smul G α _ g) continuous : ∀ g : G, Continuous (@SMul.smul G α _ g)
#align continuous_mul_action Rubin.Topological.ContinuousMulAction #align continuous_mul_action Rubin.Topological.ContinuousMulAction
structure Rubin.Topological.equivariant_homeomorph (G α β : Type _) [Group G] [TopologicalSpace α] structure Rubin.Topological.equivariant_homeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
[TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where [TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where
equivariant : Rubin.GroupActionExt.is_equivariant G to_fun equivariant : GroupActionExt.is_equivariant G toFun
#align equivariant_homeomorph Rubin.Topological.equivariant_homeomorph #align equivariant_homeomorph Rubin.Topological.equivariant_homeomorph
theorem Rubin.Topological.equivariant_fun [MulAction G α] [MulAction G β] theorem Rubin.Topological.equivariant_fun [MulAction G α] [MulAction G β]
@ -518,9 +526,10 @@ theorem Rubin.Topological.equivariant_inv [MulAction G α] [MulAction G β]
Rubin.GroupActionExt.is_equivariant G h.invFun := Rubin.GroupActionExt.is_equivariant G h.invFun :=
by by
intro g x intro g x
let e := congr_arg h.inv_fun (h.equivariant g (h.inv_fun x)) symm
let e := congr_arg h.invFun (h.equivariant g (h.invFun x))
rw [h.left_inv _, h.right_inv _] at e rw [h.left_inv _, h.right_inv _] at e
exact e.symm exact e
#align equivariant_inv Rubin.Topological.equivariant_inv #align equivariant_inv Rubin.Topological.equivariant_inv
variable [Rubin.Topological.ContinuousMulAction G α] variable [Rubin.Topological.ContinuousMulAction G α]
@ -535,15 +544,18 @@ theorem Rubin.Topological.img_open_open (g : G) (U : Set α) (h : IsOpen U)
theorem Rubin.Topological.support_open (g : G) [TopologicalSpace α] [T2Space α] theorem Rubin.Topological.support_open (g : G) [TopologicalSpace α] [T2Space α]
[Rubin.Topological.ContinuousMulAction G α] : IsOpen (Rubin.SmulSupport.Support α g) := [Rubin.Topological.ContinuousMulAction G α] : IsOpen (Rubin.SmulSupport.Support α g) :=
by by
apply is_open_iff_forall_mem_open.mpr apply isOpen_iff_forall_mem_open.mpr
intro x xmoved intro x xmoved
rcases T2Space.t2 (g • x) x xmoved with ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩ rcases T2Space.t2 (g • x) x xmoved with ⟨U, V, open_U, open_V, gx_in_U, x_in_V, disjoint_U_V⟩
exact exact
⟨V ∩ (g⁻¹•''U), fun y yW => ⟨V ∩ (g⁻¹•''U), fun y yW =>
@Disjoint.ne_of_mem α U V disjoint_U_V (g • y) y -- TODO: don't use @-notation here
(mem_inv_smul''.mp (Set.mem_of_mem_inter_right yW)) (Set.mem_of_mem_inter_left yW), @Disjoint.ne_of_mem α U V disjoint_U_V (g • y)
(SmulImage.mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW))
y
(Set.mem_of_mem_inter_left yW),
IsOpen.inter open_V (Rubin.Topological.img_open_open g⁻¹ U open_U), IsOpen.inter open_V (Rubin.Topological.img_open_open g⁻¹ U open_U),
⟨x_in_V, mem_inv_smul''.mpr gx_in_U⟩⟩ ⟨x_in_V, SmulImage.mem_inv_smulImage.mpr gx_in_U⟩⟩
#align support_open Rubin.Topological.support_open #align support_open Rubin.Topological.support_open
end TopologicalActions end TopologicalActions
@ -574,8 +586,9 @@ theorem Rubin.faithful_rigid_stabilizer_moves_point {g : G} {U : Set α} :
theorem Rubin.ne_one_support_nonempty {g : G} : g ≠ 1 → (Rubin.SmulSupport.Support α g).Nonempty := theorem Rubin.ne_one_support_nonempty {g : G} : g ≠ 1 → (Rubin.SmulSupport.Support α g).Nonempty :=
by by
intro h1 intro h1
cases' Rubin.faithful_moves_point'₁ α h1 with x _ cases' Rubin.faithful_moves_point'₁ α h1 with x h
use x use x
exact h
#align ne_one_support_nempty Rubin.ne_one_support_nonempty #align ne_one_support_nempty Rubin.ne_one_support_nonempty
-- FIXME: somehow clashes with another definition -- FIXME: somehow clashes with another definition
@ -589,20 +602,23 @@ theorem Rubin.disjoint_commute₁ {f g : G} :
rw [Rubin.bracket_mul, mul_smul, mul_smul, mul_smul] rw [Rubin.bracket_mul, mul_smul, mul_smul, mul_smul]
cases' @or_not (x ∈ Rubin.SmulSupport.Support α f) with hfmoved hffixed cases' @or_not (x ∈ Rubin.SmulSupport.Support α f) with hfmoved hffixed
· ·
rw [smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp (set.disjoint_left.mp hdisjoint hfmoved)), rw [GroupActionExt.smul_eq_iff_inv_smul_eq.mp (SmulSupport.not_mem_support.mp (Set.disjoint_left.mp hdisjoint hfmoved)),
mem_not_support.mp SmulSupport.not_mem_support.mp
(set.disjoint_left.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hfmoved)), (Set.disjoint_left.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hfmoved)),
smul_inv_smul] smul_inv_smul]
cases' @or_not (x ∈ Rubin.SmulSupport.Support α g) with hgmoved hgfixed cases' @or_not (x ∈ Rubin.SmulSupport.Support α g) with hgmoved hgfixed
· ·
rw [smul_eq_iff_inv_smul_eq.mp rw [GroupActionExt.smul_eq_iff_inv_smul_eq.mp
(mem_not_support.mp <| (SmulSupport.not_mem_support.mp <|
set.disjoint_right.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hgmoved)), Set.disjoint_right.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hgmoved)),
smul_inv_smul, mem_not_support.mp hffixed] smul_inv_smul, SmulSupport.not_mem_support.mp hffixed]
· ·
rw [smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp hgfixed), rw [
smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp hffixed), mem_not_support.mp hgfixed, GroupActionExt.smul_eq_iff_inv_smul_eq.mp (SmulSupport.not_mem_support.mp hgfixed),
mem_not_support.mp hffixed] GroupActionExt.smul_eq_iff_inv_smul_eq.mp (SmulSupport.not_mem_support.mp hffixed),
SmulSupport.not_mem_support.mp hgfixed,
SmulSupport.not_mem_support.mp hffixed
]
#align disjoint_commute Rubin.disjoint_commute₁ #align disjoint_commute Rubin.disjoint_commute₁
end FaithfulActions end FaithfulActions
@ -613,7 +629,7 @@ section RubinActions
variable [TopologicalSpace α] [TopologicalSpace β] variable [TopologicalSpace α] [TopologicalSpace β]
def Rubin.has_no_isolated_points (α : Type _) [TopologicalSpace α] := def Rubin.has_no_isolated_points (α : Type _) [TopologicalSpace α] :=
∀ x : α, (nhdsWithin x ({x}ᶜ)).ne_bot ∀ x : α, (nhdsWithin x ({x}ᶜ)) ≠ ⊥
#align has_no_isolated_points Rubin.has_no_isolated_points #align has_no_isolated_points Rubin.has_no_isolated_points
def Rubin.is_locally_dense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] := def Rubin.is_locally_dense (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α] :=
@ -644,8 +660,8 @@ theorem Rubin.Period.period_le_fix {p : α} {g : G} {m : ℕ} (m_pos : m > 0)
by by
constructor constructor
· by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith; · by_contra h'; have period_zero : Rubin.Period.period p g = 0; linarith;
rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩; linarith; rcases Nat.sInf_eq_zero.1 period_zero with ⟨cont, h_1⟩ | h; linarith;
exact set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩ exact Set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩
exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩ exact Nat.sInf_le ⟨m_pos, gmp_eq_p⟩
#align period_le_fix Rubin.Period.period_le_fix #align period_le_fix Rubin.Period.period_le_fix
@ -671,6 +687,7 @@ theorem Rubin.Period.period_neutral_eq_one (p : α) : Rubin.Period.period p (1 :
have : 0 < Rubin.Period.period p (1 : G) ∧ Rubin.Period.period p (1 : G) ≤ 1 := have : 0 < Rubin.Period.period p (1 : G) ∧ Rubin.Period.period p (1 : G) ≤ 1 :=
Rubin.Period.period_le_fix (by norm_num : 1 > 0) Rubin.Period.period_le_fix (by norm_num : 1 > 0)
(by (by
sorry
trace trace
"./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]" : "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]" :
(1 : G) ^ 1 • p = p) (1 : G) ^ 1 • p = p)
@ -683,19 +700,27 @@ def Rubin.Period.periods (U : Set α) (H : Subgroup G) : Set ℕ :=
/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/ /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/
-- TODO: split into multiple lemmas -- TODO: split into multiple lemmas
theorem Rubin.Period.periods_lemmas {U : Set α} (U_nonempty : U.Nonempty) {H : Subgroup G} theorem Rubin.Period.periods_lemmas {U : Set α} (U_nonempty : Set.Nonempty U) {H : Subgroup G}
(exp_ne_zero : Monoid.exponent H ≠ 0) : (exp_ne_zero : Monoid.exponent H ≠ 0) :
(Rubin.Period.periods U H).Nonempty ∧ (Rubin.Period.periods U H).Nonempty ∧
BddAbove (Rubin.Period.periods U H) ∧ BddAbove (Rubin.Period.periods U H) ∧
∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p := ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p :=
by by
rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩ rcases Monoid.exponentExists_iff_ne_zero.2 exp_ne_zero with ⟨m, m_pos, gm_eq_one⟩
have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by intro p g; rw [gm_eq_one g]; have gmp_eq_p : ∀ (p : α) (g : H), g ^ m • p = p := by
intro p g; rw [gm_eq_one g];
sorry
trace trace
"./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]" "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]"
have periods_nonempty : (Rubin.Period.periods U H).Nonempty := by use 1; let p := U_nonempty.some; have periods_nonempty : (Rubin.Period.periods U H).Nonempty := by
use p; exact Set.Nonempty.some_mem U_nonempty; use 1; exact Rubin.Period.period_neutral_eq_one p use 1;
have periods_bounded : BddAbove (Rubin.Period.periods U H) := by use m; intro some_period hperiod; let p := Set.Nonempty.some U_nonempty;
use p;
exact Set.Nonempty.some_mem U_nonempty;
use 1;
exact Rubin.Period.period_neutral_eq_one p
have periods_bounded : BddAbove (Rubin.Period.periods U H) := by
use m; intro some_period hperiod;
rcases hperiod with ⟨p, g, hperiod⟩; rw [← hperiod]; rcases hperiod with ⟨p, g, hperiod⟩; rw [← hperiod];
exact (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).2 exact (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).2
exact ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ exact ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
@ -709,9 +734,11 @@ theorem Rubin.Period.period_from_exponent (U : Set α) (U_nonempty : U.Nonempty)
rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with rcases Rubin.Period.periods_lemmas U_nonempty exp_ne_zero with
⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩
rcases Nat.sSup_mem periods_nonempty periods_bounded with ⟨p, g, hperiod⟩ rcases Nat.sSup_mem periods_nonempty periods_bounded with ⟨p, g, hperiod⟩
use p
use g
use sSup (Rubin.Period.periods U H)
exact exact
⟨p, g, Sup (Rubin.Period.periods U H), ⟨hperiod ▸ (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1, hperiod, rfl⟩
hperiod ▸ (Rubin.Period.period_le_fix m_pos (gmp_eq_p p g)).1, hperiod, rfl⟩
#align period_from_exponent Rubin.Period.period_from_exponent #align period_from_exponent Rubin.Period.period_from_exponent
theorem Rubin.Period.zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty) theorem Rubin.Period.zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.Nonempty)
@ -732,9 +759,9 @@ theorem Rubin.Period.zero_lt_period_le_Sup_periods {U : Set α} (U_nonempty : U.
theorem Rubin.Period.pow_period_fix (p : α) (g : G) : g ^ Rubin.Period.period p g • p = p := theorem Rubin.Period.pow_period_fix (p : α) (g : G) : g ^ Rubin.Period.period p g • p = p :=
by by
cases eq_zero_or_neZero (Rubin.Period.period p g) cases eq_zero_or_neZero (Rubin.Period.period p g) with
· rw [h]; finish | inl h => rw [h]; simp
· | inr h =>
exact exact
(Nat.sInf_mem (Nat.sInf_mem
(Nat.nonempty_of_pos_sInf (Nat.nonempty_of_pos_sInf
@ -769,9 +796,9 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- exact is_open.inter (img_open_open g⁻¹ V open_V) open_W, -- exact is_open.inter (img_open_open g⁻¹ V open_V) open_W,
-- split, -- split,
-- exact ⟨mem_inv_smul''.mpr gx_in_V,x_in_W⟩, -- exact ⟨mem_inv_smul''.mpr gx_in_V,x_in_W⟩,
-- exact set.disjoint_of_subset -- exact Set.disjoint_of_subset
-- (set.inter_subset_right (g⁻¹•''V) W) -- (Set.inter_subset_right (g⁻¹•''V) W)
-- (λ y hy, smul_inv_smul g y ▸ mem_inv_smul''.mp (set.mem_of_mem_inter_left (mem_smul''.mp hy)) : g•''U ⊆ V) -- (λ y hy, smul_inv_smul g y ▸ mem_inv_smul''.mp (Set.mem_of_mem_inter_left (mem_smulImage.mp hy)) : g•''U ⊆ V)
-- disjoint_V_W.symm -- disjoint_V_W.symm
-- end -- end
-- lemma disjoint_nbhd_in {g : G} {x : α} [t2_space α] {V : set α} : is_open V → x ∈ V → g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ U ⊆ V ∧ disjoint U (g •'' U) := begin -- lemma disjoint_nbhd_in {g : G} {x : α} [t2_space α] {V : set α} : is_open V → x ∈ V → g • x ≠ x → ∃U : set α, is_open U ∧ x ∈ U ∧ U ⊆ V ∧ disjoint U (g •'' U) := begin
@ -784,15 +811,15 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- split, -- split,
-- exact ⟨x_in_W,x_in_V⟩, -- exact ⟨x_in_W,x_in_V⟩,
-- split, -- split,
-- exact set.inter_subset_right W V, -- exact Set.inter_subset_right W V,
-- exact set.disjoint_of_subset -- exact Set.disjoint_of_subset
-- (set.inter_subset_left W V) -- (Set.inter_subset_left W V)
-- ((@smul''_inter _ _ _ _ g W V).symm ▸ set.inter_subset_left (g•''W) (g•''V) : g•''U ⊆ g•''W) -- ((@smul''_inter _ _ _ _ g W V).symm ▸ Set.inter_subset_left (g•''W) (g•''V) : g•''U ⊆ g•''W)
-- disjoint_W -- disjoint_W
-- end -- end
-- 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)) := begin -- 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)) := begin
-- ext, -- ext,
-- simp only [set.mem_Union, set.mem_union], -- simp only [Set.mem_Union, Set.mem_union],
-- split, -- split,
-- { simp only [forall_exists_index], -- { simp only [forall_exists_index],
-- intro i, -- intro i,
@ -803,27 +830,27 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- intros disjoint_f_g h hfh, -- intros disjoint_f_g h hfh,
-- let support_f := support α f, -- let support_f := support α f,
-- -- h is not the identity on support α f -- -- h is not the identity on support α f
-- cases set.not_disjoint_iff.mp (mt (@disjoint_commute G α _ _ _ _ _) hfh) with x hx, -- cases Set.not_disjoint_iff.mp (mt (@disjoint_commute G α _ _ _ _ _) hfh) with x hx,
-- let x_in_support_f := hx.1, -- let x_in_support_f := hx.1,
-- let hx_ne_x := mem_support.mp hx.2, -- let hx_ne_x := mem_support.mp hx.2,
-- -- so since α is Hausdoff there is V nonempty ⊆ support α f with h•''V disjoint from V -- -- so since α is Hausdoff there is V nonempty ⊆ support α f with h•''V disjoint from V
-- rcases disjoint_nbhd_in (support_open f) x_in_support_f hx_ne_x with ⟨V,open_V,x_in_V,V_in_support,disjoint_img_V⟩, -- rcases disjoint_nbhd_in (support_open f) x_in_support_f hx_ne_x with ⟨V,open_V,x_in_V,V_in_support,disjoint_img_V⟩,
-- let ristV_ne_bot := locally_moving V open_V (set.nonempty_of_mem x_in_V), -- let ristV_ne_bot := locally_moving V open_V (Set.nonempty_of_mem x_in_V),
-- -- let f₂ be a nontrivial element of rigid_stabilizer G V -- -- let f₂ be a nontrivial element of rigid_stabilizer G V
-- rcases (or_iff_right ristV_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨f₂,f₂_in_ristV,f₂_ne_one⟩, -- rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨f₂,f₂_in_ristV,f₂_ne_one⟩,
-- -- again since α is Hausdorff there is W nonempty ⊆ V with f₂•''W disjoint from W -- -- again since α is Hausdorff there is W nonempty ⊆ V with f₂•''W disjoint from W
-- rcases faithful_moves_point' α f₂_ne_one with ⟨y,ymoved⟩, -- rcases faithful_moves_point' α f₂_ne_one with ⟨y,ymoved⟩,
-- let y_in_V : y ∈ V := (rist_supported_in_set f₂_in_ristV) (mem_support.mpr ymoved), -- let y_in_V : y ∈ V := (rist_supported_in_set f₂_in_ristV) (mem_support.mpr ymoved),
-- rcases disjoint_nbhd_in open_V y_in_V ymoved with ⟨W,open_W,y_in_W,W_in_V,disjoint_img_W⟩, -- rcases disjoint_nbhd_in open_V y_in_V ymoved with ⟨W,open_W,y_in_W,W_in_V,disjoint_img_W⟩,
-- -- let f₁ be a nontrivial element of rigid_stabilizer G W -- -- let f₁ be a nontrivial element of rigid_stabilizer G W
-- let ristW_ne_bot := locally_moving W open_W (set.nonempty_of_mem y_in_W), -- let ristW_ne_bot := locally_moving W open_W (Set.nonempty_of_mem y_in_W),
-- rcases (or_iff_right ristW_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨f₁,f₁_in_ristW,f₁_ne_one⟩, -- rcases (or_iff_right ristW_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨f₁,f₁_in_ristW,f₁_ne_one⟩,
-- use f₁, use f₂, -- use f₁, use f₂,
-- -- note that f₁,f₂ commute with g since their support is in support α f -- -- note that f₁,f₂ commute with g since their support is in support α f
-- split, -- split,
-- exact disjoint_commute (set.disjoint_of_subset_left (set.subset.trans (set.subset.trans (rist_supported_in_set f₁_in_ristW) W_in_V) V_in_support) disjoint_f_g), -- exact disjoint_commute (Set.disjoint_of_subset_left (Set.subset.trans (Set.subset.trans (rist_supported_in_set f₁_in_ristW) W_in_V) V_in_support) disjoint_f_g),
-- split, -- split,
-- exact disjoint_commute (set.disjoint_of_subset_left (set.subset.trans (rist_supported_in_set f₂_in_ristV) V_in_support) disjoint_f_g), -- exact disjoint_commute (Set.disjoint_of_subset_left (Set.subset.trans (rist_supported_in_set f₂_in_ristV) V_in_support) disjoint_f_g),
-- -- we claim that [f₁,[f₂,h]] is a nontrivial element of centralizer G g -- -- we claim that [f₁,[f₂,h]] is a nontrivial element of centralizer G g
-- let k := ⁅f₂,h⁆, -- let k := ⁅f₂,h⁆,
-- -- first, h*f₂⁻¹*h⁻¹ is supported on h V, so k := [f₂,h] agrees with f₂ on V -- -- first, h*f₂⁻¹*h⁻¹ is supported on h V, so k := [f₂,h] agrees with f₂ on V
@ -831,12 +858,12 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- (disjoint_support_comm f₂ h (rist_supported_in_set f₂_in_ristV) disjoint_img_V z (W_in_V z_in_W)).symm, -- (disjoint_support_comm f₂ h (rist_supported_in_set f₂_in_ristV) disjoint_img_V z (W_in_V z_in_W)).symm,
-- -- 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. -- -- 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.
-- have h3 : support α ⁅f₁,k⁆ ⊆ support α f := begin -- have h3 : support α ⁅f₁,k⁆ ⊆ support α f := begin
-- let := (support_comm α k f₁).trans (set.union_subset_union (rist_supported_in_set f₁_in_ristW) (smul''_subset k $ rist_supported_in_set f₁_in_ristW)), -- let := (support_comm α k f₁).trans (Set.union_subset_union (rist_supported_in_set f₁_in_ristW) (smul''_subset k $ rist_supported_in_set f₁_in_ristW)),
-- rw [← commutator_element_inv,support_inv,(smul''_eq_of_smul_eq h2).symm] at this, -- rw [← commutator_element_inv,support_inv,(smul''_eq_of_smul_eq h2).symm] at this,
-- exact (this.trans $ (set.union_subset_union W_in_V (moves_subset_within_support f₂ W V W_in_V $ rist_supported_in_set f₂_in_ristV)).trans $ eq.subset V.union_self).trans V_in_support -- exact (this.trans $ (Set.union_subset_union W_in_V (moves_subset_within_support f₂ W V W_in_V $ rist_supported_in_set f₂_in_ristV)).trans $ eq.subset V.union_self).trans V_in_support
-- end, -- end,
-- split, -- split,
-- exact disjoint_commute (set.disjoint_of_subset_left h3 disjoint_f_g), -- exact disjoint_commute (Set.disjoint_of_subset_left h3 disjoint_f_g),
-- -- finally, [f₁,k] agrees with f₁ on W, so is not the identity. -- -- finally, [f₁,k] agrees with f₁ on W, so is not the identity.
-- have h4 : ∀z ∈ W, ⁅f₁,k⁆•z = f₁•z := -- have h4 : ∀z ∈ W, ⁅f₁,k⁆•z = f₁•z :=
-- disjoint_support_comm f₁ k (rist_supported_in_set f₁_in_ristW) (smul''_eq_of_smul_eq h2 ▸ disjoint_img_W), -- disjoint_support_comm f₁ k (rist_supported_in_set f₁_in_ristW) (smul''_eq_of_smul_eq h2 ▸ disjoint_img_W),
@ -860,10 +887,10 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- split, -- split,
-- exact is_open_Inter (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.1), -- exact is_open_Inter (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.1),
-- split, -- split,
-- exact set.mem_Inter.mpr (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.2.1), -- exact Set.mem_Inter.mpr (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.2.1),
-- intros i j i_ne_j, -- intros i j i_ne_j,
-- let U_inc := set.Inter_subset (λ p : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some) ⟨⟨i,j⟩,i_ne_j⟩, -- let U_inc := Set.Inter_subset (λ p : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some) ⟨⟨i,j⟩,i_ne_j⟩,
-- let := (disjoint_smul'' (f j) (set.disjoint_of_subset U_inc (smul''_subset ((f j)⁻¹ * (f i)) U_inc) (disjoint_hyp i j i_ne_j).some_spec.2.2)).symm, -- let := (disjoint_smul'' (f j) (Set.disjoint_of_subset U_inc (smul''_subset ((f j)⁻¹ * (f i)) U_inc) (disjoint_hyp i j i_ne_j).some_spec.2.2)).symm,
-- simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this, -- simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this,
-- from this -- from this
-- end -- end
@ -904,7 +931,7 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this, -- rw [(zpow_coe_nat g k.nat_abs).symm, (int_to_nat k one_le_k).symm] at this,
-- exact this }, -- exact this },
-- have := moves_inj period_ge_n, -- have := moves_inj period_ge_n,
-- finish -- done
-- end -- end
-- lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin -- lemma moves_1234_of_moves_12 {g : G} {x : α} (xmoves : g^12 • x ≠ x) : function.injective (λi : fin 5, g^(i:ℤ) • x) := begin
-- apply moves_inj, -- apply moves_inj,
@ -925,21 +952,21 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- -- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty -- -- suppose to the contrary that the set U = supp(f) ∩ supp(g^12) is nonempty
-- by_contra not_disjoint, -- by_contra not_disjoint,
-- let U := support α f ∩ support α (g^12), -- let U := support α f ∩ support α (g^12),
-- have U_nonempty : U.nonempty := set.not_disjoint_iff_nonempty_inter.mp not_disjoint, -- have U_nonempty : U.nonempty := Set.not_disjoint_iff_nonempty_inter.mp not_disjoint,
-- -- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint -- -- since X is Hausdorff, we can find a nonempty open set V ⊆ U such that f(V) is disjoint from V and the sets {g^i(V): i=0..4} are pairwise disjoint
-- let x := U_nonempty.some, -- let x := U_nonempty.some,
-- have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (set.inter_subset_right _ _) U_nonempty.some_mem), -- have five_points : function.injective (λi : fin 5, g^(i:ℤ) • x) := moves_1234_of_moves_12 (mem_support.mp $ (Set.inter_subset_right _ _) U_nonempty.some_mem),
-- rcases disjoint_nbhd_in (is_open.inter (support_open f) (support_open $ g^12)) U_nonempty.some_mem ((set.inter_subset_left _ _) U_nonempty.some_mem) with ⟨V₀,open_V₀,x_in_V₀,V₀_in_support,disjoint_img_V₀⟩, -- rcases disjoint_nbhd_in (is_open.inter (support_open f) (support_open $ g^12)) U_nonempty.some_mem ((Set.inter_subset_left _ _) U_nonempty.some_mem) with ⟨V₀,open_V₀,x_in_V₀,V₀_in_support,disjoint_img_V₀⟩,
-- rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩, -- rcases disjoint_nbhd_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩,
-- simp only at disjoint_img_V₁, -- simp only at disjoint_img_V₁,
-- let V := V₀ ∩ V₁, -- let V := V₀ ∩ V₁,
-- -- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V -- -- let h be a nontrivial element of rigid_stabilizer G V, and note that [f,h]≠1 since f(V) is disjoint from V
-- let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩), -- let ristV_ne_bot := locally_moving V (is_open.inter open_V₀ open_V₁) (Set.nonempty_of_mem ⟨x_in_V₀,x_in_V₁⟩),
-- rcases (or_iff_right ristV_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩, -- rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩,
-- have comm_non_trivial : ¬commute f h := begin -- have comm_non_trivial : ¬commute f h := begin
-- by_contra comm_trivial, -- by_contra comm_trivial,
-- rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩, -- rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨z,z_in_V,z_moved⟩,
-- let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (set.disjoint_of_subset (set.inter_subset_left V₀ V₁) (smul''_subset f (set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V, -- let act_comm := disjoint_support_comm h f (rist_supported_in_set h_in_ristV) (Set.disjoint_of_subset (Set.inter_subset_left V₀ V₁) (smul''_subset f (Set.inter_subset_left V₀ V₁)) disjoint_img_V₀) z z_in_V,
-- rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm, -- rw [commutator_element_eq_one_iff_commute.mpr comm_trivial.symm,one_smul] at act_comm,
-- exact z_moved act_comm.symm, -- exact z_moved act_comm.symm,
-- end, -- end,
@ -947,9 +974,9 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩, -- rcases alg_disjoint h comm_non_trivial with ⟨f₁,f₂,f₁_commutes,f₂_commutes,h'_commutes,h'_non_trivial⟩,
-- let h' := ⁅f₁,⁅f₂,h⁆⁆, -- let h' := ⁅f₁,⁅f₂,h⁆⁆,
-- -- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V) -- -- now observe that supp([f₂, h]) ⊆ V ∪ f₂(V), and by the same reasoning supp(h')⊆V∪f₁(V)∪f₂(V)∪f₁f₂(V)
-- have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV), -- have support_f₂h : support α ⁅f₂,h⁆ ⊆ V ∪ (f₂ •'' V) := (support_comm α f₂ h).trans (Set.union_subset_union (rist_supported_in_set h_in_ristV) $ smul''_subset f₂ $ rist_supported_in_set h_in_ristV),
-- have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin -- have support_h' : support α h' ⊆ ⋃(i : fin 2 × fin 2), (f₁^i.1.val*f₂^i.2.val) •'' V := begin
-- let this := (support_comm α f₁ ⁅f₂,h⁆).trans (set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)), -- let this := (support_comm α f₁ ⁅f₂,h⁆).trans (Set.union_subset_union support_f₂h (smul''_subset f₁ support_f₂h)),
-- rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this, -- rw [smul''_union,← one_smul'' V,← mul_smul'',← mul_smul'',← mul_smul'',mul_one,mul_one] at this,
-- let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V), -- let rw_u := rewrite_Union (λi : fin 2 × fin 2, (f₁^i.1.val*f₂^i.2.val) •'' V),
-- simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u, -- simp only [fin.val_eq_coe, fin.val_zero', pow_zero, mul_one, fin.val_one, pow_one, one_mul] at rw_u,
@ -967,20 +994,20 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- end, -- end,
-- -- 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₂} -- -- 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) := dec_trivial, -- let pigeonhole : fintype.card (fin 5) > fintype.card (fin 2 × fin 2) := dec_trivial,
-- let choice := λi : fin 5, (set.mem_Union.mp $ support_h' $ gi_in_support i).some, -- let choice := λi : fin 5, (Set.mem_Union.mp $ support_h' $ gi_in_support i).some,
-- rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩, -- rcases finset.exists_ne_map_eq_of_card_lt_of_maps_to pigeonhole (λ(i : fin 5) _, finset.mem_univ (choice i)) with ⟨i,_,j,_,i_ne_j,same_choice⟩,
-- clear h_1_w h_1_h_h_w pigeonhole, -- clear h_1_w h_1_h_h_w pigeonhole,
-- let k := f₁^(choice i).1.val*f₂^(choice i).2.val, -- 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 { simp only at same_choice, -- have same_k : f₁^(choice j).1.val*f₂^(choice j).2.val = k := by { simp only at same_choice,
-- rw ← same_choice }, -- rw ← same_choice },
-- have g_i : g^i.val • p ∈ k •'' V := (set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec, -- have g_i : g^i.val • p ∈ k •'' V := (Set.mem_Union.mp $ support_h' $ gi_in_support i).some_spec,
-- have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec, -- have g_j : g^j.val • p ∈ k •'' V := same_k ▸ (Set.mem_Union.mp $ support_h' $ gi_in_support j).some_spec,
-- -- but 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), a contradiction since g^i(p) and g^j(p) both lie in k(V). -- -- but 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), 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) := begin -- have g_disjoint : disjoint ((g^i.val)⁻¹ •'' V) ((g^j.val)⁻¹ •'' V) := begin
-- let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm, -- let := (disjoint_smul'' (g^(-(i.val+j.val : ℤ))) (disjoint_img_V₁ i j i_ne_j)).symm,
-- rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this, -- rw [← mul_smul'',← mul_smul'',← zpow_add,← zpow_add] at this,
-- simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this, -- simp only [fin.val_eq_coe, neg_add_rev, coe_coe, neg_add_cancel_right, zpow_neg, zpow_coe_nat, neg_add_cancel_comm] at this,
-- from set.disjoint_of_subset (smul''_subset _ (set.inter_subset_right V₀ V₁)) (smul''_subset _ (set.inter_subset_right V₀ V₁)) this -- from Set.disjoint_of_subset (smul''_subset _ (Set.inter_subset_right V₀ V₁)) (smul''_subset _ (Set.inter_subset_right V₀ V₁)) this
-- end, -- end,
-- have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val), -- have k_commutes : commute k g := commute.mul_left (f₁_commutes.pow_left (choice i).1.val) (f₂_commutes.pow_left (choice i).2.val),
-- have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin -- have g_k_disjoint : disjoint ((g^i.val)⁻¹ •'' (k •'' V)) ((g^j.val)⁻¹ •'' (k •'' V)) := begin
@ -991,7 +1018,7 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa
-- mul_smul'',inv_pow g i.val,mul_smul'' (g⁻¹^j.val) k V,inv_pow g j.val] at this, -- mul_smul'',inv_pow g i.val,mul_smul'' (g⁻¹^j.val) k V,inv_pow g j.val] at this,
-- from this -- from this
-- end, -- end,
-- exact set.disjoint_left.mp g_k_disjoint (mem_inv_smul''.mpr g_i) (mem_inv_smul''.mpr g_j) -- exact Set.disjoint_left.mp g_k_disjoint (mem_inv_smul''.mpr g_i) (mem_inv_smul''.mpr g_j)
-- end -- end
-- lemma remark_1_2 (f g : G) : is_algebraically_disjoint f g → commute f g := begin -- lemma remark_1_2 (f g : G) : is_algebraically_disjoint f g → commute f g := begin
-- intro alg_disjoint, -- intro alg_disjoint,
@ -1035,13 +1062,13 @@ theorem Rubin.RegularSupport.interiorClosure_mono {U V : Set α} :
interior_mono ∘ closure_mono interior_mono ∘ closure_mono
#align interior_closure_mono Rubin.RegularSupport.interiorClosure_mono #align interior_closure_mono Rubin.RegularSupport.interiorClosure_mono
def Rubin.RegularSupport.Set.is_regular_open (U : Set α) := def Set.is_regular_open (U : Set α) :=
Rubin.RegularSupport.InteriorClosure U = U Rubin.RegularSupport.InteriorClosure U = U
#align set.is_regular_open Rubin.RegularSupport.Set.is_regular_open #align Set.is_regular_open Set.is_regular_open
theorem Rubin.RegularSupport.Set.is_regular_def (U : Set α) : theorem Set.is_regular_def (U : Set α) :
U.is_regular_open ↔ Rubin.RegularSupport.InteriorClosure U = U := by rfl U.is_regular_open ↔ Rubin.RegularSupport.InteriorClosure U = U := by rfl
#align set.is_regular_def Rubin.RegularSupport.Set.is_regular_def #align Set.is_regular_def Set.is_regular_def
theorem Rubin.RegularSupport.IsOpen.in_closure {U : Set α} : IsOpen U → U ⊆ interior (closure U) := theorem Rubin.RegularSupport.IsOpen.in_closure {U : Set α} : IsOpen U → U ⊆ interior (closure U) :=
by by
@ -1059,7 +1086,7 @@ theorem Rubin.RegularSupport.IsOpen.interiorClosure_subset {U : Set α} :
theorem Rubin.RegularSupport.regular_interior_closure (U : Set α) : theorem Rubin.RegularSupport.regular_interior_closure (U : Set α) :
(Rubin.RegularSupport.InteriorClosure U).is_regular_open := (Rubin.RegularSupport.InteriorClosure U).is_regular_open :=
by by
rw [Rubin.RegularSupport.Set.is_regular_def] rw [Set.is_regular_def]
apply Set.Subset.antisymm apply Set.Subset.antisymm
exact interior_mono ((closure_mono interior_subset).trans (subset_of_eq closure_closure)) exact interior_mono ((closure_mono interior_subset).trans (subset_of_eq closure_closure))
exact (subset_of_eq interior_interior.symm).trans (interior_mono subset_closure) exact (subset_of_eq interior_interior.symm).trans (interior_mono subset_closure)
@ -1082,7 +1109,7 @@ theorem Rubin.RegularSupport.support_subset_regularSupport [T2Space α] (g : G)
theorem Rubin.RegularSupport.mem_regularSupport (g : G) (U : Set α) : theorem Rubin.RegularSupport.mem_regularSupport (g : G) (U : Set α) :
U.is_regular_open → g ∈ rigidStabilizer G U → Rubin.RegularSupport.RegularSupport α g ⊆ U := U.is_regular_open → g ∈ rigidStabilizer G U → Rubin.RegularSupport.RegularSupport α g ⊆ U :=
fun U_ro g_moves => fun U_ro g_moves =>
(Rubin.RegularSupport.Set.is_regular_def _).mp U_ro ▸ (Set.is_regular_def _).mp U_ro ▸
Rubin.RegularSupport.interiorClosure_mono (rist_supported_in_set g_moves) Rubin.RegularSupport.interiorClosure_mono (rist_supported_in_set g_moves)
#align mem_regular_support Rubin.RegularSupport.mem_regularSupport #align mem_regular_support Rubin.RegularSupport.mem_regularSupport
@ -1103,10 +1130,10 @@ end Rubin.RegularSupport.RegularSupport
-- ∀ (q : α) (hq : q ∈ V) (i : fin n), (i : ℕ) > 0 → g ^ (i : ℕ) • (q : α) ∉ V := -- ∀ (q : α) (hq : q ∈ V) (i : fin n), (i : ℕ) > 0 → g ^ (i : ℕ) • (q : α) ∉ V :=
-- begin -- begin
-- intros q hq i i_pos hcontra, -- intros q hq i i_pos hcontra,
-- have i_ne_zero : i ≠ (⟨ 0, n_pos ⟩ : fin n), { intro, finish }, -- have i_ne_zero : i ≠ (⟨ 0, n_pos ⟩ : fin n), { intro, done },
-- have hcontra' : g ^ (i : ℕ) • (q : α) ∈ g ^ (i : ℕ) •'' V, exact ⟨ q, hq, rfl ⟩, -- have hcontra' : g ^ (i : ℕ) • (q : α) ∈ g ^ (i : ℕ) •'' V, exact ⟨ q, hq, rfl ⟩,
-- have giq_notin_V := set.disjoint_left.mp (h_disj i (⟨ 0, n_pos ⟩ : fin n) i_ne_zero) hcontra', -- have giq_notin_V := Set.disjoint_left.mp (h_disj i (⟨ 0, n_pos ⟩ : fin n) i_ne_zero) hcontra',
-- exact ((by finish : g ^ 0•''V = V) ▸ giq_notin_V) hcontra -- exact ((by done : g ^ 0•''V = V) ▸ giq_notin_V) hcontra
-- end -- end
-- lemma moves_inj_period {g : G} {p : α} {n : ℕ} (period_eq_n : period p g = n) : function.injective (λ (i : fin n), g ^ (i : ℕ) • p) := begin -- lemma moves_inj_period {g : G} {p : α} {n : ℕ} (period_eq_n : period p g = n) : function.injective (λ (i : fin n), g ^ (i : ℕ) • p) := begin
-- have period_ge_n : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • p ≠ p, -- have period_ge_n : ∀ (k : ℕ), 1 ≤ k → k < n → g ^ k • p ≠ p,
@ -1126,17 +1153,17 @@ end Rubin.RegularSupport.RegularSupport
-- rcases disjoint_nbhd_fin (moves_inj_period hpgn) with ⟨ V', V'_open, p_in_V', disj' ⟩, -- rcases disjoint_nbhd_fin (moves_inj_period hpgn) with ⟨ V', V'_open, p_in_V', disj' ⟩,
-- dsimp at disj', -- dsimp at disj',
-- let V := U ∩ V', -- let V := U ∩ V',
-- have V_ss_U : V ⊆ U := set.inter_subset_left U V', -- have V_ss_U : V ⊆ U := Set.inter_subset_left U V',
-- have V'_ss_V : V ⊆ V' := set.inter_subset_right U V', -- have V'_ss_V : V ⊆ V' := Set.inter_subset_right U V',
-- have V_open : is_open V := is_open.inter U_open V'_open, -- have V_open : is_open V := is_open.inter U_open V'_open,
-- have p_in_V : (p : α) ∈ V := ⟨ subtype.mem p, p_in_V' ⟩, -- have p_in_V : (p : α) ∈ V := ⟨ subtype.mem p, p_in_V' ⟩,
-- have disj : ∀ (i j : fin n), ¬ i = j → disjoint (↑g ^ ↑i•''V) (↑g ^ ↑j•''V), -- have disj : ∀ (i j : fin n), ¬ i = j → disjoint (↑g ^ ↑i•''V) (↑g ^ ↑j•''V),
-- { intros i j i_ne_j W W_ss_giV W_ss_gjV, -- { intros i j i_ne_j W W_ss_giV W_ss_gjV,
-- exact disj' i j i_ne_j -- exact disj' i j i_ne_j
-- (set.subset.trans W_ss_giV (smul''_subset (↑g ^ ↑i) V'_ss_V)) -- (Set.subset.trans W_ss_giV (smul''_subset (↑g ^ ↑i) V'_ss_V))
-- (set.subset.trans W_ss_gjV (smul''_subset (↑g ^ ↑j) V'_ss_V)) }, -- (Set.subset.trans W_ss_gjV (smul''_subset (↑g ^ ↑j) V'_ss_V)) },
-- have ristV_ne_bot := locally_moving V V_open (set.nonempty_of_mem p_in_V), -- have ristV_ne_bot := locally_moving V V_open (Set.nonempty_of_mem p_in_V),
-- rcases (or_iff_right ristV_ne_bot).mp (subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩, -- rcases (or_iff_right ristV_ne_bot).mp (Subgroup.bot_or_exists_ne_one _) with ⟨h,h_in_ristV,h_ne_one⟩,
-- rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨ q, q_in_V, hq_ne_q ⟩, -- rcases faithful_rist_moves_point h_in_ristV h_ne_one with ⟨ q, q_in_V, hq_ne_q ⟩,
-- have hg_in_ristU : (h : G) * (g : G) ∈ rigid_stabilizer G U := (rigid_stabilizer G U).mul_mem' (rist_ss_rist V_ss_U h_in_ristV) (subtype.mem g), -- have hg_in_ristU : (h : G) * (g : G) ∈ rigid_stabilizer G U := (rigid_stabilizer G U).mul_mem' (rist_ss_rist V_ss_U h_in_ristV) (subtype.mem g),
-- have giq_notin_V : ∀ (i : fin n), (i : ℕ) > 0 → g ^ (i : ℕ) • (q : α) ∉ V := distinct_images_from_disjoint n_pos disj q q_in_V, -- have giq_notin_V : ∀ (i : fin n), (i : ℕ) > 0 → g ^ (i : ℕ) • (q : α) ∉ V := distinct_images_from_disjoint n_pos disj q q_in_V,

Write Preview
Loading…
Cancel
Save