Basic properties of group actions #
This file primarily concerns itself with orbits, stabilizers, and other objects defined in terms of
actions. Despite this file being called basic, low-level helper lemmas for algebraic manipulation
of • belong elsewhere.
Main definitions #
@[simp]
theorem
MulAction.mem_orbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(a : α)
(m : M)
:
m • a ∈ MulAction.orbit M a
@[simp]
theorem
AddAction.mem_orbit
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(a : α)
(m : M)
:
m +ᵥ a ∈ AddAction.orbit M a
@[simp]
theorem
MulAction.mem_orbit_self
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(a : α)
:
a ∈ MulAction.orbit M a
@[simp]
theorem
AddAction.mem_orbit_self
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(a : α)
:
a ∈ AddAction.orbit M a
theorem
MulAction.orbit_nonempty
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(a : α)
:
(MulAction.orbit M a).Nonempty
theorem
AddAction.orbit_nonempty
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(a : α)
:
(AddAction.orbit M a).Nonempty
theorem
MulAction.mapsTo_smul_orbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(m : M)
(a : α)
:
Set.MapsTo (fun (x : α) => m • x) (MulAction.orbit M a) (MulAction.orbit M a)
theorem
AddAction.mapsTo_vadd_orbit
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(m : M)
(a : α)
:
Set.MapsTo (fun (x : α) => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a)
theorem
MulAction.smul_orbit_subset
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(m : M)
(a : α)
:
m • MulAction.orbit M a ⊆ MulAction.orbit M a
theorem
AddAction.vadd_orbit_subset
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(m : M)
(a : α)
:
m +ᵥ AddAction.orbit M a ⊆ AddAction.orbit M a
theorem
MulAction.orbit_smul_subset
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(m : M)
(a : α)
:
MulAction.orbit M (m • a) ⊆ MulAction.orbit M a
theorem
AddAction.orbit_vadd_subset
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(m : M)
(a : α)
:
AddAction.orbit M (m +ᵥ a) ⊆ AddAction.orbit M a
instance
MulAction.instElemOrbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{a : α}
:
MulAction M ↑(MulAction.orbit M a)
Equations
- MulAction.instElemOrbit = MulAction.mk ⋯ ⋯
instance
AddAction.instElemOrbit
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{a : α}
:
AddAction M ↑(AddAction.orbit M a)
Equations
- AddAction.instElemOrbit = AddAction.mk ⋯ ⋯
theorem
AddAction.instElemOrbit.proof_1
{M : Type u_2}
[AddMonoid M]
{α : Type u_1}
[AddAction M α]
{a : α}
(m : ↑(AddAction.orbit M a))
:
@[simp]
theorem
MulAction.orbit.coe_smul
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{a : α}
{m : M}
{a' : ↑(MulAction.orbit M a)}
:
@[simp]
theorem
AddAction.orbit.coe_vadd
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{a : α}
{m : M}
{a' : ↑(AddAction.orbit M a)}
:
theorem
MulAction.orbit_submonoid_subset
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(S : Submonoid M)
(a : α)
:
MulAction.orbit (↥S) a ⊆ MulAction.orbit M a
theorem
AddAction.orbit_addSubmonoid_subset
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(S : AddSubmonoid M)
(a : α)
:
AddAction.orbit (↥S) a ⊆ AddAction.orbit M a
theorem
MulAction.mem_orbit_of_mem_orbit_submonoid
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{S : Submonoid M}
{a : α}
{b : α}
(h : a ∈ MulAction.orbit (↥S) b)
:
a ∈ MulAction.orbit M b
theorem
AddAction.mem_orbit_of_mem_orbit_addSubmonoid
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{S : AddSubmonoid M}
{a : α}
{b : α}
(h : a ∈ AddAction.orbit (↥S) b)
:
a ∈ AddAction.orbit M b
theorem
MulAction.fst_mem_orbit_of_mem_orbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{β : Type u_1}
[MulAction M β]
{x : α × β}
{y : α × β}
(h : x ∈ MulAction.orbit M y)
:
x.1 ∈ MulAction.orbit M y.1
theorem
AddAction.fst_mem_orbit_of_mem_orbit
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{β : Type u_1}
[AddAction M β]
{x : α × β}
{y : α × β}
(h : x ∈ AddAction.orbit M y)
:
x.1 ∈ AddAction.orbit M y.1
theorem
MulAction.snd_mem_orbit_of_mem_orbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{β : Type u_1}
[MulAction M β]
{x : α × β}
{y : α × β}
(h : x ∈ MulAction.orbit M y)
:
x.2 ∈ MulAction.orbit M y.2
theorem
AddAction.snd_mem_orbit_of_mem_orbit
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{β : Type u_1}
[AddAction M β]
{x : α × β}
{y : α × β}
(h : x ∈ AddAction.orbit M y)
:
x.2 ∈ AddAction.orbit M y.2
theorem
Finite.finite_mulAction_orbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
[Finite M]
(a : α)
:
(MulAction.orbit M a).Finite
theorem
Finite.finite_addAction_orbit
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
[Finite M]
(a : α)
:
(AddAction.orbit M a).Finite
theorem
MulAction.orbit_eq_univ
(M : Type u)
[Monoid M]
{α : Type v}
[MulAction M α]
[MulAction.IsPretransitive M α]
(a : α)
:
MulAction.orbit M a = Set.univ
theorem
AddAction.orbit_eq_univ
(M : Type u)
[AddMonoid M]
{α : Type v}
[AddAction M α]
[AddAction.IsPretransitive M α]
(a : α)
:
AddAction.orbit M a = Set.univ
theorem
MulAction.fixed_eq_iInter_fixedBy
(M : Type u)
[Monoid M]
(α : Type v)
[MulAction M α]
:
MulAction.fixedPoints M α = ⋂ (m : M), MulAction.fixedBy α m
theorem
AddAction.fixed_eq_iInter_fixedBy
(M : Type u)
[AddMonoid M]
(α : Type v)
[AddAction M α]
:
AddAction.fixedPoints M α = ⋂ (m : M), AddAction.fixedBy α m
theorem
MulAction.mem_fixedPoints'
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{a : α}
:
a ∈ MulAction.fixedPoints M α ↔ ∀ a' ∈ MulAction.orbit M a, a' = a
theorem
AddAction.mem_fixedPoints'
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{a : α}
:
a ∈ AddAction.fixedPoints M α ↔ ∀ a' ∈ AddAction.orbit M a, a' = a
theorem
MulAction.mem_fixedPoints_iff_card_orbit_eq_one
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
{a : α}
[Fintype ↑(MulAction.orbit M a)]
:
a ∈ MulAction.fixedPoints M α ↔ Fintype.card ↑(MulAction.orbit M a) = 1
theorem
AddAction.mem_fixedPoints_iff_card_orbit_eq_one
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
{a : α}
[Fintype ↑(AddAction.orbit M a)]
:
a ∈ AddAction.fixedPoints M α ↔ Fintype.card ↑(AddAction.orbit M a) = 1
def
AddAction.stabilizerAddSubmonoid
(M : Type u)
[AddMonoid M]
{α : Type v}
[AddAction M α]
(a : α)
:
The stabilizer of a point a as an additive submonoid of M.
Equations
- AddAction.stabilizerAddSubmonoid M a = { carrier := {m : M | m +ᵥ a = a}, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
instance
MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
[DecidableEq α]
(a : α)
:
DecidablePred fun (x : M) => x ∈ MulAction.stabilizerSubmonoid M a
Equations
instance
AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
[DecidableEq α]
(a : α)
:
DecidablePred fun (x : M) => x ∈ AddAction.stabilizerAddSubmonoid M a
Equations
def
FixedPoints.submonoid
(M : Type u)
(α : Type v)
[Monoid M]
[Monoid α]
[MulDistribMulAction M α]
:
The submonoid of elements fixed under the whole action.
Equations
- FixedPoints.submonoid M α = { carrier := MulAction.fixedPoints M α, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
@[simp]
theorem
FixedPoints.mem_submonoid
(M : Type u)
(α : Type v)
[Monoid M]
[Monoid α]
[MulDistribMulAction M α]
(a : α)
:
a ∈ FixedPoints.submonoid M α ↔ ∀ (m : M), m • a = a
def
FixedPoints.subgroup
(M : Type u)
(α : Type v)
[Monoid M]
[Group α]
[MulDistribMulAction M α]
:
Subgroup α
The subgroup of elements fixed under the whole action.
Equations
- FixedPoints.subgroup M α = { toSubmonoid := FixedPoints.submonoid M α, inv_mem' := ⋯ }
Instances For
@[simp]
theorem
FixedPoints.mem_subgroup
(M : Type u)
(α : Type v)
[Monoid M]
[Group α]
[MulDistribMulAction M α]
(a : α)
:
a ∈ FixedPoints.subgroup M α ↔ ∀ (m : M), m • a = a
@[simp]
theorem
FixedPoints.subgroup_toSubmonoid
(M : Type u)
(α : Type v)
[Monoid M]
[Group α]
[MulDistribMulAction M α]
:
(FixedPoints.subgroup M α).toSubmonoid = FixedPoints.submonoid M α
def
FixedPoints.addSubmonoid
(M : Type u)
(α : Type v)
[Monoid M]
[AddMonoid α]
[DistribMulAction M α]
:
The additive submonoid of elements fixed under the whole action.
Equations
- FixedPoints.addSubmonoid M α = { carrier := MulAction.fixedPoints M α, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
@[simp]
theorem
FixedPoints.mem_addSubmonoid
(M : Type u)
(α : Type v)
[Monoid M]
[AddMonoid α]
[DistribMulAction M α]
(a : α)
:
a ∈ FixedPoints.addSubmonoid M α ↔ ∀ (m : M), m • a = a
def
FixedPoints.addSubgroup
(M : Type u)
(α : Type v)
[Monoid M]
[AddGroup α]
[DistribMulAction M α]
:
The additive subgroup of elements fixed under the whole action.
Equations
- α^+M = { toAddSubmonoid := FixedPoints.addSubmonoid M α, neg_mem' := ⋯ }
Instances For
@[simp]
theorem
FixedPoints.addSubgroup_toAddSubmonoid
(M : Type u)
(α : Type v)
[Monoid M]
[AddGroup α]
[DistribMulAction M α]
:
(α^+M).toAddSubmonoid = FixedPoints.addSubmonoid M α
theorem
smul_cancel_of_non_zero_divisor
{M : Type u_1}
{R : Type u_2}
[Monoid M]
[NonUnitalNonAssocRing R]
[DistribMulAction M R]
(k : M)
(h : ∀ (x : R), k • x = 0 → x = 0)
{a : R}
{b : R}
(h' : k • a = k • b)
:
a = b
smul by a k : M over a ring is injective, if k is not a zero divisor.
The general theory of such k is elaborated by IsSMulRegular.
The typeclass that restricts all terms of M to have this property is NoZeroSMulDivisors.
@[simp]
theorem
MulAction.smul_orbit
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(g : G)
(a : α)
:
g • MulAction.orbit G a = MulAction.orbit G a
@[simp]
theorem
AddAction.vadd_orbit
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(g : G)
(a : α)
:
g +ᵥ AddAction.orbit G a = AddAction.orbit G a
@[simp]
theorem
MulAction.orbit_smul
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(g : G)
(a : α)
:
MulAction.orbit G (g • a) = MulAction.orbit G a
@[simp]
theorem
AddAction.orbit_vadd
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(g : G)
(a : α)
:
AddAction.orbit G (g +ᵥ a) = AddAction.orbit G a
instance
MulAction.instIsPretransitiveElemOrbit
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(a : α)
:
MulAction.IsPretransitive G ↑(MulAction.orbit G a)
The action of a group on an orbit is transitive.
Equations
- ⋯ = ⋯
instance
AddAction.instIsPretransitiveElemOrbit
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(a : α)
:
AddAction.IsPretransitive G ↑(AddAction.orbit G a)
The action of an additive group on an orbit is transitive.
Equations
- ⋯ = ⋯
theorem
MulAction.orbit_eq_iff
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{a : α}
{b : α}
:
MulAction.orbit G a = MulAction.orbit G b ↔ a ∈ MulAction.orbit G b
theorem
AddAction.orbit_eq_iff
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{a : α}
{b : α}
:
AddAction.orbit G a = AddAction.orbit G b ↔ a ∈ AddAction.orbit G b
theorem
MulAction.mem_orbit_smul
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(g : G)
(a : α)
:
a ∈ MulAction.orbit G (g • a)
theorem
AddAction.mem_orbit_vadd
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(g : G)
(a : α)
:
a ∈ AddAction.orbit G (g +ᵥ a)
theorem
MulAction.smul_mem_orbit_smul
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(g : G)
(h : G)
(a : α)
:
g • a ∈ MulAction.orbit G (h • a)
theorem
AddAction.vadd_mem_orbit_vadd
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(g : G)
(h : G)
(a : α)
:
g +ᵥ a ∈ AddAction.orbit G (h +ᵥ a)
instance
MulAction.instMulAction
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(H : Subgroup G)
:
MulAction (↥H) α
Equations
- MulAction.instMulAction H = inferInstanceAs (MulAction (↥H.toSubmonoid) α)
instance
AddAction.instAddAction
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H : AddSubgroup G)
:
AddAction (↥H) α
Equations
- AddAction.instAddAction H = inferInstanceAs (AddAction (↥H.toAddSubmonoid) α)
theorem
MulAction.orbit_subgroup_subset
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(H : Subgroup G)
(a : α)
:
MulAction.orbit (↥H) a ⊆ MulAction.orbit G a
theorem
AddAction.orbit_addSubgroup_subset
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H : AddSubgroup G)
(a : α)
:
AddAction.orbit (↥H) a ⊆ AddAction.orbit G a
theorem
MulAction.mem_orbit_of_mem_orbit_subgroup
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{H : Subgroup G}
{a : α}
{b : α}
(h : a ∈ MulAction.orbit (↥H) b)
:
a ∈ MulAction.orbit G b
theorem
AddAction.mem_orbit_of_mem_orbit_addSubgroup
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{a : α}
{b : α}
(h : a ∈ AddAction.orbit (↥H) b)
:
a ∈ AddAction.orbit G b
theorem
MulAction.mem_orbit_symm
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{a₁ : α}
{a₂ : α}
:
a₁ ∈ MulAction.orbit G a₂ ↔ a₂ ∈ MulAction.orbit G a₁
theorem
AddAction.mem_orbit_symm
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{a₁ : α}
{a₂ : α}
:
a₁ ∈ AddAction.orbit G a₂ ↔ a₂ ∈ AddAction.orbit G a₁
theorem
MulAction.mem_subgroup_orbit_iff
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{H : Subgroup G}
{x : α}
{a : ↑(MulAction.orbit G x)}
{b : ↑(MulAction.orbit G x)}
:
a ∈ MulAction.orbit (↥H) b ↔ ↑a ∈ MulAction.orbit ↥H ↑b
theorem
AddAction.mem_addSubgroup_orbit_iff
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{x : α}
{a : ↑(AddAction.orbit G x)}
{b : ↑(AddAction.orbit G x)}
:
a ∈ AddAction.orbit (↥H) b ↔ ↑a ∈ AddAction.orbit ↥H ↑b
The relation 'in the same orbit'.
Equations
- MulAction.orbitRel G α = { r := fun (a b : α) => a ∈ MulAction.orbit G b, iseqv := ⋯ }
Instances For
The relation 'in the same orbit'.
Equations
- AddAction.orbitRel G α = { r := fun (a b : α) => a ∈ AddAction.orbit G b, iseqv := ⋯ }
Instances For
theorem
AddAction.orbitRel.proof_1
(G : Type u_2)
(α : Type u_1)
[AddGroup G]
[AddAction G α]
:
Equivalence fun (a b : α) => a ∈ AddAction.orbit G b
theorem
MulAction.orbitRel_apply
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{a : α}
{b : α}
:
(MulAction.orbitRel G α) a b ↔ a ∈ MulAction.orbit G b
theorem
AddAction.orbitRel_apply
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{a : α}
{b : α}
:
(AddAction.orbitRel G α) a b ↔ a ∈ AddAction.orbit G b
@[deprecated]
theorem
MulAction.orbitRel_r_apply
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{a : α}
{b : α}
:
(MulAction.orbitRel G α) a b ↔ a ∈ MulAction.orbit G b
Alias of MulAction.orbitRel_apply.
@[deprecated]
theorem
AddAction.orbitRel_r_apply
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{a : α}
{b : α}
:
(AddAction.orbitRel G α) a b ↔ a ∈ AddAction.orbit G b
theorem
MulAction.orbitRel_subgroup_le
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(H : Subgroup G)
:
MulAction.orbitRel (↥H) α ≤ MulAction.orbitRel G α
theorem
AddAction.orbitRel_addSubgroup_le
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H : AddSubgroup G)
:
AddAction.orbitRel (↥H) α ≤ AddAction.orbitRel G α
theorem
MulAction.orbitRel_subgroupOf
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(H : Subgroup G)
(K : Subgroup G)
:
MulAction.orbitRel (↥(H.subgroupOf K)) α = MulAction.orbitRel (↥(H ⊓ K)) α
theorem
AddAction.orbitRel_addSubgroupOf
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H : AddSubgroup G)
(K : AddSubgroup G)
:
AddAction.orbitRel (↥(H.addSubgroupOf K)) α = AddAction.orbitRel (↥(H ⊓ K)) α
@[reducible, inline]
abbrev
MulAction.orbitRel.Quotient
(G : Type u_1)
(α : Type u_2)
[Group G]
[MulAction G α]
:
Type u_2
The quotient by MulAction.orbitRel, given a name to enable dot notation.
Equations
Instances For
@[reducible, inline]
abbrev
AddAction.orbitRel.Quotient
(G : Type u_1)
(α : Type u_2)
[AddGroup G]
[AddAction G α]
:
Type u_2
The quotient by AddAction.orbitRel, given a name to enable dot notation.
Equations
Instances For
theorem
MulAction.pretransitive_iff_subsingleton_quotient
(G : Type u_1)
(α : Type u_2)
[Group G]
[MulAction G α]
:
An action is pretransitive if and only if the quotient by MulAction.orbitRel is a
subsingleton.
theorem
AddAction.pretransitive_iff_subsingleton_quotient
(G : Type u_1)
(α : Type u_2)
[AddGroup G]
[AddAction G α]
:
An additive action is pretransitive if and only if the quotient by
AddAction.orbitRel is a subsingleton.
def
MulAction.orbitRel.Quotient.orbit
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : MulAction.orbitRel.Quotient G α)
:
Set α
The orbit corresponding to an element of the quotient by MulAction.orbitRel
Equations
- x.orbit = Quotient.liftOn' x (MulAction.orbit G) ⋯
Instances For
theorem
AddAction.orbitRel.Quotient.orbit.proof_1
{G : Type u_2}
{α : Type u_1}
[AddGroup G]
[AddAction G α]
:
∀ (x x_1 : α), x ∈ AddAction.orbit G x_1 → AddAction.orbit G x = AddAction.orbit G x_1
def
AddAction.orbitRel.Quotient.orbit
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : AddAction.orbitRel.Quotient G α)
:
Set α
The orbit corresponding to an element of the quotient by AddAction.orbitRel
Equations
- x.orbit = Quotient.liftOn' x (AddAction.orbit G) ⋯
Instances For
@[simp]
theorem
MulAction.orbitRel.Quotient.orbit_mk
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(a : α)
:
@[simp]
theorem
AddAction.orbitRel.Quotient.orbit_mk
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(a : α)
:
theorem
MulAction.orbitRel.Quotient.mem_orbit
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{a : α}
{x : MulAction.orbitRel.Quotient G α}
:
a ∈ x.orbit ↔ Quotient.mk'' a = x
theorem
AddAction.orbitRel.Quotient.mem_orbit
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{a : α}
{x : AddAction.orbitRel.Quotient G α}
:
a ∈ x.orbit ↔ Quotient.mk'' a = x
theorem
MulAction.orbitRel.Quotient.orbit_eq_orbit_out
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : MulAction.orbitRel.Quotient G α)
{φ : MulAction.orbitRel.Quotient G α → α}
(hφ : Function.RightInverse φ Quotient.mk')
:
x.orbit = MulAction.orbit G (φ x)
Note that hφ = Quotient.out_eq' is a useful choice here.
theorem
AddAction.orbitRel.Quotient.orbit_eq_orbit_out
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : AddAction.orbitRel.Quotient G α)
{φ : AddAction.orbitRel.Quotient G α → α}
(hφ : Function.RightInverse φ Quotient.mk')
:
x.orbit = AddAction.orbit G (φ x)
Note that hφ = Quotient.out_eq' is a useful choice here.
theorem
MulAction.orbitRel.Quotient.orbit_injective
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
:
Function.Injective MulAction.orbitRel.Quotient.orbit
theorem
AddAction.orbitRel.Quotient.orbit_injective
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
:
Function.Injective AddAction.orbitRel.Quotient.orbit
@[simp]
theorem
MulAction.orbitRel.Quotient.orbit_inj
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x : MulAction.orbitRel.Quotient G α}
{y : MulAction.orbitRel.Quotient G α}
:
@[simp]
theorem
AddAction.orbitRel.Quotient.orbit_inj
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x : AddAction.orbitRel.Quotient G α}
{y : AddAction.orbitRel.Quotient G α}
:
theorem
AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{a : α}
{b : α}
(h : ⟦a⟧ = ⟦b⟧)
:
⟦a⟧ = ⟦b⟧
theorem
MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq'
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{H : Subgroup G}
{a : α}
{b : α}
(h : Quotient.mk'' a = Quotient.mk'' b)
:
theorem
AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq'
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{a : α}
{b : α}
(h : Quotient.mk'' a = Quotient.mk'' b)
:
theorem
MulAction.orbitRel.Quotient.orbit_nonempty
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : MulAction.orbitRel.Quotient G α)
:
x.orbit.Nonempty
theorem
AddAction.orbitRel.Quotient.orbit_nonempty
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : AddAction.orbitRel.Quotient G α)
:
x.orbit.Nonempty
theorem
MulAction.orbitRel.Quotient.mapsTo_smul_orbit
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(g : G)
(x : MulAction.orbitRel.Quotient G α)
:
Set.MapsTo (fun (x : α) => g • x) x.orbit x.orbit
theorem
AddAction.orbitRel.Quotient.mapsTo_vadd_orbit
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(g : G)
(x : AddAction.orbitRel.Quotient G α)
:
Set.MapsTo (fun (x : α) => g +ᵥ x) x.orbit x.orbit
instance
MulAction.instElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : MulAction.orbitRel.Quotient G α)
:
MulAction G ↑x.orbit
Equations
instance
AddAction.instElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : AddAction.orbitRel.Quotient G α)
:
AddAction G ↑x.orbit
Equations
theorem
AddAction.instElemOrbit_1.proof_1
{G : Type u_2}
{α : Type u_1}
[AddGroup G]
[AddAction G α]
(x : AddAction.orbitRel.Quotient G α)
(a : ↑x.orbit)
:
@[simp]
theorem
MulAction.orbitRel.Quotient.orbit.coe_smul
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{g : G}
{x : MulAction.orbitRel.Quotient G α}
{a : ↑x.orbit}
:
@[simp]
theorem
AddAction.orbitRel.Quotient.orbit.coe_vadd
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{g : G}
{x : AddAction.orbitRel.Quotient G α}
{a : ↑x.orbit}
:
instance
MulAction.instIsPretransitiveElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : MulAction.orbitRel.Quotient G α)
:
MulAction.IsPretransitive G ↑x.orbit
Equations
- ⋯ = ⋯
instance
AddAction.instIsPretransitiveElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : AddAction.orbitRel.Quotient G α)
:
AddAction.IsPretransitive G ↑x.orbit
Equations
- ⋯ = ⋯
@[simp]
theorem
MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{H : Subgroup G}
{x : MulAction.orbitRel.Quotient G α}
{a : ↑x.orbit}
{b : ↑x.orbit}
:
↑a ∈ MulAction.orbit ↥H ↑b ↔ a ∈ MulAction.orbit (↥H) b
@[simp]
theorem
AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{x : AddAction.orbitRel.Quotient G α}
{a : ↑x.orbit}
{b : ↑x.orbit}
:
↑a ∈ AddAction.orbit ↥H ↑b ↔ a ∈ AddAction.orbit (↥H) b
theorem
AddAction.orbitRel.Quotient.addSubgroup_quotient_eq_iff
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{x : AddAction.orbitRel.Quotient G α}
{a : ↑x.orbit}
{b : ↑x.orbit}
:
theorem
MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff'
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{H : Subgroup G}
{x : MulAction.orbitRel.Quotient G α}
{a : ↑x.orbit}
{b : ↑x.orbit}
{c : α}
(h : ⟦a⟧ = ⟦b⟧)
:
↑a ∈ MulAction.orbit (↥H) c ↔ ↑b ∈ MulAction.orbit (↥H) c
theorem
AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff'
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{x : AddAction.orbitRel.Quotient G α}
{a : ↑x.orbit}
{b : ↑x.orbit}
{c : α}
(h : ⟦a⟧ = ⟦b⟧)
:
↑a ∈ AddAction.orbit (↥H) c ↔ ↑b ∈ AddAction.orbit (↥H) c
def
MulAction.selfEquivSigmaOrbits'
(G : Type u_1)
(α : Type u_2)
[Group G]
[MulAction G α]
:
α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑ω.orbit
Decomposition of a type X as a disjoint union of its orbits under a group action.
This version is expressed in terms of MulAction.orbitRel.Quotient.orbit instead of
MulAction.orbit, to avoid mentioning Quotient.out'.
Equations
- MulAction.selfEquivSigmaOrbits' G α = Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun (x : MulAction.orbitRel.Quotient G α) => Equiv.subtypeEquivRight ⋯)
Instances For
theorem
AddAction.selfEquivSigmaOrbits'.proof_1
(G : Type u_2)
(α : Type u_1)
[AddGroup G]
[AddAction G α]
:
∀ (x : AddAction.orbitRel.Quotient G α) (x_1 : α), Quotient.mk'' x_1 = x ↔ x_1 ∈ x.orbit
def
AddAction.selfEquivSigmaOrbits'
(G : Type u_1)
(α : Type u_2)
[AddGroup G]
[AddAction G α]
:
α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑ω.orbit
Decomposition of a type X as a disjoint union of its orbits under an additive group action.
This version is expressed in terms of AddAction.orbitRel.Quotient.orbit instead of
AddAction.orbit, to avoid mentioning Quotient.out'.
Equations
- AddAction.selfEquivSigmaOrbits' G α = Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun (x : AddAction.orbitRel.Quotient G α) => Equiv.subtypeEquivRight ⋯)
Instances For
def
MulAction.selfEquivSigmaOrbits
(G : Type u_1)
(α : Type u_2)
[Group G]
[MulAction G α]
:
α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑(MulAction.orbit G (Quotient.out' ω))
Decomposition of a type X as a disjoint union of its orbits under a group action.
Equations
- MulAction.selfEquivSigmaOrbits G α = (MulAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun (x : MulAction.orbitRel.Quotient G α) => Equiv.Set.ofEq ⋯)
Instances For
theorem
AddAction.selfEquivSigmaOrbits.proof_1
(G : Type u_2)
(α : Type u_1)
[AddGroup G]
[AddAction G α]
:
∀ (x : AddAction.orbitRel.Quotient G α), x.orbit = AddAction.orbit G (Quotient.out' x)
def
AddAction.selfEquivSigmaOrbits
(G : Type u_1)
(α : Type u_2)
[AddGroup G]
[AddAction G α]
:
α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑(AddAction.orbit G (Quotient.out' ω))
Decomposition of a type X as a disjoint union of its orbits under an additive group
action.
Equations
- AddAction.selfEquivSigmaOrbits G α = (AddAction.selfEquivSigmaOrbits' G α).trans (Equiv.sigmaCongrRight fun (x : AddAction.orbitRel.Quotient G α) => Equiv.Set.ofEq ⋯)
Instances For
theorem
MulAction.univ_eq_iUnion_orbit
(G : Type u_1)
(α : Type u_2)
[Group G]
[MulAction G α]
:
Set.univ = ⋃ (x : MulAction.orbitRel.Quotient G α), x.orbit
Decomposition of a type X as a disjoint union of its orbits under a group action.
Phrased as a set union. See MulAction.selfEquivSigmaOrbits for the type isomorphism.
theorem
AddAction.univ_eq_iUnion_orbit
(G : Type u_1)
(α : Type u_2)
[AddGroup G]
[AddAction G α]
:
Set.univ = ⋃ (x : AddAction.orbitRel.Quotient G α), x.orbit
Decomposition of a type X as a disjoint union of its orbits under an additive group
action. Phrased as a set union. See AddAction.selfEquivSigmaOrbits for the type isomorphism.
theorem
Finite.of_finite_mulAction_orbitRel_quotient
(G : Type u_1)
(α : Type u_2)
[Group G]
[MulAction G α]
[Finite G]
[Finite (MulAction.orbitRel.Quotient G α)]
:
Finite α
theorem
Finite.of_finite_addAction_orbitRel_quotient
(G : Type u_1)
(α : Type u_2)
[AddGroup G]
[AddAction G α]
[Finite G]
[Finite (AddAction.orbitRel.Quotient G α)]
:
Finite α
theorem
MulAction.orbitRel_le_fst
(G : Type u_1)
(α : Type u_2)
(β : Type u_3)
[Group G]
[MulAction G α]
[MulAction G β]
:
MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (MulAction.orbitRel G α)
theorem
AddAction.orbitRel_le_fst
(G : Type u_1)
(α : Type u_2)
(β : Type u_3)
[AddGroup G]
[AddAction G α]
[AddAction G β]
:
AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (AddAction.orbitRel G α)
theorem
MulAction.orbitRel_le_snd
(G : Type u_1)
(α : Type u_2)
(β : Type u_3)
[Group G]
[MulAction G α]
[MulAction G β]
:
MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (MulAction.orbitRel G β)
theorem
AddAction.orbitRel_le_snd
(G : Type u_1)
(α : Type u_2)
(β : Type u_3)
[AddGroup G]
[AddAction G α]
[AddAction G β]
:
AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.snd (AddAction.orbitRel G β)
def
MulAction.stabilizer
(G : Type u_1)
{α : Type u_2}
[Group G]
[MulAction G α]
(a : α)
:
Subgroup G
The stabilizer of an element under an action, i.e. what sends the element to itself. A subgroup.
Equations
- MulAction.stabilizer G a = { toSubmonoid := MulAction.stabilizerSubmonoid G a, inv_mem' := ⋯ }
Instances For
The stabilizer of an element under an action, i.e. what sends the element to itself. An additive subgroup.
Equations
- AddAction.stabilizer G a = { toAddSubmonoid := AddAction.stabilizerAddSubmonoid G a, neg_mem' := ⋯ }
Instances For
instance
MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[DecidableEq α]
(a : α)
:
DecidablePred fun (x : G) => x ∈ MulAction.stabilizer G a
Equations
instance
AddAction.instDecidablePredMemAddSubgroupStabilizerOfDecidableEq
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
[DecidableEq α]
(a : α)
:
DecidablePred fun (x : G) => x ∈ AddAction.stabilizer G a
Equations
theorem
MulAction.le_stabilizer_smul_left
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Group G]
[MulAction G α]
[MulAction G β]
[SMul α β]
[IsScalarTower G α β]
(a : α)
(b : β)
:
MulAction.stabilizer G a ≤ MulAction.stabilizer G (a • b)
theorem
AddAction.le_stabilizer_vadd_left
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddGroup G]
[AddAction G α]
[AddAction G β]
[VAdd α β]
[VAddAssocClass G α β]
(a : α)
(b : β)
:
AddAction.stabilizer G a ≤ AddAction.stabilizer G (a +ᵥ b)
theorem
MulAction.le_stabilizer_smul_right
{α : Type u_2}
{β : Type u_3}
{G' : Type u_4}
[Group G']
[SMul α β]
[MulAction G' β]
[SMulCommClass G' α β]
(a : α)
(b : β)
:
MulAction.stabilizer G' b ≤ MulAction.stabilizer G' (a • b)
theorem
AddAction.le_stabilizer_vadd_right
{α : Type u_2}
{β : Type u_3}
{G' : Type u_4}
[AddGroup G']
[VAdd α β]
[AddAction G' β]
[VAddCommClass G' α β]
(a : α)
(b : β)
:
AddAction.stabilizer G' b ≤ AddAction.stabilizer G' (a +ᵥ b)
@[simp]
theorem
MulAction.stabilizer_smul_eq_left
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Group G]
[MulAction G α]
[MulAction G β]
[SMul α β]
[IsScalarTower G α β]
(a : α)
(b : β)
(h : Function.Injective fun (x : α) => x • b)
:
MulAction.stabilizer G (a • b) = MulAction.stabilizer G a
@[simp]
theorem
AddAction.stabilizer_vadd_eq_left
{G : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddGroup G]
[AddAction G α]
[AddAction G β]
[VAdd α β]
[VAddAssocClass G α β]
(a : α)
(b : β)
(h : Function.Injective fun (x : α) => x +ᵥ b)
:
AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G a
@[simp]
theorem
MulAction.stabilizer_smul_eq_right
{G : Type u_1}
{β : Type u_3}
[Group G]
[MulAction G β]
{α : Type u_4}
[Group α]
[MulAction α β]
[SMulCommClass G α β]
(a : α)
(b : β)
:
MulAction.stabilizer G (a • b) = MulAction.stabilizer G b
@[simp]
theorem
AddAction.stabilizer_vadd_eq_right
{G : Type u_1}
{β : Type u_3}
[AddGroup G]
[AddAction G β]
{α : Type u_4}
[AddGroup α]
[AddAction α β]
[VAddCommClass G α β]
(a : α)
(b : β)
:
AddAction.stabilizer G (a +ᵥ b) = AddAction.stabilizer G b
@[simp]
theorem
MulAction.stabilizer_mul_eq_left
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[Group α]
[IsScalarTower G α α]
(a : α)
(b : α)
:
MulAction.stabilizer G (a * b) = MulAction.stabilizer G a
@[simp]
theorem
AddAction.stabilizer_add_eq_left
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
[AddGroup α]
[VAddAssocClass G α α]
(a : α)
(b : α)
:
AddAction.stabilizer G (a + b) = AddAction.stabilizer G a
@[simp]
theorem
MulAction.stabilizer_mul_eq_right
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[Group α]
[SMulCommClass G α α]
(a : α)
(b : α)
:
MulAction.stabilizer G (a * b) = MulAction.stabilizer G b
@[simp]
theorem
AddAction.stabilizer_add_eq_right
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
[AddGroup α]
[VAddCommClass G α α]
(a : α)
(b : α)
:
AddAction.stabilizer G (a + b) = AddAction.stabilizer G b
theorem
MulAction.stabilizer_smul_eq_stabilizer_map_conj
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(g : G)
(a : α)
:
MulAction.stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MulAction.stabilizer G a)
If the stabilizer of a is S, then the stabilizer of g • a is gSg⁻¹.
noncomputable def
MulAction.stabilizerEquivStabilizerOfOrbitRel
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{a : α}
{b : α}
(h : (MulAction.orbitRel G α) a b)
:
↥(MulAction.stabilizer G a) ≃* ↥(MulAction.stabilizer G b)
A bijection between the stabilizers of two elements in the same orbit.
Equations
- MulAction.stabilizerEquivStabilizerOfOrbitRel h = (MulEquiv.subgroupCongr ⋯).trans (MulEquiv.subgroupMap (MulAut.conj (Classical.choose h)) (MulAction.stabilizer G b)).symm
Instances For
theorem
AddAction.stabilizer_vadd_eq_stabilizer_map_conj
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(g : G)
(a : α)
:
AddAction.stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (AddAction.stabilizer G a)
If the stabilizer of x is S, then the stabilizer of g +ᵥ x is g + S + (-g).
noncomputable def
AddAction.stabilizerEquivStabilizerOfOrbitRel
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{a : α}
{b : α}
(h : (AddAction.orbitRel G α) a b)
:
↥(AddAction.stabilizer G a) ≃+ ↥(AddAction.stabilizer G b)
A bijection between the stabilizers of two elements in the same orbit.
Equations
- AddAction.stabilizerEquivStabilizerOfOrbitRel h = (AddEquiv.addSubgroupCongr ⋯).trans (AddEquiv.addSubgroupMap (AddAut.conj (Classical.choose h)) (AddAction.stabilizer G b)).symm
Instances For
theorem
Equiv.swap_mem_stabilizer
{α : Type u_1}
[DecidableEq α]
{S : Set α}
{a : α}
{b : α}
:
Equiv.swap a b ∈ MulAction.stabilizer (Equiv.Perm α) S ↔ (a ∈ S ↔ b ∈ S)