MulAction.stabilizer_smul_eq_stabilizer_map_conj
theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj :
∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α),
MulAction.stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MulAction.stabilizer G a)
The theorem `MulAction.stabilizer_smul_eq_stabilizer_map_conj` states that for a given group `G` acting on a type `α`, if an element `a` of `α` has a stabilizer `S` (a subgroup of `G` whose action leaves `a` unchanged), then the stabilizer of `g • a` (the result of `G`'s action on `a`) is `gSg⁻¹`. Here `g` is an element of `G`, `•` represents the action of group `G` on `α`, and `gSg⁻¹` denotes the conjugate of `S` by `g`, which is formed by applying the group conjugation operation to each element of `S`. This theorem essentially describes how the stabilizer of an element changes under the group action.
More concisely: For any group action of `G` on `α` and stabilizer `S` of an element `a` in `α`, the stabilizer of `g • a` is `gSg⁻¹` for all `g` in `G`.
|
MulAction.mem_stabilizer_iff
theorem MulAction.mem_stabilizer_iff :
∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : α} {g : G},
g ∈ MulAction.stabilizer G a ↔ g • a = a
The theorem `MulAction.mem_stabilizer_iff` states that for any group `G`, any type `α` equipped with a `MulAction` of `G`, any element `a` of `α`, and any group element `g` of `G`, `g` is a member of the stabilizer of `a` under the action of `G` if and only if the action of `g` leaves `a` unchanged, i.e., `g` acting on `a` equals `a`. In other words, it establishes the equivalence between an element being in the stabilizer of `a` and the action of that element on `a` resulting in `a` itself.
More concisely: For any group `G` acting on a type `α` via a `MulAction`, an element `g` in `G` is in the stabilizer of `α` element `a` if and only if `g` leaves `a` unchanged under the action, i.e., `g * a = a`.
|
AddAction.mem_stabilizer_iff
theorem AddAction.mem_stabilizer_iff :
∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : α} {g : G},
g ∈ AddAction.stabilizer G a ↔ g +ᵥ a = a
This theorem states that for any additive group `G`, any set `α` that `G` acts on, any element `a` of `α`, and any element `g` of `G`, the element `g` is in the stabilizer of `a` (i.e., the subgroup of `G` that leaves `a` fixed) if and only if the action of `g` on `a` leaves `a` unchanged. In other words, `g` is in the stabilizer of `a` exactly when `g +ᵥ a = a` (where `+ᵥ` represents the additive action of `G` on `α`).
More concisely: For any additive group `G` acting on a set `α`, an element `g` of `G` stabilizes `α`'s element `a` if and only if `g + a = a`.
|
smul_cancel_of_non_zero_divisor
theorem smul_cancel_of_non_zero_divisor :
∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : NonUnitalNonAssocRing R] [inst_2 : DistribMulAction M R]
(k : M), (∀ (x : R), k • x = 0 → x = 0) → ∀ {a b : R}, k • a = k • b → a = b
The theorem `smul_cancel_of_non_zero_divisor` states that for any type `M`, such that `M` is a monoid, and any type `R`, such that `R` is a non-unital non-associative ring with a distributive multiplication action of `M` on `R`, scalar multiplication (`smul`) by an element `k` of `M` is injective, if `k` is not a zero divisor. This means that if `k` multiplied by any `x` in `R` equals zero, then `x` must be zero. Therefore, if scalar multiplication of `k` with any two elements `a` and `b` in `R` yields the same result, then `a` and `b` must be the same element. The property that all elements of `M` are not zero divisors is generalized by the `IsSMulRegular` structure, and the typeclass that enforces this property is `NoZeroSMulDivisors`.
More concisely: If `M` is a monoid and `R` is a non-unital non-associative ring with a distributive multiplication action of `M` on `R`, and `k` is a non-zero divisor in `M`, then scalar multiplication by `k` is injective on `R`.
|
Mathlib.GroupTheory.GroupAction.Basic._auxLemma.18
theorem Mathlib.GroupTheory.GroupAction.Basic._auxLemma.18 :
∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {a : α} {m : M}
{a' : ↑(MulAction.orbit M a)}, m • ↑a' = ↑(m • a')
This theorem states that for any additive group `G`, an action `AddAction` of `G` on a type `α`, an element `a` of type `α`, and an element `g` of `G`, `g` belongs to the stabilizer of `a` under the additive action if and only if the action of `g` on `a` leaves `a` unchanged. In mathematical terms, the stabilizer of `a` is the set of all elements of `G` that, when acting on `a`, produce `a`.
More concisely: For any additive group `G`, an element `a` of a type `α`, and an action `AddAction` of `G` on `α`, an element `g` stabilizes `a` if and only if `AddAction g a = a`.
|
AddAction.orbit_vadd
theorem AddAction.orbit_vadd :
∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
AddAction.orbit G (g +ᵥ a) = AddAction.orbit G a
The theorem `AddAction.orbit_vadd` establishes that for any additive group `G`, any additive action of `G` on a type `α`, and any elements `g` of `G` and `a` of `α`, the orbit under the action of `G` of the translated element `g +ᵥ a` is identically equal to the orbit of the original element `a`. In other words, translating an element by additive action does not change its orbit under the same action.
More concisely: For any additive group G, any additive action of G on a type α, and all g in G and a in α, the orbit of g +ᵥ a under the action of G is identical to the orbit of a.
|
MulAction.quotient_preimage_image_eq_union_mul
theorem MulAction.quotient_preimage_image_eq_union_mul :
∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (U : Set α),
Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g, (fun x => g • x) '' U
This theorem, `MulAction.quotient_preimage_image_eq_union_mul`, states that for any group `G`, any set `U` in a type `α` equipped with a `G` action (`MulAction G α`), when we map `U` to the quotient by the `Quotient.mk'` function, and then pull it back to `α` again, we get the union of the `G`-orbits of `U`. Here, `G`-orbit of `U` refers to the set of all possible results obtained by applying the group elements (via the group action) to the elements of `U`. This involves group theory and set theory, and describes a property of the interaction between the group action and the quotient mapping.
More concisely: For any set `U` in a type `α` with a `G`-action, the preimage of `Quotient.mk' U` under the quotient map and the image of `U` under the `G`-action are equal. In other words, the set of `G`-orbits of `U` is the same as the set obtained by mapping `U` to its quotient and then pulling it back to `α`.
|
MulAction.mem_orbit_self
theorem MulAction.mem_orbit_self :
∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] (a : α), a ∈ MulAction.orbit M a
This theorem states that for any type `M` with a Monoid structure, any type `α` with a `MulAction` of `M`, and any element `a` of type `α`, the element `a` is always an element of its own orbit in the `MulAction`. In mathematical terms, this means that for any element `a` in a set that a monoid `M` acts on, the orbit of `a` (which is the set of all elements that can be reached from `a` by the action of elements in `M`) always includes `a` itself.
More concisely: For any monoid action of a type `M` on a type `α` and any element `a` in `α`, the orbit of `a` contains `a` itself.
|
Mathlib.GroupTheory.GroupAction.Basic._auxLemma.17
theorem Mathlib.GroupTheory.GroupAction.Basic._auxLemma.17 :
∀ {M' : Type u_5} {α : Type u_6} [inst : MulOneClass M'] [inst_1 : SMul M' α] {S : Submonoid M'} (g : ↥S) (a : α),
↑g • a = g • a
This theorem states that for any group `G` and any type `α` with a multiplication action of `G` on `α`, and for any element `a` of `α` and `g` of `G`, the element `g` belongs to the stabilizer of `a` if and only if the action of `g` on `a` leaves `a` invariant. In other words, `g` is in the stabilizer of `a` under this action if and only if multiplying `a` by `g` results in `a` again.
More concisely: For any group action of a group `G` on a type `α` and any element `a` in `α`, an element `g` in `G` is in the stabilizer of `a` if and only if `a * g = a`.
|
MulAction.orbit_smul
theorem MulAction.orbit_smul :
∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α),
MulAction.orbit G (g • a) = MulAction.orbit G a
The theorem `MulAction.orbit_smul` asserts that for any group `G` and any type `α` that `G` acts on, the orbit under the action of `G` of the result of the action of any element of `G` on any element of `α` is the same as the orbit of the original element of `α`. In simpler terms, if a group element `g` acts on an element `a`, the set of all possible results you can get by letting any element of the group act on `g • a` is the same as the set of all results you can get by letting any group element act on `a`. This is a statement about the invariance of the orbit under the action of the group.
More concisely: For any group action on a type `α`, the orbit of `g • a` is equal to the orbit of `a` for all `g` in the group.
|
AddAction.mem_orbit_self
theorem AddAction.mem_orbit_self :
∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] (a : α), a ∈ AddAction.orbit M a := by
sorry
This theorem states that for any type `M` equipped with an add monoid structure, any type `α` equipped with an AddAction of `M`, and any element `a` of type `α`, `a` is an element of its own orbit under the action of the add monoid `M`. In mathematical terms, this theorem asserts that for every element in a set that is acted upon by an additive monoid, the element is always contained in its own orbit under this action.
More concisely: For any add monoid `M` acting on type `α` through an AddAction, and for any element `a` in `α`, `a` is in the orbit of `{0} : M` under the action of `M`.
|
AddAction.stabilizer_vadd_eq_stabilizer_map_conj
theorem AddAction.stabilizer_vadd_eq_stabilizer_map_conj :
∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
AddAction.stabilizer G (g +ᵥ a) =
AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (AddAction.stabilizer G a)
This theorem states that for any additive group `G` acting on a set `α`, for any element `g` of `G` and any element `a` of `α`, the stabilizer of the point `g +ᵥ a` (that is, the subgroup of `G` whose elements fix `g +ᵥ a` under the action) is the image of the stabilizer of `a` under the additive group conjugation by `g`. In other words, if `S` is the stabilizer of `a`, then the stabilizer of `g +ᵥ a` is the set `{ g + s - g | s ∈ S }`. This theorem describes how the stabilizer changes when we shift the point `a` by `g` under the action.
More concisely: The stabilizer of `g + a` under the action of an additive group `G` on a set `α` is the conjugate subgroup of the stabilizer of `a` by `g`, i.e., the set `{ g + s - g | s ∈ S }`, where `S` is the stabilizer of `a`.
|
MulAction.mem_orbit_iff
theorem MulAction.mem_orbit_iff :
∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {a₁ a₂ : α},
a₂ ∈ MulAction.orbit M a₁ ↔ ∃ x, x • a₁ = a₂
The theorem `MulAction.mem_orbit_iff` states that for any monoid `M` and any type `α` with a monoid action (`MulAction`), for any two elements `a₁` and `a₂` of α, `a₂` is in the orbit of `a₁` under the action of `M` if and only if there exists an element `x` in `M` such that the action of `x` on `a₁` results in `a₂`. In mathematical terms, `a₂` is in the orbit of `a₁` under the group action if and only if there exists `x` in `M` such that `x * a₁ = a₂`.
More concisely: For any monoid `M` and `MulAction` on type `α`, an element `a₂` is in the orbit of `a₁` under the action if and only if there exists an element `x` in `M` such that `x * a₁ = a₂`.
|
AddAction.quotient_preimage_image_eq_union_add
theorem AddAction.quotient_preimage_image_eq_union_add :
∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (U : Set α),
Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g, (fun x => g +ᵥ x) '' U
The theorem `AddAction.quotient_preimage_image_eq_union_add` states that, for any set `U` in a type `α`, under the context of an additive group `G` and a corresponding additive action of `G` on `α`, the preimage of the image of `U` under the canonical quotient map is equal to the union of all the orbits of `U` under the additive group `G`. Here, an orbit refers to a set of elements in `α` that can be reached by adding an element of `G` to an element in `U`.
More concisely: For an additive group action on a set U in α, the preimage of the image of U under the quotient map is equal to the union of all orbit sets of U.
|
AddAction.orbitRel.Quotient.orbit_eq_orbit_out
theorem AddAction.orbitRel.Quotient.orbit_eq_orbit_out :
∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (x : AddAction.orbitRel.Quotient G α)
{φ : AddAction.orbitRel.Quotient G α → α},
Function.RightInverse φ Quotient.mk' → x.orbit = AddAction.orbit G (φ x)
The theorem `AddAction.orbitRel.Quotient.orbit_eq_orbit_out` states that for any type `G` which forms an add group, any type `α` on which `G` acts, and any element `x` of the quotient type under the orbit relation of this action, if there exists a function `φ` which serves as a right inverse to the canonical quotient map, then the orbit of `x` under the action of `G` is equal to the orbit of the element `φ(x)`. In other words, if we have a function that can 'undo' the quotient map, the orbits before and after applying this function are the same. The theorem suggests that a useful choice for `φ` is the function `Quotient.out_eq'` which returns a representative for each equivalence class in the quotient.
More concisely: For any add group action `G` on type `α`, if there exists a right inverse `φ` for the quotient map, then the orbit of `x` under `G` is equal to the orbit of `φ(x)`.
|
MulAction.orbitRel.Quotient.orbit_eq_orbit_out
theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out :
∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (x : MulAction.orbitRel.Quotient G α)
{φ : MulAction.orbitRel.Quotient G α → α},
Function.RightInverse φ Quotient.mk' → x.orbit = MulAction.orbit G (φ x)
The theorem `MulAction.orbitRel.Quotient.orbit_eq_orbit_out` states that for any group `G` and any type `α`, given a group action of `G` on `α`, any element `x` in the quotient of `α` by the orbit relation of `G`, and any function `φ` that is a right inverse to the canonical quotient map `Quotient.mk'`, the orbit of `x` under the group `G` is equal to the orbit of the image of `x` under `φ` under the group `G`.
In other words, if we have a function that can "undo" the process of taking equivalence classes (orbits) under group action, applying this function to a member of the quotient space and then calculating the orbit gives the same result as directly calculating the orbit in the quotient space.
More concisely: For any group action on a type, the orbit of an equivalence class under the group is equal to the orbit of any of its representatives under the group.
|
MulAction.mem_fixedBy
theorem MulAction.mem_fixedBy :
∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] {m : M} {a : α},
a ∈ MulAction.fixedBy α m ↔ m • a = a
The theorem `MulAction.mem_fixedBy` states that for any type `M` with a monoid structure, any type `α` on which `M` acts as a multiplicative action, any element `m` of type `M` and any element `a` of type `α`, `a` is an element of the set of elements fixed by `m` (`MulAction.fixedBy α m`) if and only if the action of `m` on `a` leaves `a` unchanged (i.e., `m • a = a`). In other words, it provides a characterization of the set of elements fixed by a given element in the monoid under the given action.
More concisely: For any type `M` with a monoid structure, any type `α` on which `M` acts as a multiplicative action, and any `m` in `M` and `α` in `α`, `α` is in the set of elements fixed by `m` if and only if `m • α = α`.
|
AddAction.mem_orbit
theorem AddAction.mem_orbit :
∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] (a : α) (m : M),
m +ᵥ a ∈ AddAction.orbit M a
The theorem `AddAction.mem_orbit` states that for any given add monoid `M`, any type `α` acting under `M`, any element `a` of type `α`, and any element `m` of the add monoid `M`, the result of applying the additive action of `m` to `a` (denoted `m +ᵥ a`) is a member of the orbit of `a` under the action of `M`. Here, the orbit of an element `a` under the action of `M` is defined as the set of all possible results of applying elements of `M` to `a` via the additive action.
More concisely: For any add monoid M, type α with an additive action, element a of α, and m in M, we have m +ᵥ a ∈ orbit a, where orbit a is the set of all elements obtained by applying elements of M to a via addition.
|
MulAction.mem_orbit
theorem MulAction.mem_orbit :
∀ {M : Type u} [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] (a : α) (m : M),
m • a ∈ MulAction.orbit M a
This theorem states that for any monoid `M` and any type `α` with a `MulAction` of `M` on `α`, for any element `a` of type `α` and any element `m` of the monoid `M`, the action of `m` on `a`, denoted by `m • a`, is an element of the orbit of `a` under the action of `M`. In terms of group theory, this means that the result of the group action of any element of the group on a specific element is always within the set of elements reachable by the group action on that element.
More concisely: For any monoid action on a type, the image of an element under the action of any element in the monoid lies in the orbit of that element.
|
AddAction.mem_fixedBy
theorem AddAction.mem_fixedBy :
∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] {m : M} {a : α},
a ∈ AddAction.fixedBy α m ↔ m +ᵥ a = a
The theorem `AddAction.mem_fixedBy` states that, for any additive monoid `M`, any type `α` with an additive action of `M`, any element `m` of `M`, and any element `a` of `α`, the element `a` is in the set of elements fixed by `m` (denoted as `AddAction.fixedBy α m`) if and only if the result of the additive action of `m` on `a` (denoted as `m +ᵥ a`) is equal to `a`. In other words, `a` is deemed "fixed" by `m` exactly when `m` acting on `a` leaves `a` unchanged.
More concisely: For any additive monoid M, any type α with an additive action of M, and any m in M and a in α, a is in the fixed set of m if and only if m + a = a.
|