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

🚚 Start moving more theorems in different files

Browse Source
pull/1/head
Shad Amethyst 12 months ago
parent 5fcca86b58
commit adc7194774
5 changed files with 459 additions and 368 deletions
Show Stats Download Patch File Download Diff File

385
Rubin.lean
Unescape View File

@ -17,19 +17,16 @@ import Mathlib.Topology.Separation
import Mathlib.Topology.Homeomorph
import Rubin.Tactic
import Rubin.MulActionExt
import Rubin.SmulImage
import Rubin.Support
#align_import rubin
namespace Rubin
open Rubin.Tactic
-- TODO: remove
--@[simp]
theorem GroupActionExt.smul_smul' {G α : Type _} [Group G] [MulAction G α] {g h : G} {x : α} :
g • h • x = (g * h) • x :=
smul_smul g h x
#align smul_smul' Rubin.GroupActionExt.smul_smul'
-- TODO: find a home
theorem equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y → e x ≠ e y :=
by
intro x_ne_y
@ -38,14 +35,6 @@ theorem equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y
convert congr_arg e.symm h <;> simp only [Equiv.symm_apply_apply]
#align equiv.congr_ne Rubin.equiv_congr_ne
-- this definitely should be added to mathlib!
@[simp, to_additive]
theorem 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 :=
rfl
#align Subgroup.mk_smul Rubin.GroupActionExt.subgroup_mk_smul
#align add_subgroup.mk_vadd AddSubgroup.mk_vadd
----------------------------------------------------------------
section Rubin
@ -54,9 +43,6 @@ variable {G α β : Type _} [Group G]
----------------------------------------------------------------
section Groups
theorem bracket_mul {f g : G} : ⁅f, g⁆ = f * g * f⁻¹ * g⁻¹ := by tauto
#align bracket_mul Rubin.bracket_mul
def is_algebraically_disjoint (f g : G) :=
∀ h : G,
¬Commute f h →
@ -78,308 +64,11 @@ theorem orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) :
rw [MulAction.mem_orbit_iff]
constructor
· 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, 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
--------------------------------
section SmulImage
theorem GroupActionExt.smul_congr (g : G) {x y : α} (h : x = y) : g • x = g • y :=
congr_arg ((· • ·) g) h
#align smul_congr Rubin.GroupActionExt.smul_congr
theorem GroupActionExt.smul_eq_iff_inv_smul_eq {x : α} {g : G} : g • x = x ↔ g⁻¹ • x = x :=
⟨fun h => (Rubin.GroupActionExt.smul_congr g⁻¹ h).symm.trans (inv_smul_smul g x), fun h =>
(Rubin.GroupActionExt.smul_congr g h).symm.trans (smul_inv_smul g x)⟩
#align smul_eq_iff_inv_smul_eq Rubin.GroupActionExt.smul_eq_iff_inv_smul_eq
theorem GroupActionExt.smul_pow_eq_of_smul_eq {x : α} {g : G} (n : ℕ) :
g • x = x → g ^ n • x = x := by
induction n with
| zero => simp only [pow_zero, one_smul, eq_self_iff_true, imp_true_iff]
| succ n n_ih =>
intro h
nth_rw 2 [← (Rubin.GroupActionExt.smul_congr g (n_ih h)).trans h]
rw [← mul_smul, ← pow_succ]
#align smul_pow_eq_of_smul_eq Rubin.GroupActionExt.smul_pow_eq_of_smul_eq
theorem GroupActionExt.smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) :
g • x = x → g ^ n • x = x := by
intro h
cases n with
| ofNat n => let res := Rubin.GroupActionExt.smul_pow_eq_of_smul_eq n h; simp; exact res
| negSucc n =>
let res :=
smul_eq_iff_inv_smul_eq.mp (Rubin.GroupActionExt.smul_pow_eq_of_smul_eq (1 + n) h);
simp
rw [add_comm]
exact res
#align smul_zpow_eq_of_smul_eq Rubin.GroupActionExt.smul_zpow_eq_of_smul_eq
def GroupActionExt.is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
[MulAction G β] (f : α → β) :=
∀ g : G, ∀ x : α, f (g • x) = g • f x
#align is_equivariant Rubin.GroupActionExt.is_equivariant
def SmulImage.smulImage' (g : G) (U : Set α) :=
{x | g⁻¹ • x ∈ U}
#align subset_img' Rubin.SmulImage.smulImage'
def SmulImage.smul_preimage' (g : G) (U : Set α) :=
{x | g • x ∈ U}
#align subset_preimg' Rubin.SmulImage.smul_preimage'
def SmulImage.SmulImage (g : G) (U : Set α) :=
(· • ·) g '' U
#align subset_img Rubin.SmulImage.SmulImage
infixl:60 "•''" => Rubin.SmulImage.SmulImage
theorem SmulImage.smulImage_def {g : G} {U : Set α} : g•''U = (· • ·) g '' U :=
rfl
#align subset_img_def Rubin.SmulImage.smulImage_def
theorem SmulImage.mem_smulImage {x : α} {g : G} {U : Set α} : x ∈ g•''U ↔ g⁻¹ • x ∈ U :=
by
rw [Rubin.SmulImage.smulImage_def, Set.mem_image ((· • ·) g) U x]
constructor
· rintro ⟨y, yU, gyx⟩
let ygx : y = g⁻¹ • x := inv_smul_smul g y ▸ Rubin.GroupActionExt.smul_congr g⁻¹ gyx
exact ygx ▸ yU
· intro h
exact ⟨g⁻¹ • x, ⟨Set.mem_preimage.mp h, smul_inv_smul g x⟩⟩
#align mem_smul'' Rubin.SmulImage.mem_smulImage
theorem SmulImage.mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹•''U ↔ g • x ∈ U :=
by
let msi := @Rubin.SmulImage.mem_smulImage _ _ _ _ x g⁻¹ U
rw [inv_inv] at msi
exact msi
#align mem_inv_smul'' Rubin.SmulImage.mem_inv_smulImage
theorem SmulImage.mul_smulImage (g h : G) (U : Set α) : g * h•''U = g•''(h•''U) :=
by
ext
rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage, ←
mul_smul, mul_inv_rev]
#align mul_smul'' Rubin.SmulImage.mul_smulImage
@[simp]
theorem SmulImage.smulImage_smulImage {g h : G} {U : Set α} : g•''(h•''U) = g * h•''U :=
(Rubin.SmulImage.mul_smulImage g h U).symm
#align smul''_smul'' Rubin.SmulImage.smulImage_smulImage
@[simp]
theorem SmulImage.one_smulImage (U : Set α) : (1 : G)•''U = U :=
by
ext
rw [Rubin.SmulImage.mem_smulImage, inv_one, one_smul]
#align one_smul'' Rubin.SmulImage.one_smulImage
theorem SmulImage.disjoint_smulImage (g : G) {U V : Set α} :
Disjoint U V → Disjoint (g•''U) (g•''V) :=
by
intro disjoint_U_V
rw [Set.disjoint_left]
rw [Set.disjoint_left] at disjoint_U_V
intro x x_in_gU
by_contra h
exact (disjoint_U_V (mem_smulImage.mp x_in_gU)) (mem_smulImage.mp h)
#align disjoint_smul'' Rubin.SmulImage.disjoint_smulImage
-- TODO: check if this is actually needed
theorem SmulImage.smulImage_congr (g : G) {U V : Set α} : U = V → g•''U = g•''V :=
congr_arg fun W : Set α => g•''W
#align smul''_congr Rubin.SmulImage.smulImage_congr
theorem SmulImage.smulImage_subset (g : G) {U V : Set α} : U ⊆ V → g•''U ⊆ g•''V :=
by
intro h1 x
rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage]
exact fun h2 => h1 h2
#align smul''_subset Rubin.SmulImage.smulImage_subset
theorem SmulImage.smulImage_union (g : G) {U V : Set α} : g•''U ∪ V = (g•''U) ∪ (g•''V) :=
by
ext
rw [Rubin.SmulImage.mem_smulImage, Set.mem_union, Set.mem_union, Rubin.SmulImage.mem_smulImage,
Rubin.SmulImage.mem_smulImage]
#align smul''_union Rubin.SmulImage.smulImage_union
theorem SmulImage.smulImage_inter (g : G) {U V : Set α} : g•''U ∩ V = (g•''U) ∩ (g•''V) :=
by
ext
rw [Set.mem_inter_iff, Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage,
Rubin.SmulImage.mem_smulImage, Set.mem_inter_iff]
#align smul''_inter Rubin.SmulImage.smulImage_inter
theorem SmulImage.smulImage_eq_inv_preimage {g : G} {U : Set α} : g•''U = (· • ·) g⁻¹ ⁻¹' U :=
by
ext
constructor
· intro h; rw [Set.mem_preimage]; exact mem_smulImage.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
theorem SmulImage.smulImage_eq_of_smul_eq {g h : G} {U : Set α} :
(∀ x ∈ U, g • x = h • x) → g•''U = h•''U :=
by
intro hU
ext x
rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage]
constructor
· intro k; let a := congr_arg ((· • ·) h⁻¹) (hU (g⁻¹ • x) k);
simp only [smul_inv_smul, inv_smul_smul] at a ; exact Set.mem_of_eq_of_mem a k
· intro k; let a := congr_arg ((· • ·) g⁻¹) (hU (h⁻¹ • x) 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
end SmulImage
--------------------------------
section Support
def SmulSupport.Support (α : Type _) [MulAction G α] (g : G) :=
{x : α | g • x ≠ x}
#align support Rubin.SmulSupport.Support
theorem SmulSupport.support_eq_not_fixed_by {g : G}:
Rubin.SmulSupport.Support α g = (MulAction.fixedBy α g)ᶜ := by tauto
#align support_eq_not_fixed_by Rubin.SmulSupport.support_eq_not_fixed_by
theorem SmulSupport.mem_support {x : α} {g : G} :
x ∈ Rubin.SmulSupport.Support α g ↔ g • x ≠ x := by tauto
#align mem_support Rubin.SmulSupport.mem_support
theorem SmulSupport.not_mem_support {x : α} {g : G} :
x ∉ Rubin.SmulSupport.Support α g ↔ g • x = x := by
rw [Rubin.SmulSupport.mem_support, Classical.not_not]
#align mem_not_support Rubin.SmulSupport.not_mem_support
theorem SmulSupport.smul_mem_support {g : G} {x : α} :
x ∈ Rubin.SmulSupport.Support α g → g • x ∈ Rubin.SmulSupport.Support α g := fun h =>
h ∘ smul_left_cancel g
#align smul_in_support Rubin.SmulSupport.smul_mem_support
theorem SmulSupport.inv_smul_mem_support {g : G} {x : α} :
x ∈ Rubin.SmulSupport.Support α g → g⁻¹ • x ∈ Rubin.SmulSupport.Support α g := fun h k =>
h (smul_inv_smul g x ▸ Rubin.GroupActionExt.smul_congr g k)
#align inv_smul_in_support Rubin.SmulSupport.inv_smul_mem_support
theorem SmulSupport.fixed_of_disjoint {g : G} {x : α} {U : Set α} :
x ∈ U → Disjoint U (Rubin.SmulSupport.Support α g) → g • x = x :=
fun x_in_U disjoint_U_support =>
Rubin.SmulSupport.not_mem_support.mp (Set.disjoint_left.mp disjoint_U_support x_in_U)
#align fixed_of_disjoint Rubin.SmulSupport.fixed_of_disjoint
theorem SmulSupport.fixed_smulImage_in_support (g : G) {U : Set α} :
Rubin.SmulSupport.Support α g ⊆ U → g•''U = U :=
by
intro support_in_U
ext x
cases' @or_not (x ∈ Rubin.SmulSupport.Support α g) with xmoved xfixed
exact
⟨fun _ => support_in_U xmoved, fun _ =>
SmulImage.mem_smulImage.mpr (support_in_U (Rubin.SmulSupport.inv_smul_mem_support xmoved))⟩
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
theorem SmulSupport.smulImage_subset_in_support (g : G) (U V : Set α) :
U ⊆ V → Rubin.SmulSupport.Support α g ⊆ V → g•''U ⊆ V := fun U_in_V support_in_V =>
Rubin.SmulSupport.fixed_smulImage_in_support g support_in_V ▸
Rubin.SmulImage.smulImage_subset g U_in_V
#align moves_subset_within_support Rubin.SmulSupport.smulImage_subset_in_support
theorem SmulSupport.support_mul (g h : G) (α : Type _) [MulAction G α] :
Rubin.SmulSupport.Support α (g * h) ⊆
Rubin.SmulSupport.Support α g ∪ Rubin.SmulSupport.Support α h :=
by
intro x x_in_support
by_contra h_support
let res := not_or.mp h_support
exact
x_in_support
((mul_smul g h x).trans
((congr_arg ((· • ·) g) (not_mem_support.mp res.2)).trans <| not_mem_support.mp res.1))
#align support_mul Rubin.SmulSupport.support_mul
theorem SmulSupport.support_conjugate (α : Type _) [MulAction G α] (g h : G) :
Rubin.SmulSupport.Support α (h * g * h⁻¹) = h•''Rubin.SmulSupport.Support α g :=
by
ext x
rw [Rubin.SmulSupport.mem_support, Rubin.SmulImage.mem_smulImage, Rubin.SmulSupport.mem_support,
mul_smul, mul_smul]
constructor
· intro h1; by_contra h2; exact h1 ((congr_arg ((· • ·) h) h2).trans (smul_inv_smul _ _))
· intro h1; by_contra h2; exact h1 (inv_smul_smul h (g • h⁻¹ • x) ▸ congr_arg ((· • ·) h⁻¹) h2)
#align support_conjugate Rubin.SmulSupport.support_conjugate
theorem SmulSupport.support_inv (α : Type _) [MulAction G α] (g : G) :
Rubin.SmulSupport.Support α g⁻¹ = Rubin.SmulSupport.Support α g :=
by
ext x
rw [Rubin.SmulSupport.mem_support, Rubin.SmulSupport.mem_support]
constructor
· intro h1; by_contra h2; exact h1 (GroupActionExt.smul_eq_iff_inv_smul_eq.mp h2)
· intro h1; by_contra h2; exact h1 (GroupActionExt.smul_eq_iff_inv_smul_eq.mpr h2)
#align support_inv Rubin.SmulSupport.support_inv
theorem SmulSupport.support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) :
Rubin.SmulSupport.Support α (g ^ j) ⊆ Rubin.SmulSupport.Support α g :=
by
intro x xmoved
by_contra xfixed
rw [Rubin.SmulSupport.mem_support] at xmoved
induction j with
| zero => apply xmoved; rw [pow_zero g, one_smul]
| succ j j_ih =>
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
exact j_ih
#align support_pow Rubin.SmulSupport.support_pow
theorem SmulSupport.support_comm (α : Type _) [MulAction G α] (g h : G) :
Rubin.SmulSupport.Support α ⁅g, h⁆ ⊆
Rubin.SmulSupport.Support α h ∪ (g•''Rubin.SmulSupport.Support α h) :=
by
intro x x_in_support
by_contra all_fixed
rw [Set.mem_union] at all_fixed
cases' @or_not (h • x = x) with xfixed xmoved
· rw [Rubin.SmulSupport.mem_support, Rubin.bracket_mul, mul_smul,
GroupActionExt.smul_eq_iff_inv_smul_eq.mp xfixed, ← Rubin.SmulSupport.mem_support] at x_in_support
exact
((Rubin.SmulSupport.support_conjugate α h g).symm ▸ (not_or.mp all_fixed).2)
x_in_support
· exact all_fixed (Or.inl xmoved)
#align support_comm Rubin.SmulSupport.support_comm
theorem SmulSupport.disjoint_support_comm (f g : G) {U : Set α} :
Rubin.SmulSupport.Support α f ⊆ U → Disjoint U (g•''U) → ∀ x ∈ U, ⁅f, g⁆ • x = f • x :=
by
intro support_in_U disjoint_U x x_in_U
have support_conj : Rubin.SmulSupport.Support α (g * f⁻¹ * g⁻¹) ⊆ g•''U :=
((Rubin.SmulSupport.support_conjugate α f⁻¹ g).trans
(Rubin.SmulImage.smulImage_congr g (Rubin.SmulSupport.support_inv α f))).symm ▸
Rubin.SmulImage.smulImage_subset g support_in_U
have goal :=
(congr_arg ((· • ·) f)
(Rubin.SmulSupport.fixed_of_disjoint x_in_U
(Set.disjoint_of_subset_right support_conj disjoint_U))).symm
simp at goal
sorry
-- rw [mul_smul, mul_smul] at goal
-- exact goal.symm
#align disjoint_support_comm Rubin.SmulSupport.disjoint_support_comm
end Support
-- 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 :=
{g : G | ∀ x : α, g • x = x ∨ x ∈ U}
@ -390,12 +79,12 @@ def rigidStabilizer (G : Type _) [Group G] [MulAction G α] (U : Set α) : Subgr
where
carrier := {g : G | ∀ (x) (_ : x ∉ U), g • x = x}
mul_mem' ha hb x x_notin_U := by rw [mul_smul, hb x x_notin_U, ha x x_notin_U]
inv_mem' hg x x_notin_U := Rubin.GroupActionExt.smul_eq_iff_inv_smul_eq.mp (hg x x_notin_U)
inv_mem' hg x x_notin_U := smul_eq_iff_inv_smul_eq.mp (hg x x_notin_U)
one_mem' x _ := one_smul G x
#align rigid_stabilizer Rubin.rigidStabilizer
theorem rist_supported_in_set {g : G} {U : Set α} :
g ∈ rigidStabilizer G U → Rubin.SmulSupport.Support α g ⊆ U := fun h x x_in_support =>
g ∈ rigidStabilizer G U → Support α g ⊆ U := fun h x x_in_support =>
by_contradiction (x_in_support ∘ h x)
#align rist_supported_in_set Rubin.rist_supported_in_set
@ -421,18 +110,18 @@ class Topological.ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpac
structure Topological.equivariant_homeomorph (G α β : Type _) [Group G] [TopologicalSpace α]
[TopologicalSpace β] [MulAction G α] [MulAction G β] extends Homeomorph α β where
equivariant : GroupActionExt.is_equivariant G toFun
equivariant : is_equivariant G toFun
#align equivariant_homeomorph Rubin.Topological.equivariant_homeomorph
theorem Topological.equivariant_fun [MulAction G α] [MulAction G β]
(h : Rubin.Topological.equivariant_homeomorph G α β) :
Rubin.GroupActionExt.is_equivariant G h.toFun :=
is_equivariant G h.toFun :=
h.equivariant
#align equivariant_fun Rubin.Topological.equivariant_fun
theorem Topological.equivariant_inv [MulAction G α] [MulAction G β]
(h : Rubin.Topological.equivariant_homeomorph G α β) :
Rubin.GroupActionExt.is_equivariant G h.invFun :=
is_equivariant G h.invFun :=
by
intro g x
symm
@ -446,12 +135,12 @@ variable [Rubin.Topological.ContinuousMulAction G α]
theorem Topological.img_open_open (g : G) (U : Set α) (h : IsOpen U)
[Rubin.Topological.ContinuousMulAction G α] : IsOpen (g •'' U) :=
by
rw [Rubin.SmulImage.smulImage_eq_inv_preimage]
rw [Rubin.smulImage_eq_inv_preimage]
exact Continuous.isOpen_preimage (Rubin.Topological.ContinuousMulAction.continuous g⁻¹) U h
#align img_open_open Rubin.Topological.img_open_open
theorem Topological.support_open (g : G) [TopologicalSpace α] [T2Space α]
[Rubin.Topological.ContinuousMulAction G α] : IsOpen (Rubin.SmulSupport.Support α g) :=
[Rubin.Topological.ContinuousMulAction G α] : IsOpen (Support α g) :=
by
apply isOpen_iff_forall_mem_open.mpr
intro x xmoved
@ -460,11 +149,11 @@ theorem Topological.support_open (g : G) [TopologicalSpace α] [T2Space α]
⟨V ∩ (g⁻¹ •'' U), fun y yW =>
-- TODO: don't use @-notation here
@Disjoint.ne_of_mem α U V disjoint_U_V (g • y)
(SmulImage.mem_inv_smulImage.mp (Set.mem_of_mem_inter_right yW))
(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),
⟨x_in_V, SmulImage.mem_inv_smulImage.mpr gx_in_U⟩⟩
⟨x_in_V, mem_inv_smulImage.mpr gx_in_U⟩⟩
#align support_open Rubin.Topological.support_open
end TopologicalActions
@ -492,7 +181,7 @@ theorem faithful_rigid_stabilizer_moves_point {g : G} {U : Set α} :
exact ⟨x, rist_supported_in_set g_rigid xmoved, xmoved⟩
#align faithful_rist_moves_point Rubin.faithful_rigid_stabilizer_moves_point
theorem ne_one_support_nonempty {g : G} : g ≠ 1 → (Rubin.SmulSupport.Support α g).Nonempty :=
theorem ne_one_support_nonempty {g : G} : g ≠ 1 → (Support α g).Nonempty :=
by
intro h1
cases' Rubin.faithful_moves_point'₁ α h1 with x h
@ -500,35 +189,31 @@ theorem ne_one_support_nonempty {g : G} : g ≠ 1 → (Rubin.SmulSupport.Support
exact h
#align ne_one_support_nempty Rubin.ne_one_support_nonempty
-- FIXME: somehow clashes with another definition
theorem disjoint_commute₁ {f g : G} :
Disjoint (Rubin.SmulSupport.Support α f) (Rubin.SmulSupport.Support α g) → Commute f g :=
theorem disjoint_commute {f g : G} :
Disjoint (Support α f) (Support α g) → Commute f g :=
by
intro hdisjoint
rw [← commutatorElement_eq_one_iff_commute]
apply @Rubin.faithful_moves_point₁ _ α
intro x
rw [Rubin.bracket_mul, mul_smul, mul_smul, mul_smul]
cases' @or_not (x ∈ Rubin.SmulSupport.Support α f) with hfmoved hffixed
·
rw [GroupActionExt.smul_eq_iff_inv_smul_eq.mp (SmulSupport.not_mem_support.mp (Set.disjoint_left.mp hdisjoint hfmoved)),
SmulSupport.not_mem_support.mp
(Set.disjoint_left.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hfmoved)),
rw [commutatorElement_def, mul_smul, mul_smul, mul_smul]
cases' @or_not (x ∈ Support α f) with hfmoved hffixed
· rw [smul_eq_iff_inv_smul_eq.mp (not_mem_support.mp (Set.disjoint_left.mp hdisjoint hfmoved)),
not_mem_support.mp
(Set.disjoint_left.mp hdisjoint (inv_smul_mem_support hfmoved)),
smul_inv_smul]
cases' @or_not (x ∈ Rubin.SmulSupport.Support α g) with hgmoved hgfixed
·
rw [GroupActionExt.smul_eq_iff_inv_smul_eq.mp
(SmulSupport.not_mem_support.mp <|
Set.disjoint_right.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hgmoved)),
smul_inv_smul, SmulSupport.not_mem_support.mp hffixed]
·
rw [
GroupActionExt.smul_eq_iff_inv_smul_eq.mp (SmulSupport.not_mem_support.mp hgfixed),
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
cases' @or_not (x ∈ Support α g) with hgmoved hgfixed
· rw [smul_eq_iff_inv_smul_eq.mp
(not_mem_support.mp <|
Set.disjoint_right.mp hdisjoint (inv_smul_mem_support hgmoved)),
smul_inv_smul, not_mem_support.mp hffixed]
· rw [
smul_eq_iff_inv_smul_eq.mp (not_mem_support.mp hgfixed),
smul_eq_iff_inv_smul_eq.mp (not_mem_support.mp hffixed),
not_mem_support.mp hgfixed,
not_mem_support.mp hffixed
]
#align disjoint_commute Rubin.disjoint_commute₁
#align disjoint_commute Rubin.disjoint_commute
end FaithfulActions
@ -1003,7 +688,7 @@ theorem RegularSupport.regular_interior_closure (U : Set α) :
#align regular_interior_closure Rubin.RegularSupport.regular_interior_closure
def RegularSupport.RegularSupport (α : Type _) [TopologicalSpace α] [MulAction G α] (g : G) :=
Rubin.RegularSupport.InteriorClosure (Rubin.SmulSupport.Support α g)
Rubin.RegularSupport.InteriorClosure (Support α g)
#align regular_support Rubin.RegularSupport.RegularSupport
theorem RegularSupport.regularSupport_regular {g : G} :
@ -1012,7 +697,7 @@ theorem RegularSupport.regularSupport_regular {g : G} :
#align regular_regular_support Rubin.RegularSupport.regularSupport_regular
theorem RegularSupport.support_subset_regularSupport [T2Space α] (g : G) :
Rubin.SmulSupport.Support α g ⊆ Rubin.RegularSupport.RegularSupport α g :=
Support α g ⊆ Rubin.RegularSupport.RegularSupport α g :=
Rubin.RegularSupport.IsOpen.interiorClosure_subset (Rubin.Topological.support_open g)
#align support_in_regular_support Rubin.RegularSupport.support_subset_regularSupport

45
Rubin/MulActionExt.lean
Unescape View File

@ -0,0 +1,45 @@
import Mathlib.GroupTheory.GroupAction.Basic
namespace Rubin
variable {G α β : Type _} [Group G]
variable [MulAction G α]
theorem smul_congr (g : G) {x y : α} (h : x = y) : g • x = g • y :=
congr_arg ((· • ·) g) h
#align smul_congr Rubin.smul_congr
theorem smul_eq_iff_inv_smul_eq {x : α} {g : G} : g • x = x ↔ g⁻¹ • x = x :=
⟨fun h => (smul_congr g⁻¹ h).symm.trans (inv_smul_smul g x), fun h =>
(smul_congr g h).symm.trans (smul_inv_smul g x)⟩
#align smul_eq_iff_inv_smul_eq Rubin.smul_eq_iff_inv_smul_eq
theorem smul_pow_eq_of_smul_eq {x : α} {g : G} (n : ℕ) :
g • x = x → g ^ n • x = x := by
induction n with
| zero => simp only [pow_zero, one_smul, eq_self_iff_true, imp_true_iff]
| succ n n_ih =>
intro h
nth_rw 2 [← (smul_congr g (n_ih h)).trans h]
rw [← mul_smul, ← pow_succ]
#align smul_pow_eq_of_smul_eq Rubin.smul_pow_eq_of_smul_eq
theorem smul_zpow_eq_of_smul_eq {x : α} {g : G} (n : ℤ) :
g • x = x → g ^ n • x = x := by
intro h
cases n with
| ofNat n => let res := smul_pow_eq_of_smul_eq n h; simp; exact res
| negSucc n =>
let res :=
smul_eq_iff_inv_smul_eq.mp (smul_pow_eq_of_smul_eq (1 + n) h);
simp
rw [add_comm]
exact res
#align smul_zpow_eq_of_smul_eq Rubin.smul_zpow_eq_of_smul_eq
def is_equivariant (G : Type _) {β : Type _} [Group G] [MulAction G α]
[MulAction G β] (f : α → β) :=
∀ g : G, ∀ x : α, f (g • x) = g • f x
#align is_equivariant Rubin.is_equivariant
end Rubin

138
Rubin/SmulImage.lean
Unescape View File

@ -0,0 +1,138 @@
import Mathlib.Data.Finset.Basic
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.GroupAction.Basic
import Rubin.MulActionExt
namespace Rubin
/--
The image of a group action (here generalized to any pair `(G, α)` implementing `SMul`)
is the image of the elements of `U` under the `g • u` operation.
An alternative definition (which is available through the [`mem_smulImage`] theorem and the [`smulImage_set`] equality) would be:
`SmulImage g U = {x | g⁻¹ • x ∈ U}`.
The notation used for this operator is `g •'' U`.
-/
def SmulImage {G α : Type _} [SMul G α] (g : G) (U : Set α) :=
(g • ·) '' U
#align subset_img Rubin.SmulImage
infixl:60 " •'' " => Rubin.SmulImage
/--
The pre-image of a group action (here generalized to any pair `(G, α)` implementing `SMul`)
is the set of values `x: α` such that `g • x ∈ U`.
Unlike [`SmulImage`], no notation is defined for this operator.
--/
def SmulPreImage {G α : Type _} [SMul G α] (g : G) (U : Set α) :=
{x | g • x ∈ U}
#align subset_preimg' Rubin.SmulPreImage
variable {G α : Type _}
variable [Group G]
variable [MulAction G α]
theorem smulImage_def {g : G} {U : Set α} : g •'' U = (· • ·) g '' U :=
rfl
#align subset_img_def Rubin.smulImage_def
theorem mem_smulImage {x : α} {g : G} {U : Set α} : x ∈ g •'' U ↔ g⁻¹ • x ∈ U :=
by
rw [Rubin.smulImage_def, Set.mem_image (g • ·) U x]
constructor
· rintro ⟨y, yU, gyx⟩
let ygx : y = g⁻¹ • x := inv_smul_smul g y ▸ Rubin.smul_congr g⁻¹ gyx
exact ygx ▸ yU
· intro h
exact ⟨g⁻¹ • x, ⟨Set.mem_preimage.mp h, smul_inv_smul g x⟩⟩
#align mem_smul'' Rubin.mem_smulImage
-- Provides a way to express a [`SmulImage`] as a `Set`;
-- this is simply [`mem_smulImage`] paired with set extensionality.
theorem smulImage_set {g: G} {U: Set α} : g •'' U = {x | g⁻¹ • x ∈ U} := Set.ext (fun _x => mem_smulImage)
theorem mem_inv_smulImage {x : α} {g : G} {U : Set α} : x ∈ g⁻¹ •'' U ↔ g • x ∈ U :=
by
let msi := @Rubin.mem_smulImage _ _ _ _ x g⁻¹ U
rw [inv_inv] at msi
exact msi
#align mem_inv_smul'' Rubin.mem_inv_smulImage
@[simp]
theorem mul_smulImage (g h : G) (U : Set α) : g •'' (h •'' U) = (g * h) •'' U :=
by
ext
rw [Rubin.mem_smulImage, Rubin.mem_smulImage, Rubin.mem_smulImage, ←
mul_smul, mul_inv_rev]
#align mul_smul'' Rubin.mul_smulImage
@[simp]
theorem one_smulImage (U : Set α) : (1 : G) •'' U = U :=
by
ext
rw [Rubin.mem_smulImage, inv_one, one_smul]
#align one_smul'' Rubin.one_smulImage
theorem disjoint_smulImage (g : G) {U V : Set α} :
Disjoint U V → Disjoint (g •'' U) (g •'' V) :=
by
intro disjoint_U_V
rw [Set.disjoint_left]
rw [Set.disjoint_left] at disjoint_U_V
intro x x_in_gU
by_contra h
exact (disjoint_U_V (mem_smulImage.mp x_in_gU)) (mem_smulImage.mp h)
#align disjoint_smul'' Rubin.disjoint_smulImage
namespace SmulImage
theorem congr (g : G) {U V : Set α} : U = V → g •'' U = g •'' V :=
congr_arg fun W : Set α => g •'' W
#align smul''_congr Rubin.SmulImage.congr
end SmulImage
theorem smulImage_subset (g : G) {U V : Set α} : U ⊆ V → g •'' U ⊆ g •'' V :=
by
intro h1 x
rw [Rubin.mem_smulImage, Rubin.mem_smulImage]
exact fun h2 => h1 h2
#align smul''_subset Rubin.smulImage_subset
theorem smulImage_union (g : G) {U V : Set α} : g •'' U ∪ V = (g •'' U) ∪ (g •'' V) :=
by
ext
rw [Rubin.mem_smulImage, Set.mem_union, Set.mem_union, Rubin.mem_smulImage,
Rubin.mem_smulImage]
#align smul''_union Rubin.smulImage_union
theorem smulImage_inter (g : G) {U V : Set α} : g •'' U ∩ V = (g •'' U) ∩ (g •'' V) :=
by
ext
rw [Set.mem_inter_iff, Rubin.mem_smulImage, Rubin.mem_smulImage,
Rubin.mem_smulImage, Set.mem_inter_iff]
#align smul''_inter Rubin.smulImage_inter
theorem smulImage_eq_inv_preimage {g : G} {U : Set α} : g •'' U = (· • ·) g⁻¹ ⁻¹' U :=
by
ext
constructor
· intro h; rw [Set.mem_preimage]; exact mem_smulImage.mp h
· intro h; rw [Rubin.mem_smulImage]; exact Set.mem_preimage.mp h
#align smul''_eq_inv_preimage Rubin.smulImage_eq_inv_preimage
theorem smulImage_eq_of_smul_eq {g h : G} {U : Set α} :
(∀ x ∈ U, g • x = h • x) → g •'' U = h •'' U :=
by
intro hU
ext x
rw [Rubin.mem_smulImage, Rubin.mem_smulImage]
constructor
· intro k; let a := congr_arg (h⁻¹ • ·) (hU (g⁻¹ • x) k);
simp only [smul_inv_smul, inv_smul_smul] at a ; exact Set.mem_of_eq_of_mem a k
· intro k; let a := congr_arg (g⁻¹ • ·) (hU (h⁻¹ • x) 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_eq_of_smul_eq
end Rubin

173
Rubin/Support.lean
Unescape View File

@ -0,0 +1,173 @@
import Mathlib.Data.Finset.Basic
import Mathlib.GroupTheory.Commutator
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.GroupAction.Basic
import Rubin.MulActionExt
import Rubin.SmulImage
import Rubin.Tactic
namespace Rubin
/--
The support of a group action of `g: G` on `α` (here generalized to `SMul G α`)
is the set of values `x` in `α` for which `g • x ≠ x`.
This can also be thought of as the complement of the fixpoints of `(g •)`,
which [`support_eq_not_fixed_by`] provides.
--/
def Support {G : Type _} (α : Type _) [SMul G α] (g : G) :=
{x : α | g • x ≠ x}
#align support Rubin.Support
theorem SmulSupport_def {G : Type _} (α : Type _) [SMul G α] {g : G} :
Support α g = {x : α | g • x ≠ x} := by tauto
variable {G α: Type _}
variable [Group G]
variable [MulAction G α]
variable {f g : G}
variable {x : α}
theorem support_eq_not_fixed_by : Support α g = (MulAction.fixedBy α g)ᶜ := by tauto
#align support_eq_not_fixed_by Rubin.support_eq_not_fixed_by
theorem support_compl_eq_fixed_by : (Support α g)ᶜ = MulAction.fixedBy α g := by
rw [<-compl_compl (MulAction.fixedBy _ _)]
exact congr_arg (·ᶜ) support_eq_not_fixed_by
theorem mem_support :
x ∈ Support α g ↔ g • x ≠ x := by tauto
#align mem_support Rubin.mem_support
theorem not_mem_support :
x ∉ Support α g ↔ g • x = x := by
rw [Rubin.mem_support, Classical.not_not]
#align mem_not_support Rubin.not_mem_support
theorem smul_mem_support :
x ∈ Support α g → g • x ∈ Support α g := fun h =>
h ∘ smul_left_cancel g
#align smul_in_support Rubin.smul_mem_support
theorem inv_smul_mem_support :
x ∈ Support α g → g⁻¹ • x ∈ Support α g := fun h k =>
h (smul_inv_smul g x ▸ smul_congr g k)
#align inv_smul_in_support Rubin.inv_smul_mem_support
theorem fixed_of_disjoint {U : Set α} :
x ∈ U → Disjoint U (Support α g) → g • x = x :=
fun x_in_U disjoint_U_support =>
not_mem_support.mp (Set.disjoint_left.mp disjoint_U_support x_in_U)
#align fixed_of_disjoint Rubin.fixed_of_disjoint
theorem fixed_smulImage_in_support (g : G) {U : Set α} :
Support α g ⊆ U → g •'' U = U :=
by
intro support_in_U
ext x
cases' @or_not (x ∈ Support α g) with xmoved xfixed
exact
⟨fun _ => support_in_U xmoved, fun _ =>
mem_smulImage.mpr (support_in_U (Rubin.inv_smul_mem_support xmoved))⟩
rw [Rubin.mem_smulImage, smul_eq_iff_inv_smul_eq.mp (not_mem_support.mp xfixed)]
#align fixes_subset_within_support Rubin.fixed_smulImage_in_support
theorem smulImage_subset_in_support (g : G) (U V : Set α) :
U ⊆ V → Support α g ⊆ V → g •'' U ⊆ V := fun U_in_V support_in_V =>
Rubin.fixed_smulImage_in_support g support_in_V ▸
Rubin.smulImage_subset g U_in_V
#align moves_subset_within_support Rubin.smulImage_subset_in_support
theorem support_mul (g h : G) (α : Type _) [MulAction G α] :
Support α (g * h) ⊆
Support α g ∪ Support α h :=
by
intro x x_in_support
by_contra h_support
let res := not_or.mp h_support
exact
x_in_support
((mul_smul g h x).trans
((congr_arg (g • ·) (not_mem_support.mp res.2)).trans <| not_mem_support.mp res.1))
#align support_mul Rubin.support_mul
theorem support_conjugate (α : Type _) [MulAction G α] (g h : G) :
Support α (h * g * h⁻¹) = h •'' Support α g :=
by
ext x
rw [Rubin.mem_support, Rubin.mem_smulImage, Rubin.mem_support,
mul_smul, mul_smul]
constructor
· intro h1; by_contra h2; exact h1 ((congr_arg (h • ·) h2).trans (smul_inv_smul _ _))
· intro h1; by_contra h2; exact h1 (inv_smul_smul h (g • h⁻¹ • x) ▸ congr_arg (h⁻¹ • ·) h2)
#align support_conjugate Rubin.support_conjugate
theorem support_inv (α : Type _) [MulAction G α] (g : G) :
Support α g⁻¹ = Support α g :=
by
ext x
rw [Rubin.mem_support, Rubin.mem_support]
constructor
· intro h1; by_contra h2; exact h1 (smul_eq_iff_inv_smul_eq.mp h2)
· intro h1; by_contra h2; exact h1 (smul_eq_iff_inv_smul_eq.mpr h2)
#align support_inv Rubin.support_inv
theorem support_pow (α : Type _) [MulAction G α] (g : G) (j : ℕ) :
Support α (g ^ j) ⊆ Support α g :=
by
intro x xmoved
by_contra xfixed
rw [Rubin.mem_support] at xmoved
induction j with
| zero => apply xmoved; rw [pow_zero g, one_smul]
| succ j j_ih =>
apply xmoved
let j_ih := (congr_arg (g • ·) (not_not.mp j_ih)).trans (not_mem_support.mp xfixed)
simp at j_ih
group_action at j_ih
rw [<-Nat.one_add, <-zpow_ofNat, Int.ofNat_add]
exact j_ih
-- TODO: address this pain point
-- Alternatively:
-- rw [Int.add_comm, Int.ofNat_add_one_out, zpow_ofNat] at j_ih
-- exact j_ih
#align support_pow Rubin.support_pow
theorem support_comm (α : Type _) [MulAction G α] (g h : G) :
Support α ⁅g, h⁆ ⊆
Support α h ∪ (g •'' Support α h) :=
by
intro x x_in_support
by_contra all_fixed
rw [Set.mem_union] at all_fixed
cases' @or_not (h • x = x) with xfixed xmoved
· rw [Rubin.mem_support, commutatorElement_def, mul_smul,
smul_eq_iff_inv_smul_eq.mp xfixed, ← Rubin.mem_support] at x_in_support
exact
((Rubin.support_conjugate α h g).symm ▸ (not_or.mp all_fixed).2)
x_in_support
· exact all_fixed (Or.inl xmoved)
#align support_comm Rubin.support_comm
theorem disjoint_support_comm (f g : G) {U : Set α} :
Support α f ⊆ U → Disjoint U (g •'' U) → ∀ x ∈ U, ⁅f, g⁆ • x = f • x :=
by
intro support_in_U disjoint_U x x_in_U
have support_conj : Support α (g * f⁻¹ * g⁻¹) ⊆ g •'' U :=
((Rubin.support_conjugate α f⁻¹ g).trans
(Rubin.SmulImage.congr g (Rubin.support_inv α f))).symm ▸
Rubin.smulImage_subset g support_in_U
have goal :=
(congr_arg (f • ·)
(Rubin.fixed_of_disjoint x_in_U
(Set.disjoint_of_subset_right support_conj disjoint_U))).symm
simp at goal
-- NOTE: the nth_rewrite must happen on the second occurence, or else group_action yields an incorrect f⁻²
nth_rewrite 2 [goal]
group_action
#align disjoint_support_comm Rubin.disjoint_support_comm
end Rubin

68
Rubin/Tactic.lean
Unescape View File

@ -1,8 +1,8 @@
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.Commutator
import Mathlib.GroupTheory.GroupAction.Basic
import Mathlib.GroupTheory.Exponent
import Mathlib.GroupTheory.Perm.Basic
-- import Mathlib.GroupTheory.Commutator
-- import Mathlib.GroupTheory.GroupAction.Basic
-- import Mathlib.GroupTheory.Exponent
-- import Mathlib.GroupTheory.Perm.Basic
import Lean.Meta.Tactic.Util
import Lean.Elab.Tactic.Basic
@ -36,6 +36,7 @@ theorem smul_succ {G α : Type _} (n : ℕ) [Group G] [MulAction G α] {g : G}
rw [pow_succ, mul_smul]
#align smul_succ Rubin.Tactic.smul_succ
-- Note: calling "group" after "group_action₁" might not be a good idea, as they can end up running in a loop
syntax (name := group_action₁) "group_action₁" (location)?: tactic
macro_rules
| `(tactic| group_action₁ $[at $location]?) => `(tactic| simp only [
@ -55,16 +56,16 @@ macro_rules
one_pow,
one_zpow,
mul_zpow_neg_one,
<-mul_zpow_neg_one,
zpow_zero,
mul_zpow,
zpow_sub,
zpow_ofNat,
zpow_neg_one,
<-zpow_neg_one,
<-zpow_mul,
zpow_add_one,
zpow_one_add,
zpow_add,
<-zpow_add_one,
<-zpow_one_add,
<-zpow_add,
Int.ofNat_add,
Int.ofNat_mul,
@ -110,4 +111,53 @@ example (G α : Type _) [Group G] (a b c : G) [MulAction G α] (x : α) :
⁅a * b, c⁆ • x = (a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆) • x := by
group_action
section PotentialLoops
variable {G α : Type _}
variable [Group G]
variable [MulAction G α]
variable (g f : G)
variable (x : α)
example: x = g • f⁻¹ • g⁻¹ • x ↔ g⁻¹ • x = f • g⁻¹ • x := by
group_action
constructor <;> intro h <;> exact h.symm
example: x = g • f⁻¹ • g⁻¹ • x ↔ g⁻¹ • x = f • g⁻¹ • x := by
constructor
· intro h
group_action at h
nth_rewrite 2 [h]
group_action
· intro h
group_action at h
nth_rewrite 1 [<-h]
group_action
example: x = g • f⁻¹ • g⁻¹ • x ↔ g⁻¹ • x = f⁻¹ • g⁻¹ • x := by
constructor
· intro h
nth_rewrite 1 [h]
group_action
· intro h
group_action at h
nth_rewrite 2 [<-h]
group_action
example (h: (g * f ^ (-2 : ℤ) * g ^ (-1 : ℤ)) • x = x):
g⁻¹ • (g * f ^ (-1 : ℤ) * g ^ (-1 : ℤ)) • x = f • g⁻¹ • x :=
by
group_action
exact h
example (h: x = g • f⁻¹ • g⁻¹ • x): True := by
group_action at h
exact True.intro
example (j: ℕ) (h: g • g ^ j • x = x): True := by
group_action at h
exact True.intro
end PotentialLoops
end Rubin.Tactic

Write Preview
Loading…
Cancel
Save