Mathlib.GroupTheory.GroupAction.FixingSubgroup

fixingSubmonoid definition

(s : Set α) : Submonoid M

Full source

/-- 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]

Fixing submonoid of a monoid action

Informal description

Given a monoid $M$ acting on a type $\alpha$ and a subset $s \subseteq \alpha$, the fixing submonoid of $M$ with respect to $s$ is the submonoid consisting of all elements $\phi \in M$ such that $\phi \cdot x = x$ for every $x \in s$.

mem_fixingSubmonoid_iff theorem

{s : Set α} {m : M} : m ∈ fixingSubmonoid M s ↔ ∀ y ∈ s, m • y = y

Full source

@[to_additive]
theorem mem_fixingSubmonoid_iff {s : Set α} {m : M} :
    m ∈ fixingSubmonoid M sm ∈ fixingSubmonoid M s ↔ ∀ y ∈ s, m • y = y :=
  ⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩

Characterization of Elements in the Fixing Submonoid

Informal description

An element $m$ of a monoid $M$ acting on a type $\alpha$ belongs to the fixing submonoid with respect to a subset $s \subseteq \alpha$ if and only if for every $y \in s$, the action of $m$ on $y$ fixes $y$, i.e., $m \cdot y = y$.

fixingSubmonoid_fixedPoints_gc theorem

 : GaloisConnection (OrderDual.toDual ∘ fixingSubmonoid M) ((fun P : Submonoid M => fixedPoints P α) ∘ OrderDual.ofDual)

Full source

/-- The Galois connection between fixing submonoids and fixed points of a monoid action -/
@[to_additive]
theorem fixingSubmonoid_fixedPoints_gc :
    GaloisConnection (OrderDual.toDualOrderDual.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⟩⟩

Galois Connection Between Fixing Submonoids and Fixed Points

Informal description

Let $M$ be a monoid acting on a type $\alpha$. There is a Galois connection between the fixing submonoids and the fixed points, where: - The lower adjoint maps a subset $s \subseteq \alpha$ to the fixing submonoid $\{\phi \in M \mid \forall x \in s, \phi \cdot x = x\}$. - The upper adjoint maps a submonoid $P \subseteq M$ to the set of fixed points $\{a \in \alpha \mid \forall \phi \in P, \phi \cdot a = a\}$.

fixingSubmonoid_antitone theorem

: Antitone fun s : Set α => fixingSubmonoid M s

Full source

@[to_additive]
theorem fixingSubmonoid_antitone : Antitone fun s : Set α => fixingSubmonoid M s :=
  (fixingSubmonoid_fixedPoints_gc M α).monotone_l

Antitonicity of Fixing Submonoid with Respect to Subset Inclusion

Informal description

The function that maps a subset $s \subseteq \alpha$ to its fixing submonoid $\{\phi \in M \mid \forall x \in s, \phi \cdot x = x\}$ is antitone. That is, if $s \subseteq t$ are subsets of $\alpha$, then the fixing submonoid of $M$ with respect to $t$ is contained in the fixing submonoid with respect to $s$.

fixedPoints_antitone theorem

: Antitone fun P : Submonoid M => fixedPoints P α

Full source

@[to_additive fixedPoints_antitone_addSubmonoid]
theorem fixedPoints_antitone : Antitone fun P : Submonoid M => fixedPoints P α :=
  (fixingSubmonoid_fixedPoints_gc M α).monotone_u.dual_left

Antitonicity of Fixed Points with Respect to Submonoid Inclusion

Informal description

For any monoid $M$ acting on a type $\alpha$, the function that maps a submonoid $P \subseteq M$ to its set of fixed points $\{a \in \alpha \mid \forall \phi \in P, \phi \cdot a = a\}$ is antitone. That is, if $P \subseteq Q$ are submonoids of $M$, then the set of fixed points of $Q$ is contained in the set of fixed points of $P$.

fixingSubmonoid_union theorem

{s t : Set α} : fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t

Full source

/-- Fixing submonoid of union is intersection -/
@[to_additive]
theorem fixingSubmonoid_union {s t : Set α} :
    fixingSubmonoid M (s ∪ t) = fixingSubmonoidfixingSubmonoid M s ⊓ fixingSubmonoid M t :=
  (fixingSubmonoid_fixedPoints_gc M α).l_sup

Fixing Submonoid of Union Equals Intersection of Fixing Submonoids

Informal description

For any monoid $M$ acting on a type $\alpha$ and any subsets $s, t \subseteq \alpha$, the fixing submonoid of $M$ with respect to the union $s \cup t$ is equal to the intersection of the fixing submonoids with respect to $s$ and $t$ individually. That is, \[ \text{fixingSubmonoid}_M(s \cup t) = \text{fixingSubmonoid}_M(s) \cap \text{fixingSubmonoid}_M(t). \]

fixingSubmonoid_iUnion theorem

{ι : Sort*} {s : ι → Set α} : fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i)

