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 #
Equations
- AddAction.instElemOrbit = AddAction.mk ⋯ ⋯
Equations
- MulAction.instElemOrbit = MulAction.mk ⋯ ⋯
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
Equations
Equations
The submonoid of elements fixed under the whole action.
Equations
- FixedPoints.submonoid M α = { carrier := MulAction.fixedPoints M α, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
The subgroup of elements fixed under the whole action.
Equations
- FixedPoints.subgroup M α = { toSubmonoid := FixedPoints.submonoid M α, inv_mem' := ⋯ }
Instances For
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))
Instances For
The additive submonoid of elements fixed under the whole action.
Equations
- FixedPoints.addSubmonoid M α = { carrier := MulAction.fixedPoints M α, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
The additive subgroup of elements fixed under the whole action.
Equations
- α^+M = { toAddSubmonoid := FixedPoints.addSubmonoid M α, neg_mem' := ⋯ }
Instances For
The notation for FixedPoints.addSubgroup
, chosen to resemble αᴹ
.
Equations
- «term_^+_» = Lean.ParserDescr.trailingNode `term_^+_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^+") (Lean.ParserDescr.cat `term 51))
Instances For
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
.
The action of an additive group on an orbit is transitive.
Equations
- ⋯ = ⋯
The action of a group on an orbit is transitive.
Equations
- ⋯ = ⋯
Equations
- AddAction.instAddAction H = inferInstanceAs (AddAction (↥H.toAddSubmonoid) α)
Equations
- MulAction.instMulAction H = inferInstanceAs (MulAction (↥H.toSubmonoid) α)
The relation 'in the same orbit'.
Equations
- AddAction.orbitRel G α = { r := fun (a b : α) => a ∈ AddAction.orbit G b, iseqv := ⋯ }
Instances For
The relation 'in the same orbit'.
Equations
- MulAction.orbitRel G α = { r := fun (a b : α) => a ∈ MulAction.orbit G b, iseqv := ⋯ }
Instances For
The quotient by AddAction.orbitRel
, given a name to enable dot notation.
Equations
Instances For
The quotient by MulAction.orbitRel
, given a name to enable dot notation.
Equations
Instances For
An additive action is pretransitive if and only if the quotient by
AddAction.orbitRel
is a subsingleton.
An action is pretransitive if and only if the quotient by MulAction.orbitRel
is a
subsingleton.
The orbit corresponding to an element of the quotient by AddAction.orbitRel
Equations
- x.orbit = Quotient.liftOn' x (AddAction.orbit G) ⋯
Instances For
The orbit corresponding to an element of the quotient by MulAction.orbitRel
Equations
- x.orbit = Quotient.liftOn' x (MulAction.orbit G) ⋯
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
Equations
- ⋯ = ⋯
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
- AddAction.selfEquivSigmaOrbits' G α = Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun (x : AddAction.orbitRel.Quotient G α) => Equiv.subtypeEquivRight ⋯)
Instances For
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
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
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
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
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
Equations
Equations
If the stabilizer of a
is S
, then the stabilizer of g • a
is gSg⁻¹
.
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
If the stabilizer of x
is S
, then the stabilizer of g +ᵥ x
is g + S + (-g)
.
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