fixingSubgroup_union
theorem fixingSubgroup_union :
∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {s t : Set α},
fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t
This theorem states that for any type `M` with a group structure and another type `α` with a `MulAction` of `M` on `α`, the fixing subgroup of the union of two sets `s` and `t` is the same as the intersection of the fixing subgroups of `s` and `t`. In mathematical terms, if `M` is a group acting on a set `α`, then the subgroup of `M` that leaves invariant the union of two sets `s` and `t` is exactly the intersection of the subgroups of `M` that stabilize `s` and `t` respectively.
More concisely: For any group `M` acting on a set `α`, the subgroup of `M` fixing the union of sets `s` and `t` is equal to the intersection of the subgroups fixing `s` and `t` respectively.
|
fixedPoints_submonoid_sup
theorem fixedPoints_submonoid_sup :
∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {P Q : Submonoid M},
MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α
This theorem states that for any type `M` with a monoid structure, any type `α` with a multiplication action of `M` on `α`, and for any two submonoids `P` and `Q` of `M`, the set of points fixed under the action of the union of `P` and `Q` (`P ⊔ Q`) is exactly the intersection of the set of points fixed under the action of `P` and the set of points fixed under the action of `Q`. In other words, an element in `α` is fixed by the combined action of `P` and `Q` if and only if it's fixed by both the action of `P` and the action of `Q` individually.
More concisely: For any type `M` with a monoid structure, any type `α` with a multiplication action of `M`, and for any submonoids `P` and `Q` of `M`, the fixed sets under the actions of `P ⊔ Q` and the intersection of `P` and `Q` are equal.
|
fixedPoints_submonoid_iSup
theorem fixedPoints_submonoid_iSup :
∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {ι : Sort u_3} {P : ι → Submonoid M},
MulAction.fixedPoints (↥(iSup P)) α = ⋂ i, MulAction.fixedPoints (↥(P i)) α
The theorem `fixedPoints_submonoid_iSup` states that for any type `M` with a monoid structure, any type `α` with a `MulAction` of `M`, and any indexed family `P` of submonoids of `M`, the set of fixed points under the action of the supremum of the submonoids (`iSup P`) is equal to the intersection of the sets of fixed points under the action of each individual submonoid in the family. In other words, an element of `α` is fixed by the action of all the submonoids in the `iSup P` if and only if it is fixed by the action of each submonoid in the family `P`.
More concisely: For any monoid `M`, type `α` with a `MulAction` of `M`, and indexed family `P` of submonoids of `M`, the set of elements in `α` fixed by the action of the supremum of `P` equals the intersection of the sets of elements fixed by the action of each submonoid in `P`.
|
fixedPoints_subgroup_iSup
theorem fixedPoints_subgroup_iSup :
∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {ι : Sort u_3} {P : ι → Subgroup M},
MulAction.fixedPoints (↥(iSup P)) α = ⋂ i, MulAction.fixedPoints (↥(P i)) α
The theorem `fixedPoints_subgroup_iSup` states that for any group `M` acting on a type `α`, and for any indexed family of subgroups `P` of `M`, the set of fixed points under the action of the supremum of the subgroups `P` is exactly the intersection of the set of fixed points for each individual subgroup in `P`.
In mathematical terms, if we think of `M` and `α` as sets, `ι` as an index set, and `P` as a family of subgroups of `M` indexed by `ι`, then the set of elements of `α` that remain fixed under the group action of the supremum of the subgroups in `P` is exactly the same as the intersection of the sets of elements of `α` that remain fixed under the group action of each individual subgroup in `P`.
More concisely: The set of fixed points under the group action of the supremum of a family of subgroups of a group acting on a type is equal to the intersection of the sets of fixed points for each subgroup in the family.
|
fixedPoints_subgroup_sup
theorem fixedPoints_subgroup_sup :
∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {P Q : Subgroup M},
MulAction.fixedPoints (↥(P ⊔ Q)) α = MulAction.fixedPoints (↥P) α ∩ MulAction.fixedPoints (↥Q) α
The theorem `fixedPoints_subgroup_sup` states that for any group `M` and any type `α` with a `MulAction` of `M` on `α`, and for any two subgroups `P` and `Q` of `M`, the set of fixed points under the joint action of (the elements of) the supgroup `P ⊔ Q` is exactly the intersection of the set of fixed points under the action of `P` and the set of fixed points under the action of `Q`. In other words, an element of `α` is fixed by all elements of `P ⊔ Q` if and only if it is both fixed by all elements of `P` and fixed by all elements of `Q`.
More concisely: The theorem asserts that the set of elements in `α` fixed by the joint action of a group `M`'s subgroups `P` and `Q` is equal to the intersection of the sets of elements fixed by each subgroup's action individually.
|
fixingSubmonoid_fixedPoints_gc
theorem fixingSubmonoid_fixedPoints_gc :
∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α],
GaloisConnection (⇑OrderDual.toDual ∘ fixingSubmonoid M)
((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
This theorem establishes a Galois connection between the fixing submonoids and the fixed points of a monoid action. Given a monoid `M` and a type `α` where `M` acts on `α` by multiplication, the Galois connection is formed between the function that maps `M` to its fixing submonoid under the dual order and the function that maps a submonoid `P` of `M` to the set of fixed points of `P`'s action on `α`, under the original order. Essentially, it's saying that a submonoid's fixed points and the points that fix a submonoid have a unique relationship captured by the Galois connection.
More concisely: The Galois connection establishes a bi-directional relationship between the fixing submonoids of a monoid action and the sets of fixed points under the dual and original orders, respectively.
|
fixingSubmonoid_union
theorem fixingSubmonoid_union :
∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {s t : Set α},
fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t
This theorem states that for any given type `M`, which has a structure of a Monoid, and any type `α` that has a `MulAction` of `M`, the submonoid of `M` that preserves the union of two sets `s` and `t` (i.e., leaves each element of `s ∪ t` unchanged under multiplication) is equal to the intersection of the submonoids that preserve `s` and `t` independently. In mathematical terms, if $S$ and $T$ are subsets of a set $\alpha$, and $M$ is a monoid acting on $\alpha$, then the submonoid of $M$ preserving $S \cup T$ is the same as the intersection of the submonoids preserving $S$ and $T$, respectively.
More concisely: For any monoid `M` acting on a type `α`, the submonoid preserving the union of two sets `s` and `t` is equal to the intersection of the submonoids preserving `s` and `t` independently.
|
fixingSubmonoid_iUnion
theorem fixingSubmonoid_iUnion :
∀ (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst_1 : MulAction M α] {ι : Sort u_3} {s : ι → Set α},
fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i)
This theorem states that for any monoid `M` and any type `α` with a multiplication action of `M` on `α`, the fixing submonoid of the union of a collection of sets `{s i}` indexed by `ι` is equal to the intersection of the fixing submonoids of each individual set `{s i}`. In short, the fixing submonoid of a union of sets is the intersection of their individual fixing submonoids.
More concisely: For any monoid `M` acting on a type `α` and any collection `{s i}` of `M`-invariant sets `s i` indexed by `ι`, the fixing submonoid of their union is equal to the intersection of their individual fixing submonoids.
|
fixingSubgroup_iUnion
theorem fixingSubgroup_iUnion :
∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {ι : Sort u_3} {s : ι → Set α},
fixingSubgroup M (⋃ i, s i) = ⨅ i, fixingSubgroup M (s i)
This theorem states that for any type `M` with a group structure, any type `α` with a `MulAction` of `M` on `α`, and a family of sets `s` indexed by type `ι`, the subgroup of `M` that fixes the union of the sets in the family `s` (denoted by `⋃ i, s i`) is equal to the intersection (denoted by `⨅ i`) of all the subgroups of `M` that fix each individual set in the family `s`. In other words, an element of `M` fixes the union of sets if and only if it fixes each of the sets individually.
More concisely: For any type `M` with a group structure, any type `α` with a `MulAction` of `M` on `α`, and a family of sets `s : ι → Sets`, the subgroup of `M` fixing the union of `s` equals the intersection of subgroups fixing each `s(i)`.
|
fixingSubgroup_fixedPoints_gc
theorem fixingSubgroup_fixedPoints_gc :
∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α],
GaloisConnection (⇑OrderDual.toDual ∘ fixingSubgroup M)
((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
This theorem establishes a Galois connection between the subgroups that fix a set under a group action and the set of points fixed by the whole action. Specifically, for a given group `M` and type `α` with a group action `M` on `α`, there exists a Galois connection between the dual of the function `fixingSubgroup M` (which maps a set to the subgroup that fixes it under the action) and the function that maps a group to the set of fixed points of `α` under the action of that group, after applying the dual of the function. In other words, a subgroup `P` fixes a set `s` if and only if every element of `s` is a fixed point under the action of the group `P`.
More concisely: The Galois connection exists between the function mapping sets to their fixating subgroups under a group action on type `α`, and the function mapping groups to their fixed point sets on `α`. That is, a subgroup fixes a set if and only if every element in the set is fixed by the group under the action.
|