feat: Port/GroupTheory.GroupAction.FixingSubgroup (#1868)

port of group_theory.group_action.fixing_subgroup



Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib.lean

@@ -561,6 +561,7 @@ import Mathlib.GroupTheory.GroupAction.BigOperators
 import Mathlib.GroupTheory.GroupAction.ConjAct
 import Mathlib.GroupTheory.GroupAction.Defs
 import Mathlib.GroupTheory.GroupAction.Embedding
+import Mathlib.GroupTheory.GroupAction.FixingSubgroup
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Opposite
 import Mathlib.GroupTheory.GroupAction.Option

Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean

@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2022 Antoine Chambert-Loir. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Chambert-Loir
+
+! This file was ported from Lean 3 source module group_theory.group_action.fixing_subgroup
+! leanprover-community/mathlib commit f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.GroupTheory.Subgroup.Actions
+import Mathlib.GroupTheory.GroupAction.Basic
+
+/-!
+
+# Fixing submonoid, fixing subgroup of an action
+
+In the presence of of an action of a monoid or a group,
+this file defines the fixing submonoid or the fixing subgroup,
+and relates it to the set of fixed points via a Galois connection.
+
+## Main definitions
+
+* `fixingSubmonoid M s` : in the presence of `MulAction M α` (with `monoid M`)
+  it is the `Submonoid M` consisting of elements which fix `s : Set α` pointwise.
+
+* `fixingSubmonoid_fixedPoints_gc M α` is the `GaloisConnection`
+  that relates `fixingSubmonoid` with `fixedPoints`.
+
+* `fixingSubgroup M s` : in the presence of `MulAction M α` (with `Group M`)
+  it is the `Subgroup M` consisting of elements which fix `s : Set α` pointwise.
+
+* `fixingSubgroup_fixedPoints_gc M α` is the `GaloisConnection`
+  that relates `fixingSubgroup` with `fixedPoints`.
+
+TODO :
+
+* Maybe other lemmas are useful
+
+* Treat semigroups ?
+
+-/
+
+
+section Monoid
+
+open MulAction
+
+variable (M : Type _) {α : Type _} [Monoid M] [MulAction M α]
+
+/-- The submonoid fixing a set under a `MulAction`. -/
+@[to_additive " The additive submonoid fixing a set under an `AddAction`. "]
+def fixingSubmonoid (s : Set α) : Submonoid M
+    where
+  carrier := { ϕ : M | ∀ x : s, ϕ • (x : α) = x }
+  one_mem' _ := one_smul _ _
+  mul_mem' {x y} hx hy z := by rw [mul_smul, hy z, hx z]
+#align fixing_submonoid fixingSubmonoid
+#align fixing_add_submonoid fixingAddSubmonoid
+
+theorem mem_fixingSubmonoid_iff {s : Set α} {m : M} :
+    m ∈ fixingSubmonoid M s ↔ ∀ y ∈ s, m • y = y :=
+  ⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩
+#align mem_fixing_submonoid_iff mem_fixingSubmonoid_iff
+
+variable (α)
+
+/-- The Galois connection between fixing submonoids and fixed points of a monoid action -/
+theorem fixingSubmonoid_fixedPoints_gc :
+    GaloisConnection (OrderDual.toDual ∘ fixingSubmonoid M)
+      ((fun P : Submonoid M => fixedPoints P α) ∘ OrderDual.ofDual) :=
+  fun _s _P => ⟨fun h s hs p => h p.2 ⟨s, hs⟩, fun h p hp s => h s.2 ⟨p, hp⟩⟩
+#align fixing_submonoid_fixed_points_gc fixingSubmonoid_fixedPoints_gc
+
+theorem fixingSubmonoid_antitone : Antitone fun s : Set α => fixingSubmonoid M s :=
+  (fixingSubmonoid_fixedPoints_gc M α).monotone_l
+#align fixing_submonoid_antitone fixingSubmonoid_antitone
+
+theorem fixedPoints_antitone : Antitone fun P : Submonoid M => fixedPoints P α :=
+  (fixingSubmonoid_fixedPoints_gc M α).monotone_u.dual_left
+#align fixed_points_antitone fixedPoints_antitone
+
+/-- Fixing submonoid of union is intersection -/
+theorem fixingSubmonoid_union {s t : Set α} :
+    fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t :=
+  (fixingSubmonoid_fixedPoints_gc M α).l_sup
+#align fixing_submonoid_union fixingSubmonoid_union
+
+/-- Fixing submonoid of unionᵢ is intersection -/
+theorem fixingSubmonoid_unionᵢ {ι : Sort _} {s : ι → Set α} :
+    fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i) :=
+  (fixingSubmonoid_fixedPoints_gc M α).l_supᵢ
+#align fixing_submonoid_Union fixingSubmonoid_unionᵢ
+
+/-- Fixed points of sup of submonoids is intersection -/
+theorem fixedPoints_submonoid_sup {P Q : Submonoid M} :
+    fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α :=
+  (fixingSubmonoid_fixedPoints_gc M α).u_inf
+#align fixed_points_submonoid_sup fixedPoints_submonoid_sup
+
+/-- Fixed points of supᵢ of submonoids is intersection -/
+theorem fixedPoints_submonoid_supᵢ {ι : Sort _} {P : ι → Submonoid M} :
+    fixedPoints (↥(supᵢ P)) α = ⋂ i, fixedPoints (P i) α :=
+  (fixingSubmonoid_fixedPoints_gc M α).u_infᵢ
+#align fixed_points_submonoid_supr fixedPoints_submonoid_supᵢ
+
+end Monoid
+
+section Group
+
+open MulAction
+
+variable (M : Type _) {α : Type _} [Group M] [MulAction M α]
+
+/-- The subgroup fixing a set under a `MulAction`. -/
+@[to_additive " The additive subgroup fixing a set under an `AddAction`. "]
+def fixingSubgroup (s : Set α) : Subgroup M :=
+  { fixingSubmonoid M s with inv_mem' := fun hx z => by rw [inv_smul_eq_iff, hx z] }
+#align fixing_subgroup fixingSubgroup
+#align fixing_add_subgroup fixingAddSubgroup
+
+theorem mem_fixingSubgroup_iff {s : Set α} {m : M} : m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y :=
+  ⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩
+#align mem_fixing_subgroup_iff mem_fixingSubgroup_iff
+
+variable (α)
+
+/-- The Galois connection between fixing subgroups and fixed points of a group action -/
+theorem fixingSubgroup_fixedPoints_gc :
+    GaloisConnection (OrderDual.toDual ∘ fixingSubgroup M)
+      ((fun P : Subgroup M => fixedPoints P α) ∘ OrderDual.ofDual) :=
+  fun _s _P => ⟨fun h s hs p => h p.2 ⟨s, hs⟩, fun h p hp s => h s.2 ⟨p, hp⟩⟩
+#align fixing_subgroup_fixed_points_gc fixingSubgroup_fixedPoints_gc
+
+theorem fixingSubgroup_antitone : Antitone (fixingSubgroup M : Set α → Subgroup M) :=
+  (fixingSubgroup_fixedPoints_gc M α).monotone_l
+#align fixing_subgroup_antitone fixingSubgroup_antitone
+
+theorem fixedPoints_subgroup_antitone : Antitone fun P : Subgroup M => fixedPoints P α :=
+  (fixingSubgroup_fixedPoints_gc M α).monotone_u.dual_left
+#align fixed_points_subgroup_antitone fixedPoints_subgroup_antitone
+
+/-- Fixing subgroup of union is intersection -/
+theorem fixingSubgroup_union {s t : Set α} :
+    fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t :=
+  (fixingSubgroup_fixedPoints_gc M α).l_sup
+#align fixing_subgroup_union fixingSubgroup_union
+
+/-- Fixing subgroup of unionᵢ is intersection -/
+theorem fixingSubgroup_unionᵢ {ι : Sort _} {s : ι → Set α} :
+    fixingSubgroup M (⋃ i, s i) = ⨅ i, fixingSubgroup M (s i) :=
+  (fixingSubgroup_fixedPoints_gc M α).l_supᵢ
+#align fixing_subgroup_Union fixingSubgroup_unionᵢ
+
+/-- Fixed points of sup of subgroups is intersection -/
+theorem fixedPoints_subgroup_sup {P Q : Subgroup M} :
+    fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α :=
+  (fixingSubgroup_fixedPoints_gc M α).u_inf
+#align fixed_points_subgroup_sup fixedPoints_subgroup_sup
+
+/-- Fixed points of supᵢ of subgroups is intersection -/
+theorem fixedPoints_subgroup_supᵢ {ι : Sort _} {P : ι → Subgroup M} :
+    fixedPoints (↥(supᵢ P)) α = ⋂ i, fixedPoints (P i) α :=
+  (fixingSubgroup_fixedPoints_gc M α).u_infᵢ
+#align fixed_points_subgroup_supr fixedPoints_subgroup_supᵢ
+
+end Group