From c6021b7b74fdf03681a73e4bbcb7e6eee9f15ffa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 22 Oct 2024 16:09:30 +0000 Subject: [PATCH] refactor(GroupAction/Blocks): additivise, fix names, golf API (#17578) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Most of the API can be additivised smoothly. The lemma names didn't match the naming convention. Some proofs were harder than necessary because of the suboptimal definition of `IsBlock` as `∀ _, _ ∨ _` rather than `∀ _, _ → _`. From LeanCamCombi --- Mathlib/Data/Set/Pairwise/Basic.lean | 8 +- Mathlib/GroupTheory/GroupAction/Basic.lean | 2 + Mathlib/GroupTheory/GroupAction/Blocks.lean | 476 ++++++++++---------- 3 files changed, 233 insertions(+), 253 deletions(-) diff --git a/Mathlib/Data/Set/Pairwise/Basic.lean b/Mathlib/Data/Set/Pairwise/Basic.lean index 7365c110ac476..ec5b714ca6538 100644 --- a/Mathlib/Data/Set/Pairwise/Basic.lean +++ b/Mathlib/Data/Set/Pairwise/Basic.lean @@ -296,12 +296,8 @@ lemma PairwiseDisjoint.eq_or_disjoint exact h.elim hi hj lemma pairwiseDisjoint_range_iff {α β : Type*} {f : α → (Set β)} : - (Set.range f).PairwiseDisjoint id ↔ ∀ x y, f x = f y ∨ Disjoint (f x) (f y) := by - constructor - · intro h x y - apply h.eq_or_disjoint (Set.mem_range_self x) (Set.mem_range_self y) - · rintro h _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy - exact (h x y).resolve_left hxy + (range f).PairwiseDisjoint id ↔ ∀ x y, f x ≠ f y → Disjoint (f x) (f y) := by + aesop (add simp [PairwiseDisjoint, Set.Pairwise]) /-- If the range of `f` is pairwise disjoint, then the image of any set `s` under `f` is as well. -/ lemma _root_.Pairwise.pairwiseDisjoint (h : Pairwise (Disjoint on f)) (s : Set ι) : diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean index 547d1fc8f93c9..e890d7dc7383d 100644 --- a/Mathlib/GroupTheory/GroupAction/Basic.lean +++ b/Mathlib/GroupTheory/GroupAction/Basic.lean @@ -296,6 +296,8 @@ variable {G α β : Type*} [Group G] [MulAction G α] [MulAction G β] section Orbit +-- TODO: This proof is redoing a special case of `MulAction.IsInvariantBlock.isBlock`. Can we move +-- this lemma earlier to golf? @[to_additive (attr := simp)] theorem smul_orbit (g : G) (a : α) : g • orbit G a = orbit G a := (smul_orbit_subset g a).antisymm <| diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean index cc63c90b25d16..054bfb7524698 100644 --- a/Mathlib/GroupTheory/GroupAction/Blocks.lean +++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean @@ -3,11 +3,7 @@ Copyright (c) 2024 Antoine Chambert-Loir. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Antoine Chambert-Loir -/ - -import Mathlib.Algebra.Group.Subgroup.Actions -import Mathlib.Data.Set.Card import Mathlib.Data.Setoid.Partition -import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.GroupTheory.GroupAction.Pointwise import Mathlib.GroupTheory.GroupAction.SubMulAction import Mathlib.GroupTheory.Index @@ -39,10 +35,10 @@ that contain a given point is a block ## References -We follow [wielandt1964]. - +We follow [Wielandt-1964]. -/ +open Set open scoped Pointwise namespace MulAction @@ -51,12 +47,14 @@ section orbits variable {G : Type*} [Group G] {X : Type*} [MulAction G X] +@[to_additive] theorem orbit.eq_or_disjoint (a b : X) : orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b) := by apply (em (Disjoint (orbit G a) (orbit G b))).symm.imp _ id simp (config := { contextual := true }) only [Set.not_disjoint_iff, ← orbit_eq_iff, forall_exists_index, and_imp, eq_comm, implies_true] +@[to_additive] theorem orbit.pairwiseDisjoint : (Set.range fun x : X => orbit G x).PairwiseDisjoint id := by rintro s ⟨x, rfl⟩ t ⟨y, rfl⟩ h @@ -64,6 +62,7 @@ theorem orbit.pairwiseDisjoint : exact (orbit.eq_or_disjoint x y).resolve_right h /-- Orbits of an element form a partition -/ +@[to_additive] theorem IsPartition.of_orbits : Setoid.IsPartition (Set.range fun a : X => orbit G a) := by apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty @@ -76,246 +75,201 @@ end orbits section SMul -variable (G : Type*) {X : Type*} [SMul G X] +variable (G : Type*) {X : Type*} [SMul G X] {B : Set X} {a : X} -- Change terminology : is_fully_invariant ? -/-- For `SMul G X`, a fixed block is a `Set X` which is fully invariant: - `g • B = B` for all `g : G` -/ +/-- A set `B` is a `G`-fixed block if `g • B = B` for all `g : G`. -/ +@[to_additive "A set `B` is a `G`-fixed block if `g +ᵥ B = B` for all `g : G`."] def IsFixedBlock (B : Set X) := ∀ g : G, g • B = B -/-- For `SMul G X`, an invariant block is a `Set X` which is stable: - `g • B ⊆ B` for all `g : G` -/ +/-- A set `B` is a `G`-invariant block if `g • B ⊆ B` for all `g : G`. + +Note: It is not necessarily a block when the action is not by a group. -/ +@[to_additive +"A set `B` is a `G`-invariant block if `g +ᵥ B ⊆ B` for all `g : G`. + +Note: It is not necessarily a block when the action is not by a group. "] def IsInvariantBlock (B : Set X) := ∀ g : G, g • B ⊆ B -/-- A trivial block is a `Set X` which is either a subsingleton or ⊤ - (it is not necessarily a block…) -/ -def IsTrivialBlock (B : Set X) := B.Subsingleton ∨ B = ⊤ +/-- A trivial block is a `Set X` which is either a subsingleton or `univ`. -/-- `For SMul G X`, a block is a `Set X` whose translates are pairwise disjoint -/ -def IsBlock (B : Set X) := (Set.range fun g : G => g • B).PairwiseDisjoint id +Note: It is not necessarily a block when the action is not by a group. -/ +@[to_additive +"A trivial block is a `Set X` which is either a subsingleton or `univ`. + +Note: It is not necessarily a block when the action is not by a group."] +def IsTrivialBlock (B : Set X) := B.Subsingleton ∨ B = univ + +/-- A set `B` is a `G`-block iff the sets of the form `g • B` are pairwise equal or disjoint. -/ +@[to_additive +"A set `B` is a `G`-block iff the sets of the form `g +ᵥ B` are pairwise equal or disjoint. "] +def IsBlock (B : Set X) := ∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B) variable {G} -/-- A set B is a block iff for all g, g', -the sets g • B and g' • B are either equal or disjoint -/ -theorem IsBlock.def {B : Set X} : - IsBlock G B ↔ ∀ g g' : G, g • B = g' • B ∨ Disjoint (g • B) (g' • B) := by - apply Set.pairwiseDisjoint_range_iff +@[to_additive] +lemma isBlock_iff_smul_eq_smul_of_nonempty : + IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B := by + simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm] + +@[to_additive] +lemma isBlock_iff_pairwiseDisjoint_range_smul : + IsBlock G B ↔ (range fun g : G ↦ g • B).PairwiseDisjoint id := pairwiseDisjoint_range_iff.symm -/-- Alternate definition of a block -/ -theorem IsBlock.mk_notempty {B : Set X} : - IsBlock G B ↔ ∀ g g' : G, g • B ∩ g' • B ≠ ∅ → g • B = g' • B := by - simp_rw [IsBlock.def, or_iff_not_imp_right, Set.disjoint_iff_inter_eq_empty] +@[to_additive] +lemma isBlock_iff_smul_eq_smul_or_disjoint : + IsBlock G B ↔ ∀ g₁ g₂ : G, g₁ • B = g₂ • B ∨ Disjoint (g₁ • B) (g₂ • B) := + forall₂_congr fun _ _ ↦ or_iff_not_imp_left.symm -/-- A fixed block is a block -/ -theorem IsFixedBlock.isBlock {B : Set X} (hfB : IsFixedBlock G B) : - IsBlock G B := by - simp [IsBlock.def, hfB _] +alias ⟨IsBlock.smul_eq_smul_of_nonempty, _⟩ := isBlock_iff_smul_eq_smul_of_nonempty +alias ⟨IsBlock.pairwiseDisjoint_range_smul, _⟩ := isBlock_iff_pairwiseDisjoint_range_smul +alias ⟨IsBlock.smul_eq_smul_or_disjoint, _⟩ := isBlock_iff_smul_eq_smul_or_disjoint -variable (X) +/-- A fixed block is a block. -/ +@[to_additive "A fixed block is a block."] +lemma IsFixedBlock.isBlock (hfB : IsFixedBlock G B) : IsBlock G B := by simp [IsBlock, hfB _] -/-- The empty set is a block -/ -theorem isBlock_empty : IsBlock G (⊥ : Set X) := by - simp [IsBlock.def, Set.bot_eq_empty, Set.smul_set_empty] +/-- The empty set is a block. -/ +@[to_additive (attr := simp) "The empty set is a block."] +lemma IsBlock.empty : IsBlock G (∅ : Set X) := by simp [IsBlock] -variable {X} +/-- A singleton is a block. -/ +@[to_additive "A singleton is a block."] +lemma IsBlock.singleton : IsBlock G ({a} : Set X) := by simp [IsBlock] -theorem isBlock_singleton (a : X) : IsBlock G ({a} : Set X) := by - simp [IsBlock.def, Classical.or_iff_not_imp_left] +/-- Subsingletons are (trivial) blocks. -/ +@[to_additive "Subsingletons are (trivial) blocks."] +lemma IsBlock.of_subsingleton (hB : B.Subsingleton) : IsBlock G B := + hB.induction_on .empty fun _ ↦ .singleton -/-- Subsingletons are (trivial) blocks -/ -theorem isBlock_subsingleton {B : Set X} (hB : B.Subsingleton) : - IsBlock G B := - hB.induction_on (isBlock_empty _) isBlock_singleton +/-- A fixed block is an invariant block. -/ +@[to_additive "A fixed block is an invariant block."] +lemma IsFixedBlock.isInvariantBlock (hB : IsFixedBlock G B) : IsInvariantBlock G B := + fun _ ↦ (hB _).le end SMul section Group -variable {G : Type*} [Group G] {X : Type*} [MulAction G X] +variable {G : Type*} [Group G] {X : Type*} [MulAction G X] {B : Set X} + +@[to_additive] +lemma isBlock_iff_disjoint_smul_of_ne : + IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B := by + refine ⟨fun hB g ↦ by simpa using hB (g₂ := 1), fun hB g₁ g₂ h ↦ ?_⟩ + simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢ + exact hB h + +@[to_additive] +lemma isBlock_iff_smul_eq_of_nonempty : + IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B := by + simp_rw [isBlock_iff_disjoint_smul_of_ne, ← not_disjoint_iff_nonempty_inter, not_imp_comm] + +@[to_additive] +lemma isBlock_iff_smul_eq_or_disjoint : + IsBlock G B ↔ ∀ g : G, g • B = B ∨ Disjoint (g • B) B := + isBlock_iff_disjoint_smul_of_ne.trans <| forall_congr' fun _ ↦ or_iff_not_imp_left.symm + +@[to_additive] +lemma isBlock_iff_smul_eq_of_mem : + IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B := by + simp [isBlock_iff_smul_eq_of_nonempty, Set.Nonempty, mem_smul_set] + +@[to_additive] alias ⟨IsBlock.disjoint_smul_of_ne, _⟩ := isBlock_iff_disjoint_smul_of_ne +@[to_additive] alias ⟨IsBlock.smul_eq_of_nonempty, _⟩ := isBlock_iff_smul_eq_of_nonempty +@[to_additive] alias ⟨IsBlock.smul_eq_or_disjoint, _⟩ := isBlock_iff_smul_eq_or_disjoint +@[to_additive] alias ⟨IsBlock.smul_eq_of_mem, _⟩ := isBlock_iff_smul_eq_of_mem + +-- TODO: Generalise to `SubgroupClass` +/-- If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`. -/ +@[to_additive +"If `B` is a `G`-block, then it is also a `H`-block for any subgroup `H` of `G`."] +lemma IsBlock.subgroup {H : Subgroup G} (hB : IsBlock G B) : IsBlock H B := fun _ _ h ↦ hB h + +/-- A block of a group action is invariant iff it is fixed. -/ +@[to_additive "A block of a group action is invariant iff it is fixed."] +lemma isInvariantBlock_iff_isFixedBlock : IsInvariantBlock G B ↔ IsFixedBlock G B := + ⟨fun hB g ↦ (hB g).antisymm <| subset_set_smul_iff.2 <| hB _, IsFixedBlock.isInvariantBlock⟩ + +/-- An invariant block of a group action is a fixed block. -/ +@[to_additive "An invariant block of a group action is a fixed block."] +alias ⟨IsInvariantBlock.isFixedBlock, _⟩ := isInvariantBlock_iff_isFixedBlock + +/-- An invariant block of a group action is a block. -/ +@[to_additive "An invariant block of a group action is a block."] +lemma IsInvariantBlock.isBlock (hB : IsInvariantBlock G B) : IsBlock G B := hB.isFixedBlock.isBlock + +/-- The full set is a fixed block. -/ +@[to_additive "The full set is a fixed block."] +lemma IsFixedBlock.univ : IsFixedBlock G (univ : Set X) := fun _ ↦ by simp + +/-- The full set is a block. -/ +@[to_additive (attr := simp) "The full set is a block."] +lemma IsBlock.univ : IsBlock G (univ : Set X) := IsFixedBlock.univ.isBlock + +/-- The intersection of two blocks is a block. -/ +@[to_additive "The intersection of two blocks is a block."] +lemma IsBlock.inter {B₁ B₂ : Set X} (h₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) : + IsBlock G (B₁ ∩ B₂) := by + simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢ + rintro g₁ g₂ ⟨a, ha₁, ha₂⟩ + rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩] -theorem IsBlock.smul_eq_or_disjoint {B : Set X} (hB : IsBlock G B) (g : G) : - g • B = B ∨ Disjoint (g • B) B := by - rw [IsBlock.def] at hB - simpa only [one_smul] using hB g 1 - -theorem IsBlock.def_one {B : Set X} : - IsBlock G B ↔ ∀ g : G, g • B = B ∨ Disjoint (g • B) B := by - refine ⟨IsBlock.smul_eq_or_disjoint, ?_⟩ - rw [IsBlock.def] - intro hB g g' - apply (hB (g'⁻¹ * g)).imp - · rw [← smul_smul, ← eq_inv_smul_iff, inv_inv] - exact id - · intro h - rw [Set.disjoint_iff] at h ⊢ - rintro x hx - suffices g'⁻¹ • x ∈ (g'⁻¹ * g) • B ∩ B by apply h this - rw [Set.mem_inter_iff] - simp only [← smul_smul, ← Set.mem_smul_set_iff_inv_smul_mem, smul_inv_smul] - exact hx - -theorem IsBlock.mk_notempty_one {B : Set X} : - IsBlock G B ↔ ∀ g : G, g • B ∩ B ≠ ∅ → g • B = B := by - simp_rw [IsBlock.def_one, Set.disjoint_iff_inter_eq_empty, or_iff_not_imp_right] - -theorem IsBlock.mk_mem {B : Set X} : - IsBlock G B ↔ ∀ (g : G) (a : X) (_ : a ∈ B) (_ : g • a ∈ B), g • B = B := by - rw [IsBlock.mk_notempty_one] - simp only [← Set.nonempty_iff_ne_empty, Set.nonempty_def, Set.mem_inter_iff, - exists_imp, and_imp, Set.mem_smul_set_iff_inv_smul_mem] - constructor - · intro H g a ha hga - apply H g (g • a) _ hga - simpa only [inv_smul_smul] using ha - · intro H g a ha hga - rw [← eq_inv_smul_iff, eq_comm] - exact H g⁻¹ a hga ha - -theorem IsBlock.def_mem {B : Set X} (hB : IsBlock G B) {a : X} {g : G} : - a ∈ B → g • a ∈ B → g • B = B := - IsBlock.mk_mem.mp hB g a - -theorem IsBlock.mk_subset {B : Set X} : - IsBlock G B ↔ ∀ {g : G} {b : X} (_ : b ∈ B) (_ : b ∈ g • B), g • B ⊆ B := by - simp_rw [IsBlock.mk_notempty_one, ← Set.nonempty_iff_ne_empty] - constructor - · intro hB g b hb hgb - exact (hB g ⟨b, hgb, hb⟩).le - · intro hB g ⟨b, hb', hb⟩ - apply le_antisymm (hB hb hb') - suffices g⁻¹ • B ≤ B by - rw [Set.le_iff_subset] at this ⊢ - rwa [← inv_inv g, ← Set.set_smul_subset_iff] - exact hB (Set.mem_smul_set_iff_inv_smul_mem.mp hb') (Set.smul_mem_smul_set_iff.mpr hb) - -/-- An invariant block is a fixed block -/ -theorem IsInvariantBlock.isFixedBlock {B : Set X} (hfB : IsInvariantBlock G B) : - IsFixedBlock G B := by - intro g - apply le_antisymm (hfB g) - intro x hx - rw [Set.mem_smul_set_iff_inv_smul_mem] - apply hfB g⁻¹ - rwa [Set.smul_mem_smul_set_iff] - -/-- An invariant block is a block -/ -theorem IsInvariantBlock.isBlock {B : Set X} (hfB : IsInvariantBlock G B) : - IsBlock G B := - hfB.isFixedBlock.isBlock - -/-- An orbit is a block -/ -theorem isFixedBlock_orbit (a : X) : IsFixedBlock G (orbit G a) := - (smul_orbit · a) - -/-- An orbit is a block -/ -theorem isBlock_orbit (a : X) : IsBlock G (orbit G a) := - (isFixedBlock_orbit a).isBlock - -variable (X) - -/-- The full set is a (trivial) block -/ -theorem isFixedBlock_univ : IsFixedBlock G (Set.univ : Set X) := - fun _ ↦ by simp only [Set.smul_set_univ] -@[deprecated (since := "2024-09-14")] alias isFixedBlock_top := isFixedBlock_univ - -/-- The full set is a (trivial) block -/ -theorem isBlock_univ : IsBlock G (Set.univ : Set X) := - (isFixedBlock_univ _).isBlock - -variable {X} - -/-- Is `B` is a block for an action of `G`, it is a block for the action of any subgroup of `G` -/ -theorem IsBlock.subgroup {H : Subgroup G} {B : Set X} (hfB : IsBlock G B) : - IsBlock H B := by - rw [IsBlock.def_one]; rintro ⟨g, _⟩ - simpa only using hfB.smul_eq_or_disjoint g - -theorem IsBlock.preimage {H Y : Type*} [Group H] [MulAction H Y] - {φ : H → G} (j : Y →ₑ[φ] X) {B : Set X} (hB : IsBlock G B) : +/-- An intersection of blocks is a block. -/ +@[to_additive "An intersection of blocks is a block."] +lemma IsBlock.iInter {ι : Sort*} {B : ι → Set X} (hB : ∀ i, IsBlock G (B i)) : + IsBlock G (⋂ i, B i) := by + simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢ + rintro g₁ g₂ ⟨a, ha₁, ha₂⟩ + simp_rw [fun i ↦ hB i ⟨a, iInter_subset _ i ha₁, iInter_subset _ i ha₂⟩] + +/-- A trivial block is a block. -/ +@[to_additive "A trivial block is a block."] +lemma IsTrivialBlock.isBlock (hB : IsTrivialBlock B) : IsBlock G B := by + obtain hB | rfl := hB + · exact .of_subsingleton hB + · exact .univ + +/-- An orbit is a fixed block. -/ +@[to_additive "An orbit is a fixed block."] +protected lemma IsFixedBlock.orbit (a : X) : IsFixedBlock G (orbit G a) := (smul_orbit · a) + +/-- An orbit is a block. -/ +@[to_additive "An orbit is a block."] +protected lemma IsBlock.orbit (a : X) : IsBlock G (orbit G a) := (IsFixedBlock.orbit a).isBlock + +@[to_additive] +lemma isBlock_top : IsBlock (⊤ : Subgroup G) B ↔ IsBlock G B := + Subgroup.topEquiv.toEquiv.forall_congr fun _ ↦ Subgroup.topEquiv.toEquiv.forall_congr_left + +lemma IsBlock.preimage {H Y : Type*} [Group H] [MulAction H Y] + {φ : H → G} (j : Y →ₑ[φ] X) (hB : IsBlock G B) : IsBlock H (j ⁻¹' B) := by - rw [IsBlock.def_one] - intro g - rw [← Group.preimage_smul_setₛₗ Y X φ j] - apply (hB.smul_eq_or_disjoint (φ g)).imp - · intro heq - rw [heq] - · exact Disjoint.preimage _ + rintro g₁ g₂ hg + rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢ + exact (hB <| ne_of_apply_ne _ hg).preimage _ theorem IsBlock.image {H Y : Type*} [Group H] [MulAction H Y] {φ : G →* H} (j : X →ₑ[φ] Y) (hφ : Function.Surjective φ) (hj : Function.Injective j) - {B : Set X} (hB : IsBlock G B) : + (hB : IsBlock G B) : IsBlock H (j '' B) := by - rw [IsBlock.def] - intro h h' - obtain ⟨g, rfl⟩ := hφ h - obtain ⟨g', rfl⟩ := hφ h' - simp only [← image_smul_setₛₗ X Y φ j] - cases' IsBlock.def.mp hB g g' with h h - · left; rw [h] - · right; exact Set.disjoint_image_of_injective hj h - -theorem IsBlock.subtype_val_preimage {C : SubMulAction G X} {B : Set X} (hB : IsBlock G B) : + simp only [IsBlock, hφ.forall, ← image_smul_setₛₗ] + exact fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg + +theorem IsBlock.subtype_val_preimage {C : SubMulAction G X} (hB : IsBlock G B) : IsBlock G (Subtype.val ⁻¹' B : Set C) := hB.preimage C.inclusion -theorem IsBlock.iff_subtype_val {C : SubMulAction G X} {B : Set C} : - IsBlock G B ↔ IsBlock G (Subtype.val '' B : Set X) := by - simp only [IsBlock.def_one] - apply forall_congr' - intro g - rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set _ _ _ C.inclusion g B, - ← Set.image_eq_image Subtype.coe_injective] - apply or_congr Iff.rfl - simp only [Set.disjoint_iff, Set.subset_empty_iff, Set.image_eq_empty, - ← C.inclusion_injective.injOn.image_inter (Set.subset_univ _) (Set.subset_univ _)] - -theorem IsBlock.iff_top (B : Set X) : - IsBlock G B ↔ IsBlock (⊤ : Subgroup G) B := by - simp only [IsBlock.def_one] - constructor - · intro h g; exact h g - · intro h g; exact h ⟨g, Subgroup.mem_top g⟩ +theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} : + IsBlock G (Subtype.val '' B : Set X) ↔ IsBlock G B := by + refine forall₂_congr fun g₁ g₂ ↦ ?_ + rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq, + Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective] -/-- The intersection of two blocks is a block -/ -theorem IsBlock.inter {B₁ B₂ : Set X} (h₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) : - IsBlock G (B₁ ∩ B₂) := by - rw [IsBlock.def_one] - intro g - rw [Set.smul_set_inter] - cases' h₁.smul_eq_or_disjoint g with h₁ h₁ - · cases' h₂.smul_eq_or_disjoint g with h₂ h₂ - · left; rw [h₁, h₂] - right - apply Disjoint.inter_left'; apply Disjoint.inter_right' - exact h₂ - · right - apply Disjoint.inter_left; apply Disjoint.inter_right - exact h₁ - -/-- An intersection of blocks is a block -/ -theorem IsBlock.iInter {ι : Type*} {B : ι → Set X} (hB : ∀ i : ι, IsBlock G (B i)) : - IsBlock G (⋂ i, B i) := by - by_cases hι : (IsEmpty ι) - · -- ι = ∅, block = univ - suffices (⋂ i : ι, B i) = Set.univ by simpa only [this] using isBlock_univ X - simpa only [Set.iInter_eq_univ] using (hι.elim' ·) - rw [IsBlock.def_one] - intro g - rw [Set.smul_set_iInter] - by_cases h : ∃ i : ι, Disjoint (g • B i) (B i) - · right - obtain ⟨j, hj⟩ := h - refine Disjoint.mono ?_ ?_ hj <;> apply Set.iInter_subset - · left - simp only [not_exists] at h - have : ∀ i : ι, g • B i = B i := fun i => ((hB i).smul_eq_or_disjoint g).resolve_right (h i) - rw [Set.iInter_congr this] - -theorem IsBlock.of_subgroup_of_conjugate {B : Set X} {H : Subgroup G} (hB : IsBlock H B) (g : G) : +theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g : G) : IsBlock (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H) (g • B) := by - rw [IsBlock.def_one] + rw [isBlock_iff_smul_eq_or_disjoint] intro h' obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h') simp only [MulEquiv.coe_toMonoidHom, MulAut.conj_apply] at hh @@ -329,9 +283,9 @@ theorem IsBlock.of_subgroup_of_conjugate {B : Set X} {H : Subgroup G} (hB : IsBl rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right] /-- A translate of a block is a block -/ -theorem IsBlock.translate {B : Set X} (g : G) (hB : IsBlock G B) : +theorem IsBlock.translate (g : G) (hB : IsBlock G B) : IsBlock G (g • B) := by - rw [IsBlock.iff_top] at hB ⊢ + rw [← isBlock_top] at hB ⊢ rw [← Subgroup.map_comap_eq_self_of_surjective (f := MulAut.conj g) (MulAut.conj g).surjective ⊤] apply IsBlock.of_subgroup_of_conjugate rwa [Subgroup.comap_top] @@ -339,12 +293,11 @@ theorem IsBlock.translate {B : Set X} (g : G) (hB : IsBlock G B) : variable (G) in /-- For `SMul G X`, a block system of `X` is a partition of `X` into blocks for the action of `G` -/ -def IsBlockSystem (B : Set (Set X)) := - Setoid.IsPartition B ∧ ∀ b : Set X, b ∈ B → IsBlock G b +def IsBlockSystem (ℬ : Set (Set X)) := Setoid.IsPartition ℬ ∧ ∀ ⦃B⦄, B ∈ ℬ → IsBlock G B -/-- Translates of a block form a `block_system` -/ +/-- Translates of a block form a block system. -/ theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X] - {B : Set X} (hB : IsBlock G B) (hBe : B.Nonempty) : + (hB : IsBlock G B) (hBe : B.Nonempty) : IsBlockSystem G (Set.range fun g : G => g • B) := by refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩ case mem_blocks => rintro B' ⟨g, rfl⟩; exact hB.translate g @@ -359,10 +312,7 @@ theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X] simp only [Set.smul_mem_smul_set_iff, hb, exists_unique_iff_exists, Set.mem_range, exists_apply_eq_apply, exists_const, exists_prop, and_imp, forall_exists_index, forall_apply_eq_imp_iff, true_and] - intro g' ha - apply (IsBlock.def.mp hB g' g).resolve_right - rw [Set.not_disjoint_iff] - refine ⟨g • b, ha, ⟨b, hb, rfl⟩⟩ + exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩ section Normal @@ -382,9 +332,9 @@ lemma smul_orbit_eq_orbit_smul (N : Subgroup G) [nN : N.Normal] (a : X) (g : G) simp only [← mul_assoc, ← smul_smul, smul_inv_smul, inv_inv] /-- An orbit of a normal subgroup is a block -/ -theorem orbit.isBlock_of_normal {N : Subgroup G} [N.Normal] (a : X) : +theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) : IsBlock G (orbit N a) := by - rw [IsBlock.def_one] + rw [isBlock_iff_smul_eq_or_disjoint] intro g rw [smul_orbit_eq_orbit_smul] apply orbit.eq_or_disjoint @@ -395,7 +345,48 @@ theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] : constructor · apply IsPartition.of_orbits · intro b; rintro ⟨a, rfl⟩ - exact orbit.isBlock_of_normal a + exact .orbit_of_normal a + +section Group +variable {S H : Type*} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} {a b : G} + +/-! +Annoyingly, it seems like the following two lemmas cannot be unified. +-/ + +section Left +variable [MulAction G H] [IsScalarTower G H H] + +/-- See `MulAction.isBlock_subgroup'` for a version that works for the right action of a group on +itself. -/ +@[to_additive "See `AddAction.isBlock_subgroup'` for a version that works for the right action +of a group on itself."] +lemma isBlock_subgroup : IsBlock G (s : Set H) := by + simp only [IsBlock, disjoint_left] + rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩ + refine hab ?_ + rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd] + +end Left + +section Right +variable [MulAction G H] [IsScalarTower G Hᵐᵒᵖ H] + +open MulOpposite + +/-- See `MulAction.isBlock_subgroup` for a version that works for the left action of a group on +itself. -/ +@[to_additive "See `AddAction.isBlock_subgroup` for a version that works for the left action +of a group on itself."] +lemma isBlock_subgroup' : IsBlock G (s : Set H) := by + simp only [IsBlock, disjoint_left] + rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩ + refine hab ?_ + rw [← op_smul_coe_set hc, ← smul_assoc, ← op_smul, ← hcd, op_smul, smul_assoc, op_smul_coe_set hc, + op_smul_coe_set hd] + +end Right +end Group end Normal @@ -411,28 +402,21 @@ section Stabilizer /-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block -/ theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ H) : IsBlock G (MulAction.orbit H a) := by - simp_rw [IsBlock.def_one, or_iff_not_imp_right, Set.not_disjoint_iff] - rintro g ⟨-, ⟨-, ⟨h₁, rfl⟩, h⟩, ⟨h₂, rfl⟩⟩ + rw [isBlock_iff_smul_eq_of_nonempty] + rintro g ⟨-, ⟨-, ⟨h₁, rfl⟩, h⟩, h₂, rfl⟩ suffices g ∈ H by rw [← Subgroup.coe_mk H g this, ← H.toSubmonoid.smul_def, smul_orbit (⟨g, this⟩ : H) a] rw [← mul_mem_cancel_left h₂⁻¹.2, ← mul_mem_cancel_right h₁.2] apply hH - simp only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff] - exact h + simpa only [mem_stabilizer_iff, InvMemClass.coe_inv, mul_smul, inv_smul_eq_iff] /-- If `B` is a block containing `a`, then the stabilizer of `B` contains the stabilizer of `a` -/ -theorem IsBlock.stabilizer_le {B : Set X} (hB : IsBlock G B) {a : X} (ha : a ∈ B) : - stabilizer G a ≤ stabilizer G B := by - intro g hg - apply Or.resolve_right (hB.smul_eq_or_disjoint g) - rw [Set.not_disjoint_iff] - refine ⟨a, ?_, ha⟩ - rw [← hg, Set.smul_mem_smul_set_iff] - exact ha +theorem IsBlock.stabilizer_le (hB : IsBlock G B) {a : X} (ha : a ∈ B) : + stabilizer G a ≤ stabilizer G B := + fun g hg ↦ hB.smul_eq_of_nonempty ⟨a, by rwa [← hg, smul_mem_smul_set_iff], ha⟩ /-- A block containing `a` is the orbit of `a` under its stabilizer -/ -theorem IsBlock.orbit_stabilizer_eq - [htGX : IsPretransitive G X] {B : Set X} (hB : IsBlock G B) {a : X} (ha : a ∈ B) : +theorem IsBlock.orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a : X} (ha : a ∈ B) : MulAction.orbit (stabilizer G B) a = B := by ext x constructor @@ -442,7 +426,7 @@ theorem IsBlock.orbit_stabilizer_eq exact ha · intro hx obtain ⟨k, rfl⟩ := exists_smul_eq G a x - exact ⟨⟨k, hB.def_mem ha hx⟩, rfl⟩ + exact ⟨⟨k, hB.smul_eq_of_mem ha hx⟩, rfl⟩ /-- A subgroup containing the stabilizer of `a` is the stabilizer of the orbit of `a` under that subgroup -/ @@ -479,9 +463,9 @@ def block_stabilizerOrderIso [htGX : IsPretransitive G X] (a : X) : obtain ⟨k, rfl⟩ := htGX.exists_smul_eq a b suffices k ∈ stabilizer G B' by exact this.symm ▸ (Set.smul_mem_smul_set ha') - exact hBB' (hB.def_mem ha hb) + exact hBB' (hB.smul_eq_of_mem ha hb) · intro hBB' g hgB - apply IsBlock.def_mem hB' ha' + apply hB'.smul_eq_of_mem ha' exact hBB' <| hgB.symm ▸ (Set.smul_mem_smul_set ha) end Stabilizer @@ -552,7 +536,7 @@ theorem of_subset {B : Set X} (a : X) (hfB : B.Finite) : IsBlock G (⋂ (k : G) (_ : a ∈ k • B), k • B) := by let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B cases' Set.eq_empty_or_nonempty B with hfB_e hfB_ne - · simp [hfB_e, isBlock_univ] + · simp [hfB_e] have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by intro k hk exact Set.biInter_subset_of_mem hk @@ -569,10 +553,8 @@ theorem of_subset {B : Set X} (a : X) (hfB : B.Finite) : have hag' (g : G) (hg : a ∈ g • B') : B' = g • B' := by rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_of_finite_iff_le_smul _ hfB'] exact hag g hg - rw [mk_notempty_one] - intro g hg - rw [← Set.nonempty_iff_ne_empty] at hg - obtain ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩ := Set.nonempty_def.mp hg + rw [isBlock_iff_smul_eq_of_nonempty] + rintro g ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩ obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b have hak : a ∈ k⁻¹ • B' := by refine ⟨b, hb, ?_⟩