From a8c3cd1aa145551b3f04408c16300c59621c7897 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Mon, 20 Nov 2023 02:42:01 +0100 Subject: [PATCH] Fix most issues with porting --- Rubin.lean | 405 ++++++++++++++++++++++++++++------------------------- 1 file changed, 216 insertions(+), 189 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index 9155dcf..b4d10ae 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -31,94 +31,93 @@ theorem Rubin.GroupActionExt.smul_eq_smul_inv {G α : Type _} [Group G] [MulActi by constructor · intro hyp - let this.1 := congr_arg ((· • ·) h⁻¹) hyp - rw [← mul_smul, ← mul_smul, mul_left_inv, one_smul] at this - exact this + let res := congr_arg ((· • ·) h⁻¹) hyp + simp at res + rw [← mul_smul] at res + exact res · intro hyp - let this.1 := congr_arg ((· • ·) h) hyp - rw [← mul_smul, ← mul_assoc, mul_right_inv, one_mul] at this - exact this + rw [<-hyp, mul_smul] + simp #align smul_eq_smul Rubin.GroupActionExt.smul_eq_smul_inv theorem Rubin.GroupActionExt.smul_succ {G α : Type _} (n : ℕ) [Group G] [MulAction G α] {g : G} {x : α} : g ^ n.succ • x = g • g ^ n • x := by - have := Tactic.Ring.pow_add_rev g 1 n - rw [pow_one, ← Nat.succ_eq_one_add] at this - rw [← this, smul_smul] + rw [pow_succ, mul_smul] #align smul_succ Rubin.GroupActionExt.smul_succ section GroupActionTactic -namespace Tactic.Interactive - -/- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/ -open Tactic - -/- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/ -open Tactic.SimpArgType Interactive Tactic.Group - -/-- Auxiliary tactic for the `group_action` tactic. Calls the simplifier only. -/ -unsafe def aux_group_action (locat : Loc) : tactic Unit := - tactic.interactive.simp_core { failIfUnchanged := false } skip true - [expr ``(Rubin.GroupActionExt.smul_smul'), expr ``(Rubin.GroupActionExt.smul_eq_smul_inv), - 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 ``(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_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), - 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), - 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_one'), expr ``(zpow_trick_sub), 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 ``(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.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_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 ``(Mathlib.Tactic.Group.zpow_trick), expr ``(Mathlib.Tactic.Group.zpow_trick_one), - expr ``(Mathlib.Tactic.Group.zpow_trick_one'), expr ``(zpow_trick_sub), - expr ``(Tactic.Ring.horner)] - [] locat >> - skip -#align tactic.interactive.aux_group_action tactic.interactive.aux_group_action - -/-- Tactic for normalizing expressions in group actions, without assuming -commutativity, using only the group axioms without any information about -which group is manipulated. -Example: -```lean -example {G α : Type} [group G] [mul_action G α] (a b : G) (x y : α) (h : a • b • x = a • y) : b⁻¹ • y = x := -begin - group_action at h, -- normalizes `h` which becomes `h : c = d` - rw ← h, -- the goal is now `a*d*d⁻¹ = a` - group_action -- which then normalized and closed -end -``` --/ -unsafe def group_action (locat : parse location) : tactic Unit := do - aux_group_action locat - repeat (andthen (aux_group₂ locat) (aux_group_action locat)) -#align tactic.interactive.group_action tactic.interactive.group_action +-- namespace Tactic.Interactive + +-- /- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/ +-- open Tactic + +-- /- ./././Mathport/Syntax/Translate/Tactic/Mathlib/Core.lean:38:34: unsupported: setup_tactic_parser -/ +-- open Tactic.SimpArgType Interactive Tactic.Group + +-- /-- Auxiliary tactic for the `group_action` tactic. Calls the simplifier only. -/ +-- unsafe def aux_group_action (locat : Loc) : tactic Unit := +-- tactic.interactive.simp_core { failIfUnchanged := false } skip true +-- [expr ``(Rubin.GroupActionExt.smul_smul'), expr ``(Rubin.GroupActionExt.smul_eq_smul_inv), +-- 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 ``(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_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), +-- 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), +-- 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_one'), expr ``(zpow_trick_sub), 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 ``(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.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_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 ``(Mathlib.Tactic.Group.zpow_trick), expr ``(Mathlib.Tactic.Group.zpow_trick_one), +-- expr ``(Mathlib.Tactic.Group.zpow_trick_one'), expr ``(zpow_trick_sub), +-- expr ``(Tactic.Ring.horner)] +-- [] locat >> +-- skip +-- #align tactic.interactive.aux_group_action tactic.interactive.aux_group_action + +-- /-- Tactic for normalizing expressions in group actions, without assuming +-- commutativity, using only the group axioms without any information about +-- which group is manipulated. +-- Example: +-- ```lean +-- example {G α : Type} [group G] [mul_action G α] (a b : G) (x y : α) (h : a • b • x = a • y) : b⁻¹ • y = x := +-- begin +-- group_action at h, -- normalizes `h` which becomes `h : c = d` +-- rw ← h, -- the goal is now `a*d*d⁻¹ = a` +-- group_action -- which then normalized and closed +-- end +-- ``` +-- -/ +-- unsafe def group_action (locat : parse location) : tactic Unit := do +-- aux_group_action locat +-- repeat (andthen (aux_group₂ locat) (aux_group_action locat)) +-- #align tactic.interactive.group_action tactic.interactive.group_action -end Tactic.Interactive +-- end Tactic.Interactive -add_tactic_doc - { Name := "group_action" - category := DocCategory.tactic - declNames := [`tactic.interactive.group_action] - tags := ["decision procedure", "simplification"] } +-- add_tactic_doc +-- { Name := "group_action" +-- category := DocCategory.tactic +-- declNames := [`tactic.interactive.group_action] +-- tags := ["decision procedure", "simplification"] } -end GroupActionTactic +-- end GroupActionTactic /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]] -/ example (G α : Type _) [Group G] (a b c : G) [MulAction G α] (x : α) : ⁅a * b, c⁆ • x = (a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆) • x := by + sorry trace "./././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 α] {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 Subgroup.mk_smul Rubin.GroupActionExt.subgroup_mk_smul #align add_subgroup.mk_vadd AddSubgroup.mk_vadd ---------------------------------------------------------------- @@ -171,12 +170,12 @@ theorem Rubin.orbit_bot (G : Type _) [Group G] [MulAction G α] (p : α) : constructor · rintro ⟨⟨_, g_bot⟩, g_to_x⟩ rw [← g_to_x, Set.mem_singleton_iff, Rubin.GroupActionExt.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⟩ + 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 Smul'' +section SmulImage theorem Rubin.GroupActionExt.smul_congr (g : G) {x y : α} (h : x = y) : g • x = g • y := 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 : ℕ) : g • x = x → g ^ n • x = x := by - induction n - simp only [pow_zero, one_smul, eq_self_iff_true, imp_true_iff] - · intro h + 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 @@ -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 : ℤ) : g • x = x → g ^ n • x = x := by intro h - cases n - · let this.1 := Rubin.GroupActionExt.smul_pow_eq_of_smul_eq n h; finish - · - let this.1 := + 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); - finish + simp + rw [add_comm] + exact res #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 α] @@ -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 exact ygx ▸ yU · 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 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 intro x x_in_gU 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 -- 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 ext constructor - · intro h; rw [Set.mem_preimage]; exact mem_smul''.mp h - · intro h; rw [Rubin.SmulImage.mem_smulImage]; exact set.mem_preimage.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 #align smul''_eq_inv_preimage Rubin.SmulImage.smulImage_eq_inv_preimage theorem Rubin.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 + ext x rw [Rubin.SmulImage.mem_smulImage, Rubin.SmulImage.mem_smulImage] constructor · 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 #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) := {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 exact ⟨fun _ => support_in_U xmoved, fun _ => - mem_smul''.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)] + 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 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 intro x x_in_support by_contra h_support - let this.1 := not_or_distrib.mp h_support + + let res := not_or.mp h_support exact x_in_support ((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 theorem Rubin.SmulSupport.support_conjugate (α : Type _) [MulAction G α] (g h : G) : Rubin.SmulSupport.Support α (h * g * h⁻¹) = h•''Rubin.SmulSupport.Support α g := by - ext + ext x rw [Rubin.SmulSupport.mem_support, Rubin.SmulImage.mem_smulImage, Rubin.SmulSupport.mem_support, mul_smul, mul_smul] 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) : Rubin.SmulSupport.Support α g⁻¹ = Rubin.SmulSupport.Support α g := by - ext + ext x rw [Rubin.SmulSupport.mem_support, Rubin.SmulSupport.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) + · 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 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 by_contra xfixed rw [Rubin.SmulSupport.mem_support] at xmoved - induction j - · apply xmoved; rw [pow_zero g, one_smul] - · apply xmoved - let j_ih := (congr_arg ((· • ·) g) (not_not.mp j_ih)).trans (mem_not_support.mp xfixed) + 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 @@ -438,9 +443,9 @@ theorem Rubin.SmulSupport.support_comm (α : Type _) [MulAction G α] (g h : G) 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, - 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 - ((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 · exact all_fixed (Or.inl xmoved) #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) (Rubin.SmulSupport.fixed_of_disjoint x_in_U (Set.disjoint_of_subset_right support_conj disjoint_U))).symm - rw [← mul_smul, ← mul_assoc, ← mul_assoc] at goal - exact goal.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 Rubin.SmulSupport.Support +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 := @@ -499,12 +507,12 @@ variable [TopologicalSpace α] [TopologicalSpace β] class Rubin.Topological.ContinuousMulAction (G α : Type _) [Group G] [TopologicalSpace α] extends 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 structure Rubin.Topological.equivariant_homeomorph (G α β : Type _) [Group G] [TopologicalSpace α] [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 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 := by 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 - exact e.symm + exact e #align equivariant_inv Rubin.Topological.equivariant_inv 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 α] [Rubin.Topological.ContinuousMulAction G α] : IsOpen (Rubin.SmulSupport.Support α g) := by - apply is_open_iff_forall_mem_open.mpr + apply isOpen_iff_forall_mem_open.mpr 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⟩ exact ⟨V ∩ (g⁻¹•''U), fun y yW => - @Disjoint.ne_of_mem α U V disjoint_U_V (g • y) y - (mem_inv_smul''.mp (Set.mem_of_mem_inter_right yW)) (Set.mem_of_mem_inter_left 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)) + y + (Set.mem_of_mem_inter_left yW), 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 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 := by intro h1 - cases' Rubin.faithful_moves_point'₁ α h1 with x _ + cases' Rubin.faithful_moves_point'₁ α h1 with x h use x + exact h #align ne_one_support_nempty Rubin.ne_one_support_nonempty -- 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] 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)), - mem_not_support.mp - (set.disjoint_left.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hfmoved)), + 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)), smul_inv_smul] cases' @or_not (x ∈ Rubin.SmulSupport.Support α g) with hgmoved hgfixed · - rw [smul_eq_iff_inv_smul_eq.mp - (mem_not_support.mp <| - set.disjoint_right.mp hdisjoint (Rubin.SmulSupport.inv_smul_mem_support hgmoved)), - smul_inv_smul, mem_not_support.mp hffixed] + 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 [smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp hgfixed), - smul_eq_iff_inv_smul_eq.mp (mem_not_support.mp hffixed), mem_not_support.mp hgfixed, - mem_not_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 + ] #align disjoint_commute Rubin.disjoint_commute₁ end FaithfulActions @@ -613,7 +629,7 @@ section RubinActions variable [TopologicalSpace α] [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 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 constructor · 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; - exact set.eq_empty_iff_forall_not_mem.mp h ↑m ⟨m_pos, gmp_eq_p⟩ + 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 Nat.sInf_le ⟨m_pos, gmp_eq_p⟩ #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 := Rubin.Period.period_le_fix (by norm_num : 1 > 0) (by + sorry trace "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `group_action #[[]]" : (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 #[[]] -/ -- 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) : (Rubin.Period.periods U H).Nonempty ∧ BddAbove (Rubin.Period.periods U H) ∧ ∃ (m : ℕ) (m_pos : m > 0), ∀ (p : α) (g : H), g ^ m • p = p := by 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 "./././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; - 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; + have periods_nonempty : (Rubin.Period.periods U H).Nonempty := by + use 1; + 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]; 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⟩ @@ -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 ⟨periods_nonempty, periods_bounded, m, m_pos, gmp_eq_p⟩ rcases Nat.sSup_mem periods_nonempty periods_bounded with ⟨p, g, hperiod⟩ + use p + use g + use sSup (Rubin.Period.periods U H) 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 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 := by - cases eq_zero_or_neZero (Rubin.Period.period p g) - · rw [h]; finish - · + cases eq_zero_or_neZero (Rubin.Period.period p g) with + | inl h => rw [h]; simp + | inr h => exact (Nat.sInf_mem (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, -- split, -- exact ⟨mem_inv_smul''.mpr gx_in_V,x_in_W⟩, --- exact set.disjoint_of_subset --- (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) +-- exact Set.disjoint_of_subset +-- (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_smulImage.mp hy)) : g•''U ⊆ V) -- disjoint_V_W.symm -- 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 @@ -784,15 +811,15 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa -- split, -- exact ⟨x_in_W,x_in_V⟩, -- split, --- exact set.inter_subset_right W V, --- exact set.disjoint_of_subset --- (set.inter_subset_left W V) --- ((@smul''_inter _ _ _ _ g W V).symm ▸ set.inter_subset_left (g•''W) (g•''V) : g•''U ⊆ g•''W) +-- exact Set.inter_subset_right W V, +-- exact Set.disjoint_of_subset +-- (Set.inter_subset_left W V) +-- ((@smul''_inter _ _ _ _ g W V).symm ▸ Set.inter_subset_left (g•''W) (g•''V) : g•''U ⊆ g•''W) -- disjoint_W -- 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 -- ext, --- simp only [set.mem_Union, set.mem_union], +-- simp only [Set.mem_Union, Set.mem_union], -- split, -- { simp only [forall_exists_index], -- intro i, @@ -803,27 +830,27 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa -- intros disjoint_f_g h hfh, -- let support_f := 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 hx_ne_x := mem_support.mp hx.2, -- -- 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⟩, --- 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 --- 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 -- 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), -- 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 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⟩, +-- 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⟩, -- use f₁, use f₂, -- -- note that f₁,f₂ commute with g since their support is in support α f -- 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, --- 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 -- let k := ⁅f₂,h⁆, -- -- 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, -- -- 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 --- 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, --- 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, -- 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. -- 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), @@ -860,10 +887,10 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa -- split, -- exact is_open_Inter (λp : ι2, (disjoint_hyp p.1.1 p.1.2 p.2).some_spec.1), -- 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, --- 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 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, -- simp only [subtype.val_eq_coe, smul''_mul, mul_inv_cancel_left] at this, -- from this -- 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, -- exact this }, -- have := moves_inj period_ge_n, --- finish +-- done -- end -- 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, @@ -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 -- by_contra not_disjoint, -- 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 -- 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), --- 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₀⟩, +-- 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_fin five_points with ⟨V₁,open_V₁,x_in_V₁,disjoint_img_V₁⟩, -- simp only at disjoint_img_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 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⟩, +-- 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⟩, -- have comm_non_trivial : ¬commute f h := begin -- by_contra comm_trivial, -- 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, -- exact z_moved act_comm.symm, -- 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⟩, -- 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) --- 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 --- 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, -- 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, @@ -967,20 +994,20 @@ def Rubin.Disjointness.IsLocallyMoving (G α : Type _) [Group G] [TopologicalSpa -- 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₂} -- 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⟩, -- clear h_1_w h_1_h_h_w pigeonhole, -- 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, -- 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_j : g^j.val • p ∈ k •'' V := same_k ▸ (set.mem_Union.mp $ support_h' $ gi_in_support j).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, -- -- 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 -- 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, -- 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, -- 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 @@ -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, -- from this -- 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 -- lemma remark_1_2 (f g : G) : is_algebraically_disjoint f g → commute f g := begin -- intro alg_disjoint, @@ -1035,13 +1062,13 @@ theorem Rubin.RegularSupport.interiorClosure_mono {U V : Set α} : interior_mono ∘ closure_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 -#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 -#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) := by @@ -1059,7 +1086,7 @@ theorem Rubin.RegularSupport.IsOpen.interiorClosure_subset {U : Set α} : theorem Rubin.RegularSupport.regular_interior_closure (U : Set α) : (Rubin.RegularSupport.InteriorClosure U).is_regular_open := by - rw [Rubin.RegularSupport.Set.is_regular_def] + rw [Set.is_regular_def] apply Set.Subset.antisymm 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) @@ -1082,7 +1109,7 @@ theorem Rubin.RegularSupport.support_subset_regularSupport [T2Space α] (g : G) theorem Rubin.RegularSupport.mem_regularSupport (g : G) (U : Set α) : U.is_regular_open → g ∈ rigidStabilizer G U → Rubin.RegularSupport.RegularSupport α g ⊆ U := 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) #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 := -- begin -- 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 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 +-- have giq_notin_V := Set.disjoint_left.mp (h_disj i (⟨ 0, n_pos ⟩ : fin n) i_ne_zero) hcontra', +-- exact ((by done : g ^ 0•''V = V) ▸ giq_notin_V) hcontra -- 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 -- 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' ⟩, -- dsimp at disj', -- let V := 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_U : V ⊆ U := Set.inter_subset_left 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 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), -- { intros i j i_ne_j W W_ss_giV W_ss_gjV, -- 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_gjV (smul''_subset (↑g ^ ↑j) V'_ss_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⟩, +-- (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)) }, +-- 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 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 giq_notin_V : ∀ (i : fin n), (i : ℕ) > 0 → g ^ (i : ℕ) • (q : α) ∉ V := distinct_images_from_disjoint n_pos disj q q_in_V,