Full source

/-- Fixing submonoid of iUnion is intersection -/
@[to_additive]
theorem fixingSubmonoid_iUnion {ι : Sort*} {s : ι → Set α} :
    fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i) :=
  (fixingSubmonoid_fixedPoints_gc M α).l_iSup

Fixing Submonoid of Union Equals Intersection of Fixing Submonoids

Informal description

Let $M$ be a monoid acting on a type $\alpha$, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$. The fixing submonoid of $M$ with respect to the union $\bigcup_i s_i$ is equal to the infimum (intersection) of the fixing submonoids with respect to each $s_i$ individually. That is, \[ \text{fixingSubmonoid}_M\left(\bigcup_i s_i\right) = \bigcap_i \text{fixingSubmonoid}_M(s_i). \]

fixedPoints_submonoid_sup theorem

{P Q : Submonoid M} : fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α

Full source

/-- Fixed points of sup of submonoids is intersection -/
@[to_additive]
theorem fixedPoints_submonoid_sup {P Q : Submonoid M} :
    fixedPoints (↥(P ⊔ Q)) α = fixedPointsfixedPoints P α ∩ fixedPoints Q α :=
  (fixingSubmonoid_fixedPoints_gc M α).u_inf

Fixed Points of Join of Submonoids Equals Intersection of Fixed Points

Informal description

Let $M$ be a monoid acting on a type $\alpha$, and let $P$ and $Q$ be submonoids of $M$. The set of fixed points under the action of the join $P \sqcup Q$ is equal to the intersection of the fixed points under $P$ and $Q$ individually, i.e., \[ \text{fixedPoints}(P \sqcup Q, \alpha) = \text{fixedPoints}(P, \alpha) \cap \text{fixedPoints}(Q, \alpha). \]

fixedPoints_submonoid_iSup theorem

{ι : Sort*} {P : ι → Submonoid M} : fixedPoints (↥(iSup P)) α = ⋂ i, fixedPoints (P i) α

Full source

/-- Fixed points of iSup of submonoids is intersection -/
@[to_additive]
theorem fixedPoints_submonoid_iSup {ι : Sort*} {P : ι → Submonoid M} :
    fixedPoints (↥(iSup P)) α = ⋂ i, fixedPoints (P i) α :=
  (fixingSubmonoid_fixedPoints_gc M α).u_iInf

Fixed Points of Supremum of Submonoids Equals Intersection of Fixed Points

Informal description

Let $M$ be a monoid acting on a type $\alpha$, and let $\{P_i\}_{i \in \iota}$ be a family of submonoids of $M$. The set of fixed points under the action of the supremum of the submonoids $\bigsqcup_i P_i$ is equal to the intersection of the fixed points under each individual submonoid $P_i$, i.e., \[ \text{fixedPoints}(\bigsqcup_i P_i, \alpha) = \bigcap_i \text{fixedPoints}(P_i, \alpha). \]

fixingSubgroup definition

(s : Set α) : Subgroup M

Full source

/-- 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] }

Fixing subgroup of a group action

Informal description

Given a group $M$ acting on a type $\alpha$ and a subset $s \subseteq \alpha$, the fixing subgroup of $M$ with respect to $s$ is the subgroup consisting of all elements $g \in M$ such that $g \cdot x = x$ for every $x \in s$. This is constructed by extending the fixing submonoid with the additional property that the inverse of any element in the subgroup also fixes $s$.

mem_fixingSubgroup_iff theorem

{s : Set α} {m : M} : m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y

Full source

@[to_additive]
theorem mem_fixingSubgroup_iff {s : Set α} {m : M} : m ∈ fixingSubgroup M sm ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y :=
  ⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩

Characterization of Fixing Subgroup via Pointwise Fixing Condition

Informal description

For a group $M$ acting on a set $\alpha$, an element $m \in M$ belongs to the fixing subgroup with respect to a subset $s \subseteq \alpha$ if and only if for every $y \in s$, the action of $m$ on $y$ fixes $y$, i.e., $m \cdot y = y$.

mem_fixingSubgroup_iff_subset_fixedBy theorem

{s : Set α} {m : M} : m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m

Full source

@[to_additive]
theorem mem_fixingSubgroup_iff_subset_fixedBy {s : Set α} {m : M} :
    m ∈ fixingSubgroup M sm ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m := by
  simp_rw [mem_fixingSubgroup_iff, Set.subset_def, mem_fixedBy]

Characterization of Fixing Subgroup via Fixed Points

Informal description

For a group $M$ acting on a set $\alpha$, an element $m \in M$ belongs to the fixing subgroup with respect to a subset $s \subseteq \alpha$ if and only if every element of $s$ is fixed by the action of $m$, i.e., $s \subseteq \{x \in \alpha \mid m \cdot x = x\}$.

mem_fixingSubgroup_compl_iff_movedBy_subset theorem

{s : Set α} {m : M} : m ∈ fixingSubgroup M sᶜ ↔ (fixedBy α m)ᶜ ⊆ s

Full source

@[to_additive]
theorem mem_fixingSubgroup_compl_iff_movedBy_subset {s : Set α} {m : M} :
    m ∈ fixingSubgroup M sᶜm ∈ fixingSubgroup M sᶜ ↔ (fixedBy α m)ᶜ ⊆ s := by
  rw [mem_fixingSubgroup_iff_subset_fixedBy, Set.compl_subset_comm]

Characterization of Fixing Subgroup for Complement via Moved Points

Informal description

For a group $M$ acting on a set $\alpha$, an element $m \in M$ belongs to the fixing subgroup with respect to the complement $s^c$ of a subset $s \subseteq \alpha$ if and only if the complement of the fixed points of $m$ is contained in $s$, i.e., $\{x \in \alpha \mid m \cdot x \neq x\} \subseteq s$.

fixingSubgroup_fixedPoints_gc theorem

 : GaloisConnection (OrderDual.toDual ∘ fixingSubgroup M) ((fun P : Subgroup M => fixedPoints P α) ∘ OrderDual.ofDual)

Full source

