Definition of orbit
, fixedPoints
and stabilizer
#
This file defines orbits, stabilizers, and other objects defined in terms of actions.
Main definitions #
The stabilizer of a point a
as an additive submonoid of M
.
Equations
Instances For
Equations
Equations
The submonoid of elements fixed under the whole action.
Equations
Instances For
The subgroup of elements fixed under the whole action.
Equations
Instances For
Equations
The quotient by MulAction.orbitRel
, given a name to enable dot notation.
Equations
Instances For
The quotient by AddAction.orbitRel
, given a name to enable dot notation.
Equations
Instances For
The orbit corresponding to an element of the quotient by MulAction.orbitRel
Equations
Instances For
The orbit corresponding to an element of the quotient by AddAction.orbitRel
Equations
Instances For
Note that hφ = Quotient.out_eq'
is a useful choice here.
Note that hφ = Quotient.out_eq'
is a useful choice here.
Equations
Equations
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
Instances For
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
Instances For
Decomposition of a type X
as a disjoint union of its orbits under a group action.
Equations
Instances For
Decomposition of a type X
as a disjoint union of its orbits under an additive group
action.
Equations
Instances For
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.
The stabilizer of an element under an action, i.e. what sends the element to itself. An additive subgroup.