Definition of orbit, fixedPoints and stabilizer #
This file defines orbits, stabilizers, and other objects defined in terms of actions.
Main definitions #
theorem
MulAction.mapsTo_smul_orbit
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
(m : M)
(a : α)
:
Set.MapsTo (fun (x : α) => m • x) (orbit M a) (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) (orbit M a) (orbit M a)
Equations
- MulAction.instElemOrbit = { smul := fun (m : M) => Set.MapsTo.restrict (fun (x : α) => m • x) (MulAction.orbit M a) (MulAction.orbit M a) ⋯, one_smul := ⋯, mul_smul := ⋯ }
Equations
- AddAction.instElemOrbit = { vadd := fun (m : M) => Set.MapsTo.restrict (fun (x : α) => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a) ⋯, zero_vadd := ⋯, add_vadd := ⋯ }
theorem
AddAction.orbit_addSubmonoid_subset
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
(S : AddSubmonoid M)
(a : α)
:
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.
instance
MulAction.instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq
{M : Type u}
[Monoid M]
{α : Type v}
[MulAction M α]
[DecidableEq α]
(a : α)
:
DecidablePred fun (x : M) => x ∈ stabilizerSubmonoid M a
Equations
instance
AddAction.instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq
{M : Type u}
[AddMonoid M]
{α : Type v}
[AddAction M α]
[DecidableEq α]
(a : α)
:
DecidablePred fun (x : M) => x ∈ 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' := ⋯ }
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' := ⋯ }
The notation for FixedPoints.subgroup, chosen to resemble αᴹ.
Equations
- FixedPoints.«term_^*_» = Lean.ParserDescr.trailingNode `FixedPoints.«term_^*_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^*") (Lean.ParserDescr.cat `term 51))
@[simp]
theorem
FixedPoints.subgroup_toSubmonoid
(M : Type u)
(α : Type v)
[Monoid M]
[Group α]
[MulDistribMulAction M α]
:
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
theorem
AddAction.addSubgroup_vadd_def
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
(a : ↥H)
(b : α)
:
theorem
AddAction.orbit_addSubgroup_subset
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(H : AddSubgroup G)
(a : α)
:
The relation 'in the same orbit'.
Equations
- MulAction.orbitRel G α = { r := fun (a b : α) => a ∈ MulAction.orbit G b, iseqv := ⋯ }
The relation 'in the same orbit'.
Equations
- AddAction.orbitRel G α = { r := fun (a b : α) => a ∈ AddAction.orbit G b, iseqv := ⋯ }
@[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
@[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
def
MulAction.orbitRel.Quotient.orbit
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : Quotient G α)
:
Set α
The orbit corresponding to an element of the quotient by MulAction.orbitRel
Equations
- x.orbit = Quotient.liftOn' x (MulAction.orbit G) ⋯
def
AddAction.orbitRel.Quotient.orbit
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : Quotient G α)
:
Set α
The orbit corresponding to an element of the quotient by AddAction.orbitRel
Equations
- x.orbit = Quotient.liftOn' x (AddAction.orbit G) ⋯
@[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.orbit_eq_orbit_out
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : Quotient G α)
{φ : Quotient G α → α}
(hφ : Function.RightInverse φ Quotient.mk')
:
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 : Quotient G α)
{φ : Quotient G α → α}
(hφ : Function.RightInverse φ Quotient.mk')
:
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 α]
:
theorem
AddAction.orbitRel.Quotient.orbit_injective
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
:
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)
:
instance
MulAction.instElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
(x : orbitRel.Quotient G α)
:
Equations
- MulAction.instElemOrbit_1 x = { smul := fun (g : G) => Set.MapsTo.restrict (fun (x : α) => g • x) x.orbit x.orbit ⋯, one_smul := ⋯, mul_smul := ⋯ }
instance
AddAction.instElemOrbit_1
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
(x : orbitRel.Quotient G α)
:
Equations
- AddAction.instElemOrbit_1 x = { vadd := fun (g : G) => Set.MapsTo.restrict (fun (x : α) => g +ᵥ x) x.orbit x.orbit ⋯, zero_vadd := ⋯, add_vadd := ⋯ }
@[simp]
theorem
AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{H : AddSubgroup G}
{x : Quotient G α}
{a b : ↑x.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
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
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.setCongr ⋯)
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.setCongr ⋯)
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.
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.
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' := ⋯ }
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' := ⋯ }
instance
MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[DecidableEq α]
(a : α)
:
DecidablePred fun (x : G) => x ∈ 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 ∈ 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 : β)
:
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 : β)
:
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 : β)
:
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 : β)
:
@[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)
:
@[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)
:
@[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 : β)
:
@[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 : β)
:
@[simp]
theorem
MulAction.stabilizer_mul_eq_left
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[Group α]
[IsScalarTower G α α]
(a b : α)
:
@[simp]
theorem
AddAction.stabilizer_add_eq_left
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
[AddGroup α]
[VAddAssocClass G α α]
(a b : α)
:
@[simp]
theorem
MulAction.stabilizer_mul_eq_right
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
[Group α]
[SMulCommClass G α α]
(a b : α)
:
@[simp]
theorem
AddAction.stabilizer_add_eq_right
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
[AddGroup α]
[VAddCommClass G α α]
(a b : α)
: