From 92a65e4cac0fb86ec5a14cddb8379343e338c4fa Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 5 Jan 2025 22:24:29 +0100 Subject: [PATCH 1/8] to-additive on Blocks --- Mathlib/GroupTheory/GroupAction/Blocks.lean | 72 +++++++++++++++++++-- 1 file changed, 67 insertions(+), 5 deletions(-) diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean index bb890e738c69d..e14a65eafc8bf 100644 --- a/Mathlib/GroupTheory/GroupAction/Blocks.lean +++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean @@ -15,10 +15,12 @@ import Mathlib.Tactic.IntervalCases Given `SMul G X`, an action of a type `G` on a type `X`, we define - the predicate `IsBlock G B` states that `B : Set X` is a block, - which means that the sets `g • B`, for `g ∈ G`, are equal or disjoint. +which means that the sets `g • B`, for `g ∈ G`, are equal or disjoint. +Under `Group G` and `MulAction G X`, this is equivalent to the classical +definition `MulAction.IsBlock.def_one` - a bunch of lemmas that give examples of “trivial” blocks : ⊥, ⊤, singletons, - and non trivial blocks: orbit of the group, orbit of a normal subgroup… +and non trivial blocks: orbit of the group, orbit of a normal subgroup… The non-existence of nontrivial blocks is the definition of primitive actions. @@ -143,8 +145,11 @@ lemma IsBlock.disjoint_smul_set_smul (hB : IsBlock G B) (hgs : ¬ g • B ⊆ s lemma IsBlock.disjoint_smul_smul_set (hB : IsBlock G B) (hgs : ¬ g • B ⊆ s • B) : Disjoint (s • B) (g • B) := (hB.disjoint_smul_set_smul hgs).symm +@[to_additive] alias ⟨IsBlock.smul_eq_smul_of_nonempty, _⟩ := isBlock_iff_smul_eq_smul_of_nonempty +@[to_additive] alias ⟨IsBlock.pairwiseDisjoint_range_smul, _⟩ := isBlock_iff_pairwiseDisjoint_range_smul +@[to_additive] alias ⟨IsBlock.smul_eq_smul_or_disjoint, _⟩ := isBlock_iff_smul_eq_smul_or_disjoint /-- A fixed block is a block. -/ @@ -277,6 +282,7 @@ protected lemma IsBlock.orbit (a : X) : IsBlock G (orbit G a) := (IsFixedBlock.o lemma isBlock_top : IsBlock (⊤ : Subgroup G) B ↔ IsBlock G B := Subgroup.topEquiv.toEquiv.forall_congr fun _ ↦ Subgroup.topEquiv.toEquiv.forall_congr_left +@[to_additive] 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 @@ -284,6 +290,7 @@ lemma IsBlock.preimage {H Y : Type*} [Group H] [MulAction H Y] rw [← Group.preimage_smul_setₛₗ, ← Group.preimage_smul_setₛₗ] at hg ⊢ exact (hB <| ne_of_apply_ne _ hg).preimage _ +@[to_additive] theorem IsBlock.image {H Y : Type*} [Group H] [MulAction H Y] {φ : G →* H} (j : X →ₑ[φ] Y) (hφ : Function.Surjective φ) (hj : Function.Injective j) @@ -292,10 +299,12 @@ theorem IsBlock.image {H Y : Type*} [Group H] [MulAction H Y] simp only [IsBlock, hφ.forall, ← image_smul_setₛₗ] exact fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg +@[to_additive] theorem IsBlock.subtype_val_preimage {C : SubMulAction G X} (hB : IsBlock G B) : IsBlock G (Subtype.val ⁻¹' B : Set C) := hB.preimage C.inclusion +@[to_additive] 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₂ ↦ ?_ @@ -303,7 +312,7 @@ theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} : Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective] 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 + IsBlock (H.map (MulEquiv.toMonoidHom (MulAut.conj g))) (g • B) := by rw [isBlock_iff_smul_eq_or_disjoint] intro h' obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h') @@ -317,6 +326,25 @@ theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g rw [← this]; rfl rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right] +theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate + {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] {B : Set X} + {H : AddSubgroup G} (hB : AddAction.IsBlock H B) (g : G) : + AddAction.IsBlock (H.map (AddEquiv.toAddMonoidHom (AddAut.conj g))) (g +ᵥ B) := by + rw [AddAction.isBlock_iff_vadd_eq_or_disjoint] + intro h' + obtain ⟨h, hH, hh⟩ := AddSubgroup.mem_map.mp (SetLike.coe_mem h') + simp only [AddEquiv.coe_toAddMonoidHom, AddAut.conj_apply] at hh + suffices h' +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by + simp only [this] + apply (hB.vadd_eq_or_disjoint ⟨h, hH⟩).imp + · intro hB'; congr + · exact Set.disjoint_image_of_injective (AddAction.injective g) + suffices (h' : G) +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by + exact this + rw [← hh, vadd_vadd, vadd_vadd] + erw [AddAut.conj_apply] + simp + /-- A translate of a block is a block -/ theorem IsBlock.translate (g : G) (hB : IsBlock G B) : IsBlock G (g • B) := by @@ -326,12 +354,26 @@ theorem IsBlock.translate (g : G) (hB : IsBlock G B) : apply IsBlock.of_subgroup_of_conjugate rwa [Subgroup.comap_top] +/-- A translate of a block is a block -/ +theorem _root_.AddAction.IsBlock.translate + {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] (B : Set X) + (g : G) (hB : AddAction.IsBlock G B) : + AddAction.IsBlock G (g +ᵥ B) := by + rw [← AddAction.isBlock_top] at hB ⊢ + rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤] + · apply AddAction.IsBlock.of_addsubgroup_of_conjugate + rwa [AddSubgroup.comap_top] + · exact (AddAut.conj g).surjective + variable (G) in /-- For `SMul G X`, a block system of `X` is a partition of `X` into blocks for the action of `G` -/ +@[to_additive "For `VAdd G X`, a block system of `X` is a partition of `X` into blocks + for the additive action of `G`"] def IsBlockSystem (ℬ : Set (Set X)) := Setoid.IsPartition ℬ ∧ ∀ ⦃B⦄, B ∈ ℬ → IsBlock G B /-- Translates of a block form a block system. -/ +@[to_additive] theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X] (hB : IsBlock G B) (hBe : B.Nonempty) : IsBlockSystem G (Set.range fun g : G => g • B) := by @@ -345,13 +387,14 @@ theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X] obtain ⟨b : X, hb : b ∈ B⟩ := hBe obtain ⟨g, rfl⟩ := exists_smul_eq G b a use g • B - simp only [Set.smul_mem_smul_set_iff, hb, existsUnique_iff_exists, Set.mem_range, + 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] exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩ section Normal +@[to_additive] lemma smul_orbit_eq_orbit_smul (N : Subgroup G) [nN : N.Normal] (a : X) (g : G) : g • orbit N a = orbit N (g • a) := by simp only [orbit, Set.image_smul, Set.smul_set_range] @@ -368,6 +411,7 @@ 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 -/ +@[to_additive] theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) : IsBlock G (orbit N a) := by rw [isBlock_iff_smul_eq_or_disjoint] @@ -376,6 +420,7 @@ theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) : apply orbit.eq_or_disjoint /-- The orbits of a normal subgroup form a block system -/ +@[to_additive] theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] : IsBlockSystem G (Set.range fun a : X => orbit N a) := by constructor @@ -436,6 +481,7 @@ section Stabilizer (Wielandt, th. 7.5) -/ /-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block -/ +@[to_additive] theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ H) : IsBlock G (MulAction.orbit H a) := by rw [isBlock_iff_smul_eq_of_nonempty] @@ -447,11 +493,13 @@ theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ 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` -/ +@[to_additive] 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 -/ +@[to_additive] 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 @@ -466,6 +514,7 @@ theorem IsBlock.orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a /-- A subgroup containing the stabilizer of `a` is the stabilizer of the orbit of `a` under that subgroup -/ +@[to_additive] theorem stabilizer_orbit_eq {a : X} {H : Subgroup G} (hH : stabilizer G a ≤ H) : stabilizer G (orbit H a) = H := by ext g @@ -482,6 +531,9 @@ variable (G) /-- Order equivalence between blocks in `X` containing a point `a` and subgroups of `G` containing the stabilizer of `a` (Wielandt, th. 7.5)-/ +@[to_additive + "Order equivalence between blocks in `X` containing a point `a` + and subgroups of `G` containing the stabilizer of `a` (Wielandt, th. 7.5)"] def block_stabilizerOrderIso [htGX : IsPretransitive G X] (a : X) : { B : Set X // a ∈ B ∧ IsBlock G B } ≃o Set.Ici (stabilizer G a) where toFun := fun ⟨B, ha, hB⟩ => ⟨stabilizer G B, hB.stabilizer_le ha⟩ @@ -512,6 +564,7 @@ namespace IsBlock variable [IsPretransitive G X] {B : Set X} +@[to_additive] theorem ncard_block_eq_relindex (hB : IsBlock G B) {x : X} (hx : x ∈ B) : B.ncard = (stabilizer G x).relindex (stabilizer G B) := by have key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (stabilizer G B) x := by @@ -520,6 +573,9 @@ theorem ncard_block_eq_relindex (hB : IsBlock G B) {x : X} (hx : x ∈ B) : /-- The cardinality of the ambient space is the product of the cardinality of a block by the cardinality of the set of translates of that block -/ +@[to_additive + "The cardinality of the ambient space is the product of the cardinality of a block + by the cardinality of the set of translates of that block"] theorem ncard_block_mul_ncard_orbit_eq (hB : IsBlock G B) (hB_ne : B.Nonempty) : Set.ncard B * Set.ncard (orbit G B) = Nat.card X := by obtain ⟨x, hx⟩ := hB_ne @@ -527,11 +583,13 @@ theorem ncard_block_mul_ncard_orbit_eq (hB : IsBlock G B) (hB_ne : B.Nonempty) : Subgroup.relindex_mul_index (hB.stabilizer_le hx), index_stabilizer_of_transitive] /-- The cardinality of a block divides the cardinality of the ambient type -/ +@[to_additive "The cardinality of a block divides the cardinality of the ambient type"] theorem ncard_dvd_card (hB : IsBlock G B) (hB_ne : B.Nonempty) : Set.ncard B ∣ Nat.card X := Dvd.intro _ (hB.ncard_block_mul_ncard_orbit_eq hB_ne) /-- A too large block is equal to `univ` -/ +@[to_additive "A too large block is equal to `univ`"] theorem eq_univ_of_card_lt [hX : Finite X] (hB : IsBlock G B) (hB' : Nat.card X < Set.ncard B * 2) : B = Set.univ := by rcases Set.eq_empty_or_nonempty B with rfl | hB_ne @@ -547,6 +605,7 @@ theorem eq_univ_of_card_lt [hX : Finite X] (hB : IsBlock G B) (hB' : Nat.card X @[deprecated (since := "2024-10-29")] alias eq_univ_card_lt := eq_univ_of_card_lt /-- If a block has too many translates, then it is a (sub)singleton -/ +@[to_additive "If a block has too many translates, then it is a (sub)singleton"] theorem subsingleton_of_card_lt [Finite X] (hB : IsBlock G B) (hB' : Nat.card X < 2 * Set.ncard (orbit G B)) : B.Subsingleton := by @@ -568,7 +627,10 @@ theorem subsingleton_of_card_lt [Finite X] (hB : IsBlock G B) are just `k + ℕ`, for `k ≤ 0`, and the corresponding intersection is `ℕ`, which is not a block. (Remark by Thomas Browning) -/ /-- The intersection of the translates of a *finite* subset which contain a given point -is a block (Wielandt, th. 7.3 )-/ +is a block (Wielandt, th. 7.3)-/ +@[to_additive + "The intersection of the translates of a *finite* subset which contain a given point + is a block (Wielandt, th. 7.3)"] theorem of_subset (a : X) (hfB : B.Finite) : IsBlock G (⋂ (k : G) (_ : a ∈ k • B), k • B) := by let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B From 1acc2cc44f6dcaac6e64157050e5c28fef3a38e1 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 5 Jan 2025 22:28:26 +0100 Subject: [PATCH 2/8] to additive GroupAction --- Mathlib/GroupTheory/GroupAction/Basic.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean index 552dee07b3bcd..ece1817463f7d 100644 --- a/Mathlib/GroupTheory/GroupAction/Basic.lean +++ b/Mathlib/GroupTheory/GroupAction/Basic.lean @@ -17,6 +17,13 @@ This file primarily concerns itself with orbits, stabilizers, and other objects actions. Despite this file being called `basic`, low-level helper lemmas for algebraic manipulation of `•` belong elsewhere. +## Main definitions + +* `MulAction.orbit` +* `MulAction.fixedPoints` +* `MulAction.fixedBy` +* `MulAction.stabilizer` + -/ @@ -62,6 +69,14 @@ section FixedPoints variable {M α} +@[to_additive] theorem mem_fixedPoints_iff_subsingleton_orbit {a : α} : + a ∈ fixedPoints M α ↔ (orbit M a).Subsingleton := by + rw [mem_fixedPoints] + constructor + · rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩ + simp only [h] + · exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a) + @[to_additive mem_fixedPoints_iff_card_orbit_eq_one] theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] : a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1 := by @@ -266,6 +281,8 @@ namespace MulAction variable {G : Type*} [Group G] {α : Type*} [MulAction G α] /-- To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions.-/ +@[to_additive + "To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions."] theorem le_stabilizer_iff_smul_le (s : Set α) (H : Subgroup G) : H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s := by constructor From e51ecb782b179b7db6ae3c649c92aa594b2f4ff9 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 5 Jan 2025 22:29:29 +0100 Subject: [PATCH 3/8] to additive Pointwise --- Mathlib/GroupTheory/GroupAction/Pointwise.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/GroupAction/Pointwise.lean b/Mathlib/GroupTheory/GroupAction/Pointwise.lean index 3b3918cc93570..4336d49f895c7 100644 --- a/Mathlib/GroupTheory/GroupAction/Pointwise.lean +++ b/Mathlib/GroupTheory/GroupAction/Pointwise.lean @@ -29,6 +29,7 @@ import Mathlib.GroupTheory.GroupAction.Hom open Set Pointwise +@[to_additive] theorem MulAction.smul_bijective_of_is_unit {M : Type*} [Monoid M] {α : Type*} [MulAction M α] {m : M} (hm : IsUnit m) : Function.Bijective (fun (a : α) ↦ m • a) := by @@ -54,11 +55,13 @@ variable [FunLike F M N] [MulActionSemiHomClass F σ M N] -- "Left-hand side does not simplify, when using the simp lemma on itself." -- For now we will have to manually add `image_smul_setₛₗ _` to the `simp` argument list. -- TODO: when https://github.com/leanprover/lean4/issues/3107 is fixed, mark this as `@[simp]`. +@[to_additive] theorem image_smul_setₛₗ : h '' (c • s) = σ c • h '' s := by simp only [← image_smul, image_image, map_smulₛₗ h] /-- Translation of preimage is contained in preimage of translation -/ +@[to_additive] theorem smul_preimage_set_leₛₗ : c • h ⁻¹' t ⊆ h ⁻¹' (σ c • t) := by rintro x ⟨y, hy, rfl⟩ @@ -67,6 +70,7 @@ theorem smul_preimage_set_leₛₗ : variable {c} /-- General version of `preimage_smul_setₛₗ` -/ +@[to_additive] theorem preimage_smul_setₛₗ' (hc : Function.Surjective (fun (m : M) ↦ c • m)) (hc' : Function.Injective (fun (n : N) ↦ σ c • n)) : @@ -82,6 +86,7 @@ theorem preimage_smul_setₛₗ' · exact smul_preimage_set_leₛₗ M N σ h c t /-- `preimage_smul_setₛₗ` when both scalars act by unit -/ +@[to_additive] theorem preimage_smul_setₛₗ_of_units (hc : IsUnit c) (hc' : IsUnit (σ c)) : h ⁻¹' (σ c • t) = c • h ⁻¹' t := by apply preimage_smul_setₛₗ' @@ -90,6 +95,7 @@ theorem preimage_smul_setₛₗ_of_units (hc : IsUnit c) (hc' : IsUnit (σ c)) : /-- `preimage_smul_setₛₗ` in the context of a `MonoidHom` -/ +@[to_additive] theorem MonoidHom.preimage_smul_setₛₗ (σ : R →* S) {F : Type*} [FunLike F M N] [MulActionSemiHomClass F ⇑σ M N] (h : F) {c : R} (hc : IsUnit c) (t : Set N) : @@ -97,6 +103,7 @@ theorem MonoidHom.preimage_smul_setₛₗ (σ : R →* S) preimage_smul_setₛₗ_of_units M N σ h t hc (IsUnit.map σ hc) /-- `preimage_smul_setₛₗ` in the context of a `MonoidHomClass` -/ +@[to_additive] theorem preimage_smul_setₛₗ {G : Type*} [FunLike G R S] [MonoidHomClass G R S] (σ : G) {F : Type*} [FunLike F M N] [MulActionSemiHomClass F σ M N] (h : F) @@ -105,6 +112,7 @@ theorem preimage_smul_setₛₗ MonoidHom.preimage_smul_setₛₗ M N (σ : R →* S) h hc t /-- `preimage_smul_setₛₗ` in the context of a groups -/ +@[to_additive] theorem Group.preimage_smul_setₛₗ {R S : Type*} [Group R] [Group S] (σ : R → S) [MulAction R M] [MulAction S N] @@ -121,21 +129,25 @@ variable (R) variable [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂] (c : R) (s : Set M₁) (t : Set M₂) -@[simp] -- This can be safely removed as a `@[simp]` lemma if `image_smul_setₛₗ` is readded. +-- This can be safely removed as a `@[simp]` lemma if `image_smul_setₛₗ` is readded. +@[to_additive, simp] theorem image_smul_set : h '' (c • s) = c • h '' s := image_smul_setₛₗ _ _ _ h c s +@[to_additive] theorem smul_preimage_set_le : c • h ⁻¹' t ⊆ h ⁻¹' (c • t) := smul_preimage_set_leₛₗ _ _ _ h c t variable {c} +@[to_additive] theorem preimage_smul_set (hc : IsUnit c) : h ⁻¹' (c • t) = c • h ⁻¹' t := preimage_smul_setₛₗ_of_units _ _ _ h t hc hc +@[to_additive] theorem Group.preimage_smul_set {R : Type*} [Group R] (M₁ M₂ : Type*) [MulAction R M₁] [MulAction R M₂] From 858d1e4da75bda029b90d70da3886bb4aa022214 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 5 Jan 2025 22:32:47 +0100 Subject: [PATCH 4/8] to additive SubMulAction --- .../GroupTheory/GroupAction/SubMulAction.lean | 58 ++++++++++++++++--- 1 file changed, 49 insertions(+), 9 deletions(-) diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean index babd428140d21..1a4ea96057aad 100644 --- a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean +++ b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean @@ -161,41 +161,57 @@ structure SubMulAction (R : Type u) (M : Type v) [SMul R M] : Type v where /-- The carrier set is closed under scalar multiplication. -/ smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier +/-- A SubAddAction is a set which is closed under scalar multiplication. -/ +structure SubAddAction (R : Type u) (M : Type v) [VAdd R M] : Type v where + /-- The underlying set of a `SubAddAction`. -/ + carrier : Set M + /-- The carrier set is closed under scalar multiplication. -/ + vadd_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c +ᵥ x ∈ carrier + +attribute [to_additive] SubMulAction + namespace SubMulAction variable [SMul R M] +@[to_additive] instance : SetLike (SubMulAction R M) M := ⟨SubMulAction.carrier, fun p q h => by cases p; cases q; congr⟩ +@[to_additive] instance : SMulMemClass (SubMulAction R M) R M where smul_mem := smul_mem' _ -@[simp] +@[to_additive, simp] theorem mem_carrier {p : SubMulAction R M} {x : M} : x ∈ p.carrier ↔ x ∈ (p : Set M) := Iff.rfl -@[ext] +@[to_additive (attr := ext)] theorem ext {p q : SubMulAction R M} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := SetLike.ext h /-- Copy of a sub_mul_action with a new `carrier` equal to the old one. Useful to fix definitional equalities. -/ +@[to_additive "Copy of a sub_mul_action with a new `carrier` equal to the old one. + Useful to fix definitional equalities."] protected def copy (p : SubMulAction R M) (s : Set M) (hs : s = ↑p) : SubMulAction R M where carrier := s smul_mem' := hs.symm ▸ p.smul_mem' -@[simp] +@[to_additive, simp] theorem coe_copy (p : SubMulAction R M) (s : Set M) (hs : s = ↑p) : (p.copy s hs : Set M) = s := rfl +@[to_additive] theorem copy_eq (p : SubMulAction R M) (s : Set M) (hs : s = ↑p) : p.copy s hs = p := SetLike.coe_injective hs +@[to_additive] instance : Bot (SubMulAction R M) where bot := { carrier := ∅ smul_mem' := fun _c h => Set.not_mem_empty h } +@[to_additive] instance : Inhabited (SubMulAction R M) := ⟨⊥⟩ @@ -209,14 +225,16 @@ variable [SMul R M] variable (p : SubMulAction R M) variable {r : R} {x : M} +@[to_additive] theorem smul_mem (r : R) (h : x ∈ p) : r • x ∈ p := p.smul_mem' r h +@[to_additive] instance : SMul R p where smul c x := ⟨c • x.1, smul_mem _ c x.2⟩ variable {p} -@[simp, norm_cast] +@[to_additive (attr := norm_cast), simp] theorem val_smul (r : R) (x : p) : (↑(r • x) : M) = r • (x : M) := rfl @@ -225,14 +243,16 @@ theorem val_smul (r : R) (x : p) : (↑(r • x) : M) = r • (x : M) := variable (p) /-- Embedding of a submodule `p` to the ambient space `M`. -/ +@[to_additive "Embedding of a submodule `p` to the ambient space `M`."] protected def subtype : p →[R] M where toFun := Subtype.val map_smul' := by simp [val_smul] -@[simp] +@[to_additive, simp] theorem subtype_apply (x : p) : p.subtype x = x := rfl +@[to_additive] theorem subtype_eq_val : (SubMulAction.subtype p : p → M) = Subtype.val := rfl @@ -245,14 +265,16 @@ variable [hA : SMulMemClass A R M] (S' : A) -- Prefer subclasses of `MulAction` over `SMulMemClass`. /-- A `SubMulAction` of a `MulAction` is a `MulAction`. -/ +@[to_additive "A `SubAddAction` of an `AddAction` is an `AddAction`."] instance (priority := 75) toMulAction : MulAction R S' := Subtype.coe_injective.mulAction Subtype.val (SetLike.val_smul S') /-- The natural `MulActionHom` over `R` from a `SubMulAction` of `M` to `M`. -/ +@[to_additive "The natural `AddActionHom` over `R` from a `SubAddAction` of `M` to `M`."] protected def subtype : S' →[R] M where toFun := Subtype.val; map_smul' _ _ := rfl -@[simp] +@[to_additive, simp] protected theorem coeSubtype : (SMulMemClass.subtype S' : S' → M) = Subtype.val := rfl @@ -267,28 +289,33 @@ section variable [SMul S R] [SMul S M] [IsScalarTower S R M] variable (p : SubMulAction R M) +@[to_additive] theorem smul_of_tower_mem (s : S) {x : M} (h : x ∈ p) : s • x ∈ p := by rw [← one_smul R x, ← smul_assoc] exact p.smul_mem _ h +@[to_additive] instance smul' : SMul S p where smul c x := ⟨c • x.1, smul_of_tower_mem _ c x.2⟩ +@[to_additive] instance isScalarTower : IsScalarTower S R p where smul_assoc s r x := Subtype.ext <| smul_assoc s r (x : M) +@[to_additive] instance isScalarTower' {S' : Type*} [SMul S' R] [SMul S' S] [SMul S' M] [IsScalarTower S' R M] [IsScalarTower S' S M] : IsScalarTower S' S p where smul_assoc s r x := Subtype.ext <| smul_assoc s r (x : M) -@[simp, norm_cast] +@[to_additive (attr := norm_cast), simp] theorem val_smul_of_tower (s : S) (x : p) : ((s • x : p) : M) = s • (x : M) := rfl -@[simp] +@[to_additive, simp] theorem smul_mem_iff' {G} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) {x : M} : g • x ∈ p ↔ x ∈ p := ⟨fun h => inv_smul_smul g x ▸ p.smul_of_tower_mem g⁻¹ h, p.smul_of_tower_mem g⟩ +@[to_additive] instance isCentralScalar [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S p where @@ -302,17 +329,20 @@ variable [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] variable (p : SubMulAction R M) /-- If the scalar product forms a `MulAction`, then the subset inherits this action -/ +@[to_additive] instance mulAction' : MulAction S p where smul := (· • ·) one_smul x := Subtype.ext <| one_smul _ (x : M) mul_smul c₁ c₂ x := Subtype.ext <| mul_smul c₁ c₂ (x : M) +@[to_additive] instance mulAction : MulAction R p := p.mulAction' end /-- Orbits in a `SubMulAction` coincide with orbits in the ambient space. -/ +@[to_additive] theorem val_image_orbit {p : SubMulAction R M} (m : p) : Subtype.val '' MulAction.orbit R m = MulAction.orbit R (m : M) := (Set.range_comp _ _).symm @@ -322,15 +352,18 @@ lemma orbit_of_sub_mul {p : SubMulAction R M} (m : p) : (mul_action.orbit R m : set M) = MulAction.orbit R (m : M) := rfl -/ +@[to_additive] theorem val_preimage_orbit {p : SubMulAction R M} (m : p) : Subtype.val ⁻¹' MulAction.orbit R (m : M) = MulAction.orbit R m := by rw [← val_image_orbit, Subtype.val_injective.preimage_image] +@[to_additive] lemma mem_orbit_subMul_iff {p : SubMulAction R M} {x m : p} : x ∈ MulAction.orbit R m ↔ (x : M) ∈ MulAction.orbit R (m : M) := by rw [← val_preimage_orbit, Set.mem_preimage] /-- Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space -/ +@[to_additive] theorem stabilizer_of_subMul.submonoid {p : SubMulAction R M} (m : p) : MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R (m : M) := by ext @@ -342,6 +375,7 @@ section MulActionGroup variable [Group R] [MulAction R M] +@[to_additive] lemma orbitRel_of_subMul (p : SubMulAction R M) : MulAction.orbitRel R p = (MulAction.orbitRel R M).comap Subtype.val := by refine Setoid.ext_iff.2 (fun x y ↦ ?_) @@ -349,9 +383,10 @@ lemma orbitRel_of_subMul (p : SubMulAction R M) : exact mem_orbit_subMul_iff /-- Stabilizers in group SubMulAction coincide with stabilizers in the ambient space -/ +@[to_additive] theorem stabilizer_of_subMul {p : SubMulAction R M} (m : p) : MulAction.stabilizer R m = MulAction.stabilizer R (m : M) := by - rw [← Subgroup.toSubmonoid_inj] + rw [← Subgroup.toSubmonoid_eq] exact stabilizer_of_subMul.submonoid m end MulActionGroup @@ -419,23 +454,28 @@ variable {M α : Type*} [Monoid M] [MulAction M α] /-- The inclusion of a SubMulAction into the ambient set, as an equivariant map -/ +@[to_additive "The inclusion of a SubAddAction into the ambient set, as an equivariant map."] def inclusion (s : SubMulAction M α) : s →[M] α where -- The inclusion map of the inclusion of a SubMulAction toFun := Subtype.val -- The commutation property map_smul' _ _ := rfl +@[to_additive] theorem inclusion.toFun_eq_coe (s : SubMulAction M α) : s.inclusion.toFun = Subtype.val := rfl +@[to_additive] theorem inclusion.coe_eq (s : SubMulAction M α) : ⇑s.inclusion = Subtype.val := rfl +@[to_additive] lemma image_inclusion (s : SubMulAction M α) : Set.range s.inclusion = s.carrier := by rw [inclusion.coe_eq] exact Subtype.range_coe +@[to_additive] lemma inclusion_injective (s : SubMulAction M α) : Function.Injective s.inclusion := Subtype.val_injective From d996233d0020e04fca650e14a677c099517b67a8 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Mon, 6 Jan 2025 09:09:28 +0100 Subject: [PATCH 5/8] adjust attr=simp and remove one lemma --- Mathlib/GroupTheory/GroupAction/Basic.lean | 8 -------- Mathlib/GroupTheory/GroupAction/Pointwise.lean | 2 +- Mathlib/GroupTheory/GroupAction/SubMulAction.lean | 14 +++++++------- 3 files changed, 8 insertions(+), 16 deletions(-) diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean index ece1817463f7d..520ead2860814 100644 --- a/Mathlib/GroupTheory/GroupAction/Basic.lean +++ b/Mathlib/GroupTheory/GroupAction/Basic.lean @@ -69,14 +69,6 @@ section FixedPoints variable {M α} -@[to_additive] theorem mem_fixedPoints_iff_subsingleton_orbit {a : α} : - a ∈ fixedPoints M α ↔ (orbit M a).Subsingleton := by - rw [mem_fixedPoints] - constructor - · rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩ - simp only [h] - · exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a) - @[to_additive mem_fixedPoints_iff_card_orbit_eq_one] theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] : a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1 := by diff --git a/Mathlib/GroupTheory/GroupAction/Pointwise.lean b/Mathlib/GroupTheory/GroupAction/Pointwise.lean index 4336d49f895c7..291344f1d949b 100644 --- a/Mathlib/GroupTheory/GroupAction/Pointwise.lean +++ b/Mathlib/GroupTheory/GroupAction/Pointwise.lean @@ -130,7 +130,7 @@ variable [FunLike F M₁ M₂] [MulActionHomClass F R M₁ M₂] (c : R) (s : Set M₁) (t : Set M₂) -- This can be safely removed as a `@[simp]` lemma if `image_smul_setₛₗ` is readded. -@[to_additive, simp] +@[to_additive (attr := simp)] theorem image_smul_set : h '' (c • s) = c • h '' s := image_smul_setₛₗ _ _ _ h c s diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean index 1a4ea96057aad..af9010ec96ce1 100644 --- a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean +++ b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean @@ -181,7 +181,7 @@ instance : SetLike (SubMulAction R M) M := @[to_additive] instance : SMulMemClass (SubMulAction R M) R M where smul_mem := smul_mem' _ -@[to_additive, simp] +@[to_additive (attr := simp)] theorem mem_carrier {p : SubMulAction R M} {x : M} : x ∈ p.carrier ↔ x ∈ (p : Set M) := Iff.rfl @@ -197,7 +197,7 @@ protected def copy (p : SubMulAction R M) (s : Set M) (hs : s = ↑p) : SubMulAc carrier := s smul_mem' := hs.symm ▸ p.smul_mem' -@[to_additive, simp] +@[to_additive (attr := simp)] theorem coe_copy (p : SubMulAction R M) (s : Set M) (hs : s = ↑p) : (p.copy s hs : Set M) = s := rfl @@ -234,7 +234,7 @@ instance : SMul R p where smul c x := ⟨c • x.1, smul_mem _ c x.2⟩ variable {p} -@[to_additive (attr := norm_cast), simp] +@[to_additive (attr := norm_cast, simp)] theorem val_smul (r : R) (x : p) : (↑(r • x) : M) = r • (x : M) := rfl @@ -248,7 +248,7 @@ protected def subtype : p →[R] M where toFun := Subtype.val map_smul' := by simp [val_smul] -@[to_additive, simp] +@[to_additive (attr := simp)] theorem subtype_apply (x : p) : p.subtype x = x := rfl @@ -274,7 +274,7 @@ instance (priority := 75) toMulAction : MulAction R S' := protected def subtype : S' →[R] M where toFun := Subtype.val; map_smul' _ _ := rfl -@[to_additive, simp] +@[to_additive (attr := simp)] protected theorem coeSubtype : (SMulMemClass.subtype S' : S' → M) = Subtype.val := rfl @@ -306,11 +306,11 @@ instance isScalarTower' {S' : Type*} [SMul S' R] [SMul S' S] [SMul S' M] [IsScal [IsScalarTower S' S M] : IsScalarTower S' S p where smul_assoc s r x := Subtype.ext <| smul_assoc s r (x : M) -@[to_additive (attr := norm_cast), simp] +@[to_additive (attr := norm_cast, simp)] theorem val_smul_of_tower (s : S) (x : p) : ((s • x : p) : M) = s • (x : M) := rfl -@[to_additive, simp] +@[to_additive (attr := simp)] theorem smul_mem_iff' {G} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) {x : M} : g • x ∈ p ↔ x ∈ p := ⟨fun h => inv_smul_smul g x ▸ p.smul_of_tower_mem g⁻¹ h, p.smul_of_tower_mem g⟩ From 47135a91882e9bd03890271323d8ecab8e617d22 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Mon, 6 Jan 2025 10:42:11 +0100 Subject: [PATCH 6/8] add one forgotten to_additive --- Mathlib/GroupTheory/GroupAction/Blocks.lean | 2 +- Mathlib/GroupTheory/Index.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean index e14a65eafc8bf..803c319c72f01 100644 --- a/Mathlib/GroupTheory/GroupAction/Blocks.lean +++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean @@ -387,7 +387,7 @@ theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X] obtain ⟨b : X, hb : b ∈ B⟩ := hBe obtain ⟨g, rfl⟩ := exists_smul_eq G b a use g • B - simp only [Set.smul_mem_smul_set_iff, hb, exists_unique_iff_exists, Set.mem_range, + simp only [Set.smul_mem_smul_set_iff, hb, existsUnique_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] exact fun g' ha ↦ hB.smul_eq_smul_of_nonempty ⟨g • b, ha, ⟨b, hb, rfl⟩⟩ diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean index 6ad32109acca6..f8e36f80728c3 100644 --- a/Mathlib/GroupTheory/Index.lean +++ b/Mathlib/GroupTheory/Index.lean @@ -617,12 +617,12 @@ namespace MulAction variable (G : Type*) {X : Type*} [Group G] [MulAction G X] (x : X) -theorem index_stabilizer : +@[to_additive] theorem index_stabilizer : (stabilizer G x).index = (orbit G x).ncard := (Nat.card_congr (MulAction.orbitEquivQuotientStabilizer G x)).symm.trans (Set.Nat.card_coe_set_eq (orbit G x)) -theorem index_stabilizer_of_transitive [IsPretransitive G X] : +@[to_additive] theorem index_stabilizer_of_transitive [IsPretransitive G X] : (stabilizer G x).index = Nat.card X := by rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ] From e02914a716e6647b1b67922f1fb0a7945249b4fd Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Mon, 6 Jan 2025 11:24:47 +0100 Subject: [PATCH 7/8] adjust one deprecated lemma --- Mathlib/GroupTheory/GroupAction/SubMulAction.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean index af9010ec96ce1..d8e3ff10ecc68 100644 --- a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean +++ b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean @@ -386,7 +386,7 @@ lemma orbitRel_of_subMul (p : SubMulAction R M) : @[to_additive] theorem stabilizer_of_subMul {p : SubMulAction R M} (m : p) : MulAction.stabilizer R m = MulAction.stabilizer R (m : M) := by - rw [← Subgroup.toSubmonoid_eq] + rw [← Subgroup.toSubmonoid_inj] exact stabilizer_of_subMul.submonoid m end MulActionGroup From dde6eb392759e4d146c4153020d9cd0153f47823 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Mon, 6 Jan 2025 15:20:21 +0100 Subject: [PATCH 8/8] add doc, better formatting --- Mathlib/GroupTheory/GroupAction/Blocks.lean | 83 +++++++++++---------- 1 file changed, 44 insertions(+), 39 deletions(-) diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean index 803c319c72f01..59f18a034ab8f 100644 --- a/Mathlib/GroupTheory/GroupAction/Blocks.lean +++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean @@ -15,26 +15,26 @@ import Mathlib.Tactic.IntervalCases Given `SMul G X`, an action of a type `G` on a type `X`, we define - the predicate `IsBlock G B` states that `B : Set X` is a block, -which means that the sets `g • B`, for `g ∈ G`, are equal or disjoint. -Under `Group G` and `MulAction G X`, this is equivalent to the classical -definition `MulAction.IsBlock.def_one` + which means that the sets `g • B`, for `g ∈ G`, are equal or disjoint. + Under `Group G` and `MulAction G X`, this is equivalent to the classical + definition `MulAction.IsBlock.def_one` - a bunch of lemmas that give examples of “trivial” blocks : ⊥, ⊤, singletons, -and non trivial blocks: orbit of the group, orbit of a normal subgroup… + and non trivial blocks: orbit of the group, orbit of a normal subgroup… The non-existence of nontrivial blocks is the definition of primitive actions. ## Results for actions on finite sets - `IsBlock.ncard_block_mul_ncard_orbit_eq` : The cardinality of a block -multiplied by the number of its translates is the cardinal of the ambient type + multiplied by the number of its translates is the cardinal of the ambient type - `IsBlock.eq_univ_of_card_lt` : a too large block is equal to `Set.univ` - `IsBlock.subsingleton_of_card_lt` : a too small block is a subsingleton - `IsBlock.of_subset` : the intersections of the translates of a finite subset -that contain a given point is a block + that contain a given point is a block ## References @@ -65,7 +65,7 @@ theorem orbit.pairwiseDisjoint : exact (orbit.eq_or_disjoint x y).resolve_right h /-- Orbits of an element form a partition -/ -@[to_additive] +@[to_additive "Orbits of an element of a partition"] theorem IsPartition.of_orbits : Setoid.IsPartition (Set.range fun a : X => orbit G a) := by apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty @@ -311,25 +311,10 @@ theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} : 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] -theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g : G) : - IsBlock (H.map (MulEquiv.toMonoidHom (MulAut.conj g))) (g • B) := by - 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 - suffices h' • g • B = g • h • B by - simp only [this] - apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp - · intro; congr - · exact Set.disjoint_image_of_injective (MulAction.injective g) - suffices (h' : G) • g • B = g • h • B by - rw [← this]; rfl - rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right] - theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] {B : Set X} {H : AddSubgroup G} (hB : AddAction.IsBlock H B) (g : G) : - AddAction.IsBlock (H.map (AddEquiv.toAddMonoidHom (AddAut.conj g))) (g +ᵥ B) := by + AddAction.IsBlock (H.map (AddAut.conj g).toAddMonoidHom) (g +ᵥ B) := by rw [AddAction.isBlock_iff_vadd_eq_or_disjoint] intro h' obtain ⟨h, hH, hh⟩ := AddSubgroup.mem_map.mp (SetLike.coe_mem h') @@ -345,14 +330,21 @@ theorem _root_.AddAction.IsBlock.of_addsubgroup_of_conjugate erw [AddAut.conj_apply] simp -/-- A translate of a block is a block -/ -theorem IsBlock.translate (g : G) (hB : IsBlock G B) : - IsBlock G (g • B) := by - rw [← isBlock_top] at hB ⊢ - rw [← Subgroup.map_comap_eq_self_of_surjective - (G := G) (f := MulAut.conj g) (MulAut.conj g).surjective ⊤] - apply IsBlock.of_subgroup_of_conjugate - rwa [Subgroup.comap_top] +@[to_additive existing AddAction.IsBlock.of_addsubgroup_of_conjugate] +theorem IsBlock.of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g : G) : + IsBlock (H.map (MulAut.conj g).toMonoidHom) (g • B) := by + 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 + suffices h' • g • B = g • h • B by + simp only [this] + apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp + · intro; congr + · exact Set.disjoint_image_of_injective (MulAction.injective g) + suffices (h' : G) • g • B = g • h • B by + rw [← this]; rfl + 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 _root_.AddAction.IsBlock.translate @@ -365,6 +357,16 @@ theorem _root_.AddAction.IsBlock.translate rwa [AddSubgroup.comap_top] · exact (AddAut.conj g).surjective +/-- A translate of a block is a block -/ +@[to_additive existing] +theorem IsBlock.translate (g : G) (hB : IsBlock G B) : + IsBlock G (g • B) := by + rw [← isBlock_top] at hB ⊢ + rw [← Subgroup.map_comap_eq_self_of_surjective + (G := G) (f := MulAut.conj g) (MulAut.conj g).surjective ⊤] + apply IsBlock.of_subgroup_of_conjugate + rwa [Subgroup.comap_top] + variable (G) in /-- For `SMul G X`, a block system of `X` is a partition of `X` into blocks for the action of `G` -/ @@ -372,8 +374,8 @@ variable (G) in for the additive action of `G`"] def IsBlockSystem (ℬ : Set (Set X)) := Setoid.IsPartition ℬ ∧ ∀ ⦃B⦄, B ∈ ℬ → IsBlock G B -/-- Translates of a block form a block system. -/ -@[to_additive] +/-- Translates of a block form a block system -/ +@[to_additive "Translates of a block form a block system"] theorem IsBlock.isBlockSystem [hGX : MulAction.IsPretransitive G X] (hB : IsBlock G B) (hBe : B.Nonempty) : IsBlockSystem G (Set.range fun g : G => g • B) := by @@ -411,7 +413,7 @@ 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 -/ -@[to_additive] +@[to_additive "An orbit of a normal subgroup is a block"] theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) : IsBlock G (orbit N a) := by rw [isBlock_iff_smul_eq_or_disjoint] @@ -420,7 +422,7 @@ theorem IsBlock.orbit_of_normal {N : Subgroup G} [N.Normal] (a : X) : apply orbit.eq_or_disjoint /-- The orbits of a normal subgroup form a block system -/ -@[to_additive] +@[to_additive "The orbits of a normal subgroup form a block system"] theorem IsBlockSystem.of_normal {N : Subgroup G} [N.Normal] : IsBlockSystem G (Set.range fun a : X => orbit N a) := by constructor @@ -481,7 +483,7 @@ section Stabilizer (Wielandt, th. 7.5) -/ /-- The orbit of `a` under a subgroup containing the stabilizer of `a` is a block -/ -@[to_additive] +@[to_additive "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 rw [isBlock_iff_smul_eq_of_nonempty] @@ -493,13 +495,14 @@ theorem IsBlock.of_orbit {H : Subgroup G} {a : X} (hH : stabilizer G a ≤ 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` -/ -@[to_additive] +@[to_additive + "If `B` is a block containing `a`, then the stabilizer of `B` contains the stabilizer of `a`"] 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 -/ -@[to_additive] +@[to_additive "A block containing `a` is the orbit of `a` under its stabilizer"] 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 @@ -514,7 +517,9 @@ theorem IsBlock.orbit_stabilizer_eq [IsPretransitive G X] (hB : IsBlock G B) {a /-- A subgroup containing the stabilizer of `a` is the stabilizer of the orbit of `a` under that subgroup -/ -@[to_additive] +@[to_additive + "A subgroup containing the stabilizer of `a` + is the stabilizer of the orbit of `a` under that subgroup"] theorem stabilizer_orbit_eq {a : X} {H : Subgroup G} (hH : stabilizer G a ≤ H) : stabilizer G (orbit H a) = H := by ext g