/-- The Galois connection between fixing subgroups and fixed points of a group action -/
@[to_additive]
theorem fixingSubgroup_fixedPoints_gc :
    GaloisConnection (OrderDual.toDualOrderDual.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⟩⟩

Galois Connection Between Fixing Subgroups and Fixed Points

Informal description

Let $M$ be a group acting on a set $\alpha$. There is a Galois connection between the lattice of subgroups of $M$ (ordered by reverse inclusion) and the lattice of subsets of $\alpha$ (ordered by inclusion), given by: - The left adjoint maps a subset $s \subseteq \alpha$ to the fixing subgroup $\{g \in M \mid \forall x \in s, g \cdot x = x\}$. - The right adjoint maps a subgroup $H \leq M$ to its set of fixed points $\{x \in \alpha \mid \forall h \in H, h \cdot x = x\}$.

fixingSubgroup_antitone theorem

: Antitone (fixingSubgroup M : Set α → Subgroup M)

Full source

@[to_additive]
theorem fixingSubgroup_antitone : Antitone (fixingSubgroup M : Set α → Subgroup M) :=
  (fixingSubgroup_fixedPoints_gc M α).monotone_l

Antitonicity of Fixing Subgroup with Respect to Subset Inclusion

Informal description

For a group $M$ acting on a set $\alpha$, the function that maps a subset $s \subseteq \alpha$ to its fixing subgroup $\{g \in M \mid \forall x \in s, g \cdot x = x\}$ is antitone. That is, if $s \subseteq t$ are subsets of $\alpha$, then the fixing subgroup of $t$ is contained in the fixing subgroup of $s$.

fixedPoints_subgroup_antitone theorem

: Antitone fun P : Subgroup M => fixedPoints P α

Full source

@[to_additive]
theorem fixedPoints_subgroup_antitone : Antitone fun P : Subgroup M => fixedPoints P α :=
  (fixingSubgroup_fixedPoints_gc M α).monotone_u.dual_left

Antitonicity of Fixed Points with Respect to Subgroup Inclusion

Informal description

For any group $M$ acting on a set $\alpha$, the function that maps a subgroup $P \leq M$ to its set of fixed points $\{x \in \alpha \mid \forall g \in P, g \cdot x = x\}$ is antitone. That is, if $P \leq Q$ are subgroups of $M$, then the set of fixed points of $Q$ is contained in the set of fixed points of $P$.

fixingSubgroup_union theorem

{s t : Set α} : fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t

Full source

/-- Fixing subgroup of union is intersection -/
@[to_additive]
theorem fixingSubgroup_union {s t : Set α} :
    fixingSubgroup M (s ∪ t) = fixingSubgroupfixingSubgroup M s ⊓ fixingSubgroup M t :=
  (fixingSubgroup_fixedPoints_gc M α).l_sup

Fixing Subgroup of Union Equals Intersection of Fixing Subgroups

Informal description

For a group $M$ acting on a set $\alpha$ and any subsets $s, t \subseteq \alpha$, the fixing subgroup of $M$ with respect to the union $s \cup t$ is equal to the intersection of the fixing subgroups with respect to $s$ and $t$, i.e., \[ \text{fixingSubgroup}_M(s \cup t) = \text{fixingSubgroup}_M(s) \cap \text{fixingSubgroup}_M(t). \]

fixingSubgroup_iUnion theorem

{ι : Sort*} {s : ι → Set α} : fixingSubgroup M (⋃ i, s i) = ⨅ i, fixingSubgroup M (s i)

Full source

/-- Fixing subgroup of iUnion is intersection -/
@[to_additive]
theorem fixingSubgroup_iUnion {ι : Sort*} {s : ι → Set α} :
    fixingSubgroup M (⋃ i, s i) = ⨅ i, fixingSubgroup M (s i) :=
  (fixingSubgroup_fixedPoints_gc M α).l_iSup

Fixing Subgroup of Union Equals Intersection of Fixing Subgroups

Informal description

Let $M$ be a group acting on a set $\alpha$, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$. The fixing subgroup of $M$ with respect to the union $\bigcup_i s_i$ is equal to the infimum (intersection) of the fixing subgroups with respect to each individual $s_i$, i.e., \[ \text{fixingSubgroup}_M\left(\bigcup_i s_i\right) = \bigcap_i \text{fixingSubgroup}_M(s_i). \]

fixedPoints_subgroup_sup theorem

{P Q : Subgroup M} : fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α

Full source

/-- Fixed points of sup of subgroups is intersection -/
@[to_additive]
theorem fixedPoints_subgroup_sup {P Q : Subgroup M} :
    fixedPoints (↥(P ⊔ Q)) α = fixedPointsfixedPoints P α ∩ fixedPoints Q α :=
  (fixingSubgroup_fixedPoints_gc M α).u_inf

Fixed Points of Join of Subgroups Equals Intersection of Fixed Points

Informal description

Let $M$ be a group acting on a set $\alpha$, and let $P$ and $Q$ be subgroups of $M$. The set of fixed points of the join $P \sqcup Q$ (the smallest subgroup containing both $P$ and $Q$) is equal to the intersection of the fixed points of $P$ and $Q$, i.e., \[ \text{fixedPoints}(P \sqcup Q, \alpha) = \text{fixedPoints}(P, \alpha) \cap \text{fixedPoints}(Q, \alpha). \]

fixedPoints_subgroup_iSup theorem

{ι : Sort*} {P : ι → Subgroup M} : fixedPoints (↥(iSup P)) α = ⋂ i, fixedPoints (P i) α

Full source

/-- Fixed points of iSup of subgroups is intersection -/
@[to_additive]
theorem fixedPoints_subgroup_iSup {ι : Sort*} {P : ι → Subgroup M} :
    fixedPoints (↥(iSup P)) α = ⋂ i, fixedPoints (P i) α :=
  (fixingSubgroup_fixedPoints_gc M α).u_iInf

Fixed Points of Supremum of Subgroups Equals Intersection of Fixed Points

Informal description

Let $M$ be a group acting on a set $\alpha$, and let $\{P_i\}_{i \in \iota}$ be a family of subgroups of $M$. The set of fixed points of the supremum of the subgroups $P_i$ (i.e., the smallest subgroup containing all $P_i$) is equal to the intersection of the fixed points of each individual subgroup $P_i$. In other words: \[ \text{fixedPoints}\left(\bigsqcup_{i} P_i, \alpha\right) = \bigcap_{i} \text{fixedPoints}(P_i, \alpha) \] where $\text{fixedPoints}(H, \alpha)$ denotes the set of all elements in $\alpha$ fixed by every element of the subgroup $H$.

orbit_fixingSubgroup_compl_subset theorem

{s : Set α} {a : α} (a_in_s : a ∈ s) : MulAction.orbit (fixingSubgroup M sᶜ) a ⊆ s

Full source

/-- The orbit of the fixing subgroup of `sᶜ` (ie. the moving subgroup of `s`) is a subset of `s` -/
@[to_additive]
theorem orbit_fixingSubgroup_compl_subset {s : Set α} {a : α} (a_in_s : a ∈ s) :
    MulAction.orbitMulAction.orbit (fixingSubgroup M sᶜ) a ⊆ s := by
  intro b b_in_orbit
  let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit
  rw [Submonoid.mk_smul] at g_eq
  rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing
  rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]

Orbit of Fixing Subgroup of Complement is Contained in Original Set

Informal description

Let $M$ be a group acting on a set $\alpha$, and let $s \subseteq \alpha$ be a subset. For any element $a \in s$, the orbit of $a$ under the action of the fixing subgroup of the complement $s^c$ is contained in $s$, i.e., \[ \text{orbit}_{\text{fixingSubgroup}_M(s^c)}(a) \subseteq s. \]

Main definitions