feat(GroupTheory/GroupAction/Primitive)

Mathlib.lean

@@ -352,7 +352,6 @@ import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.Injective
 import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.Algebra.Module.LinearMap.End
-import Mathlib.Algebra.Module.LinearMap.Pointwise
 import Mathlib.Algebra.Module.LocalizedModule
 import Mathlib.Algebra.Module.MinimalAxioms
 import Mathlib.Algebra.Module.Opposites
@@ -2366,6 +2365,7 @@ import Mathlib.GroupTheory.FreeGroup.IsFreeGroup
 import Mathlib.GroupTheory.FreeGroup.NielsenSchreier
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.BigOperators
+import Mathlib.GroupTheory.GroupAction.Blocks
 import Mathlib.GroupTheory.GroupAction.ConjAct
 import Mathlib.GroupTheory.GroupAction.Defs
 import Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
@@ -2379,6 +2379,7 @@ import Mathlib.GroupTheory.GroupAction.Opposite
 import Mathlib.GroupTheory.GroupAction.Option
 import Mathlib.GroupTheory.GroupAction.Period
 import Mathlib.GroupTheory.GroupAction.Pi
+import Mathlib.GroupTheory.GroupAction.Pointwise
 import Mathlib.GroupTheory.GroupAction.Prod
 import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.GroupTheory.GroupAction.Ring

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Moritz Doll. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Doll
 -/
-import Mathlib.Algebra.Module.LinearMap.Pointwise
+import Mathlib.GroupTheory.GroupAction.Pointwise
 import Mathlib.Analysis.LocallyConvex.Basic
 import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 import Mathlib.Analysis.Seminorm

Mathlib/Data/Set/Pointwise/SMul.lean

@@ -1034,6 +1034,22 @@ lemma inv_op_smul_set_distrib (a : α) (s : Set α) : (op a • s)⁻¹ = a⁻¹
 lemma smul_set_disjoint_iff : Disjoint (a • s) (a • t) ↔ Disjoint s t := by
   simp [disjoint_iff, ← smul_set_inter]
 
+example (a : α) (s : Set β) : a • s = (fun b ↦ a • b) '' s := by
+  rw [@image_smul]
+
+@[to_additive]
+lemma smul_set_iInter {ι : Type*} (a : α) (s : ι → Set β) :
+    (a • ⋂ i, s i) = ⋂ i, a • s i := by
+  obtain _ | _ := isEmpty_or_nonempty ι
+  · refine' Eq.trans _ (Set.iInter_of_empty _).symm
+    rw [Set.iInter_of_empty]
+    exact Set.smul_set_univ
+  · rw [← image_smul, Set.InjOn.image_iInter_eq ?_]
+    simp only [image_smul]
+    apply Function.Injective.injOn
+    intro x y
+    simp only [smul_left_cancel_iff, imp_self]
+
 end Group
 
 section GroupWithZero

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.Data.Setoid.Basic
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.GroupTheory.Subgroup.Basic
+import Mathlib.Data.Set.Finite
 
 #align_import group_theory.group_action.basic from "leanprover-community/mathlib"@"d30d31261cdb4d2f5e612eabc3c4bf45556350d5"
 
@@ -679,3 +680,50 @@ theorem Equiv.swap_mem_stabilizer {α : Type*} [DecidableEq α] {S : Set α} {a
   rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]
   simp_rw [Set.mem_inv_smul_set_iff, Perm.smul_def, swap_apply_def]
   exact ⟨fun h ↦ by simpa [Iff.comm] using h a, by intros; split_ifs <;> simp [*]⟩
+
+
+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.-/
+theorem le_stabilizer_iff_smul_le (s : Set α) (H : Subgroup G) :
+    H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s := by
+  constructor
+  · intro hyp g hg
+    apply Eq.subset
+    rw [← mem_stabilizer_iff]
+    exact hyp hg
+  intro hyp
+  intro g hg
+  rw [mem_stabilizer_iff]
+  apply subset_antisymm
+  exact hyp g hg
+  intro x hx; use g⁻¹ • x; constructor
+  apply hyp g⁻¹ (inv_mem hg)
+  simp only [Set.smul_mem_smul_set_iff, hx]
+  simp only [smul_inv_smul]
+
+/-- To prove membership to stabilizer of a *finite set*, it is enough to prove one inclusion. -/
+theorem mem_stabilizer_of_finite_iff_smul_le (s : Set α) (hs : s.Finite) (g : G) :
+    g ∈ stabilizer G s ↔ g • s ⊆ s := by
+  haveI : Fintype s := Set.Finite.fintype hs
+  haveI : Fintype (g • s : Set α) := Fintype.ofFinite _
+  rw [mem_stabilizer_iff]
+  constructor
+  exact Eq.subset
+  · rw [← Set.toFinset_inj, ← Set.toFinset_subset_toFinset]
+    intro h
+    apply Finset.eq_of_subset_of_card_le h
+    apply le_of_eq
+    suffices (g • s).toFinset = Finset.map ⟨_, MulAction.injective g⟩ hs.toFinset by
+      rw [this, Finset.card_map, Set.toFinite_toFinset]
+    rw [← Finset.coe_inj]
+    simp only [Set.coe_toFinset, Set.toFinite_toFinset, Finset.coe_map,
+      Function.Embedding.coeFn_mk, Set.image_smul]
+
+/-- To prove membership to stabilizer of a *finite set*, it is enough to prove one inclusion. -/
+theorem mem_stabilizer_of_finite_iff_le_smul (s : Set α) (hs : s.Finite) (g : G) :
+    g ∈ stabilizer G s ↔ s ⊆ g • s := by
+  rw [← @inv_mem_iff, mem_stabilizer_of_finite_iff_smul_le s hs]
+  exact Set.subset_set_smul_iff.symm