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

• MulAction.orbit
• MulAction.fixedPoints
• MulAction.fixedBy
• MulAction.stabilizer

def AddAction.orbit (M : Type u) {α : Type v} [AddMonoid M] [AddAction M α] (a : α) : Set α

The orbit of an element under an action.

Equations

• AddAction.orbit M a = Set.range fun m => m +ᵥ a

def MulAction.orbit (M : Type u) {α : Type v} [Monoid M] [MulAction M α] (a : α) : Set α

The orbit of an element under an action.

Equations

• MulAction.orbit M a = Set.range fun m => m • a

theorem AddAction.mem_orbit_iff {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] {a₁ : α} {a₂ : α} : a₂ ∈ AddAction.orbit M a₁ ↔ ∃ x, x +ᵥ a₁ = a₂

theorem MulAction.mem_orbit_iff {M : Type u} {α : Type v} [Monoid M] [MulAction M α] {a₁ : α} {a₂ : α} : a₂ ∈ MulAction.orbit M a₁ ↔ ∃ x, x • a₁ = a₂

@[simp]

theorem AddAction.mem_orbit {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] (a : α) (x : M) : x +ᵥ a ∈ AddAction.orbit M a

@[simp]

theorem MulAction.mem_orbit {M : Type u} {α : Type v} [Monoid M] [MulAction M α] (a : α) (x : M) : x • a ∈ MulAction.orbit M a

@[simp]

theorem AddAction.mem_orbit_self {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] (a : α) : a ∈ AddAction.orbit M a

@[simp]

theorem MulAction.mem_orbit_self {M : Type u} {α : Type v} [Monoid M] [MulAction M α] (a : α) : a ∈ MulAction.orbit M a

theorem AddAction.orbit_nonempty {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] (a : α) : Set.Nonempty (AddAction.orbit M a)

theorem MulAction.orbit_nonempty {M : Type u} {α : Type v} [Monoid M] [MulAction M α] (a : α) : Set.Nonempty (MulAction.orbit M a)

theorem AddAction.mapsTo_vadd_orbit {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] (m : M) (a : α) : Set.MapsTo ((fun x x_1 => x +ᵥ x_1) m) (AddAction.orbit M a) (AddAction.orbit M a)

theorem MulAction.mapsTo_smul_orbit {M : Type u} {α : Type v} [Monoid M] [MulAction M α] (m : M) (a : α) : Set.MapsTo ((fun x x_1 => x • x_1) m) (MulAction.orbit M a) (MulAction.orbit M a)

theorem AddAction.vadd_orbit_subset {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] (m : M) (a : α) : m +ᵥ AddAction.orbit M a ⊆ AddAction.orbit M a

theorem MulAction.smul_orbit_subset {M : Type u} {α : Type v} [Monoid M] [MulAction M α] (m : M) (a : α) : m • MulAction.orbit M a ⊆ MulAction.orbit M a

theorem AddAction.orbit_vadd_subset {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] (m : M) (a : α) : AddAction.orbit M (m +ᵥ a) ⊆ AddAction.orbit M a

theorem MulAction.orbit_smul_subset {M : Type u} {α : Type v} [Monoid M] [MulAction M α] (m : M) (a : α) : MulAction.orbit M (m • a) ⊆ MulAction.orbit M a

theorem AddAction.instAddActionElemOrbit.proof_2 {M : Type u_2} {α : Type u_1} [AddMonoid M] [AddAction M α] {a : α} (m : M) (m' : M) (a' : ↑(AddAction.orbit M a)) : m + m' +ᵥ a' = m +ᵥ (m' +ᵥ a')

instance AddAction.instAddActionElemOrbit {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] {a : α} : AddAction M ↑(AddAction.orbit M a)

Equations

• AddAction.instAddActionElemOrbit = AddAction.mk (_ : ∀ (m : ↑(AddAction.orbit M a)), 0 +ᵥ m = m) (_ : ∀ (m m' : M) (a' : ↑(AddAction.orbit M a)), m + m' +ᵥ a' = m +ᵥ (m' +ᵥ a'))

theorem AddAction.instAddActionElemOrbit.proof_1 {M : Type u_2} {α : Type u_1} [AddMonoid M] [AddAction M α] {a : α} (m : ↑(AddAction.orbit M a)) : 0 +ᵥ m = m

instance MulAction.instMulActionElemOrbit {M : Type u} {α : Type v} [Monoid M] [MulAction M α] {a : α} : MulAction M ↑(MulAction.orbit M a)

Equations

• MulAction.instMulActionElemOrbit = MulAction.mk (_ : ∀ (m : ↑(MulAction.orbit M a)), 1 • m = m) (_ : ∀ (m m' : M) (a' : ↑(MulAction.orbit M a)), (m * m') • a' = m • m' • a')

@[simp]

theorem AddAction.orbit.coe_vadd {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] {a : α} {m : M} {a' : ↑(AddAction.orbit M a)} : ↑(m +ᵥ a') = m +ᵥ ↑a'

@[simp]

theorem MulAction.orbit.coe_smul {M : Type u} {α : Type v} [Monoid M] [MulAction M α] {a : α} {m : M} {a' : ↑(MulAction.orbit M a)} : ↑(m • a') = m • ↑a'

def AddAction.fixedPoints (M : Type u) (α : Type v) [AddMonoid M] [AddAction M α] : Set α

The set of elements fixed under the whole action.

Equations

• AddAction.fixedPoints M α = {a | ∀ (m : M), m +ᵥ a = a}

def MulAction.fixedPoints (M : Type u) (α : Type v) [Monoid M] [MulAction M α] : Set α

The set of elements fixed under the whole action.

Equations

• MulAction.fixedPoints M α = {a | ∀ (m : M), m • a = a}

def AddAction.fixedBy (M : Type u) (α : Type v) [AddMonoid M] [AddAction M α] (m : M) : Set α

fixedBy m is the set of elements fixed by m.

Equations

• AddAction.fixedBy M α m = {x | m +ᵥ x = x}

def MulAction.fixedBy (M : Type u) (α : Type v) [Monoid M] [MulAction M α] (m : M) : Set α

fixedBy m is the set of elements fixed by m.

Equations

• MulAction.fixedBy M α m = {x | m • x = x}

theorem AddAction.fixed_eq_iInter_fixedBy (M : Type u) (α : Type v) [AddMonoid M] [AddAction M α] : AddAction.fixedPoints M α = ⋂ (m : M), AddAction.fixedBy M α m

theorem MulAction.fixed_eq_iInter_fixedBy (M : Type u) (α : Type v) [Monoid M] [MulAction M α] : MulAction.fixedPoints M α = ⋂ (m : M), MulAction.fixedBy M α m

@[simp]

theorem AddAction.mem_fixedPoints {M : Type u} (α : Type v) [AddMonoid M] [AddAction M α] {a : α} : a ∈ AddAction.fixedPoints M α ↔ ∀ (m : M), m +ᵥ a = a

@[simp]

theorem MulAction.mem_fixedPoints {M : Type u} (α : Type v) [Monoid M] [MulAction M α] {a : α} : a ∈ MulAction.fixedPoints M α ↔ ∀ (m : M), m • a = a

@[simp]

theorem AddAction.mem_fixedBy {M : Type u} (α : Type v) [AddMonoid M] [AddAction M α] {m : M} {a : α} : a ∈ AddAction.fixedBy M α m ↔ m +ᵥ a = a

@[simp]

theorem MulAction.mem_fixedBy {M : Type u} (α : Type v) [Monoid M] [MulAction M α] {m : M} {a : α} : a ∈ MulAction.fixedBy M α m ↔ m • a = a

theorem AddAction.mem_fixedPoints' {M : Type u} (α : Type v) [AddMonoid M] [AddAction M α] {a : α} : a ∈ AddAction.fixedPoints M α ↔ ∀ (a' : α), a' ∈ AddAction.orbit M a → a' = a

abbrev AddAction.mem_fixedPoints'.match_1 {M : Type u_1} (α : Type u_2) [AddMonoid M] [AddAction M α] {a : α} : (x : α) → (motive : (∃ x_1, x_1 +ᵥ a = x) → Prop) → ∀ (x_1 : ∃ x_1, x_1 +ᵥ a = x), (∀ (m : M) (hm : m +ᵥ a = x), motive (_ : ∃ x_2, x_2 +ᵥ a = x)) → motive x_1

Equations

• AddAction.mem_fixedPoints'.match_1 α x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem MulAction.mem_fixedPoints' {M : Type u} (α : Type v) [Monoid M] [MulAction M α] {a : α} : a ∈ MulAction.fixedPoints M α ↔ ∀ (a' : α), a' ∈ MulAction.orbit M a → a' = a

def AddAction.Stabilizer.addSubmonoid (M : Type u) {α : Type v} [AddMonoid M] [AddAction M α] (a : α) : AddSubmonoid M

The stabilizer of m point a as an additive submonoid of M.

Equations

• One or more equations did not get rendered due to their size.

theorem AddAction.Stabilizer.addSubmonoid.proof_1 (M : Type u_2) {α : Type u_1} [AddMonoid M] [AddAction M α] (a : α) {m : M} {m' : M} (ha : m +ᵥ a = a) (hb : m' +ᵥ a = a) : m + m' +ᵥ a = a

def MulAction.Stabilizer.submonoid (M : Type u) {α : Type v} [Monoid M] [MulAction M α] (a : α) : Submonoid M

The stabilizer of a point a as a submonoid of M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddAction.mem_stabilizer_addSubmonoid_iff (M : Type u) {α : Type v} [AddMonoid M] [AddAction M α] {a : α} {m : M} : m ∈ AddAction.Stabilizer.addSubmonoid M a ↔ m +ᵥ a = a

@[simp]

theorem MulAction.mem_stabilizer_submonoid_iff (M : Type u) {α : Type v} [Monoid M] [MulAction M α] {a : α} {m : M} : m ∈ MulAction.Stabilizer.submonoid M a ↔ m • a = a

theorem AddAction.orbit_eq_univ (M : Type u) {α : Type v} [AddMonoid M] [AddAction M α] [AddAction.IsPretransitive M α] (a : α) : AddAction.orbit M a = Set.univ

theorem MulAction.orbit_eq_univ (M : Type u) {α : Type v} [Monoid M] [MulAction M α] [MulAction.IsPretransitive M α] (a : α) : MulAction.orbit M a = Set.univ

abbrev AddAction.mem_fixedPoints_iff_card_orbit_eq_one.match_1 {M : Type u_2} {α : Type u_1} [AddMonoid M] [AddAction M α] {a : α} (motive : ↑(AddAction.orbit M a) → Prop) : (x : ↑(AddAction.orbit M a)) → ((a : α) → (x : M) → (hx : (fun m => m +ᵥ a) x = a) → motive { val := a, property := (_ : ∃ y, (fun m => m +ᵥ a) y = a) }) → motive x

Equations

• AddAction.mem_fixedPoints_iff_card_orbit_eq_one.match_1 motive x h_1 = Subtype.casesOn x fun val property => Exists.casesOn property fun w h => h_1 val w h

theorem AddAction.mem_fixedPoints_iff_card_orbit_eq_one {M : Type u} {α : Type v} [AddMonoid M] [AddAction M α] {a : α} [Fintype ↑(AddAction.orbit M a)] : a ∈ AddAction.fixedPoints M α ↔ Fintype.card ↑(AddAction.orbit M a) = 1

theorem MulAction.mem_fixedPoints_iff_card_orbit_eq_one {M : Type u} {α : Type v} [Monoid M] [MulAction M α] {a : α} [Fintype ↑(MulAction.orbit M a)] : a ∈ MulAction.fixedPoints M α ↔ Fintype.card ↑(MulAction.orbit M a) = 1

theorem AddAction.stabilizer.proof_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] (a : α) : 0 ∈ (AddAction.Stabilizer.addSubmonoid G a).toAddSubsemigroup.carrier

def AddAction.stabilizer (G : Type u) {α : Type v} [AddGroup G] [AddAction G α] (a : α) : AddSubgroup G

The stabilizer of an element under an action, i.e. what sends the element to itself. An additive subgroup.

Equations

• One or more equations did not get rendered due to their size.

theorem AddAction.stabilizer.proof_2 (G : Type u_2) {α : Type u_1} [AddGroup G] [AddAction G α] (a : α) {m : G} (ha : m +ᵥ a = a) : -m +ᵥ a = a

def MulAction.stabilizer (G : Type u) {α : Type v} [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

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddAction.mem_stabilizer_iff {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] {g : G} {a : α} : g ∈ AddAction.stabilizer G a ↔ g +ᵥ a = a

@[simp]

theorem MulAction.mem_stabilizer_iff {G : Type u} {α : Type v} [Group G] [MulAction G α] {g : G} {a : α} : g ∈ MulAction.stabilizer G a ↔ g • a = a

@[simp]

theorem AddAction.vadd_orbit {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] (g : G) (a : α) : g +ᵥ AddAction.orbit G a = AddAction.orbit G a

@[simp]

theorem MulAction.smul_orbit {G : Type u} {α : Type v} [Group G] [MulAction G α] (g : G) (a : α) : g • MulAction.orbit G a = MulAction.orbit G a

@[simp]

theorem AddAction.orbit_vadd {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] (g : G) (a : α) : AddAction.orbit G (g +ᵥ a) = AddAction.orbit G a

@[simp]

theorem MulAction.orbit_smul {G : Type u} {α : Type v} [Group G] [MulAction G α] (g : G) (a : α) : MulAction.orbit G (g • a) = MulAction.orbit G a

instance AddAction.instIsPretransitiveElemOrbitToAddMonoidToSubNegAddMonoidToVAddInstAddActionElemOrbit {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] (a : α) : AddAction.IsPretransitive G ↑(AddAction.orbit G a)

The action of an additive group on an orbit is transitive.

Equations

• One or more equations did not get rendered due to their size.

theorem AddAction.instIsPretransitiveElemOrbitToAddMonoidToSubNegAddMonoidToVAddInstAddActionElemOrbit.proof_1 {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (a : α) : AddAction.IsPretransitive G ↑(AddAction.orbit G a)

instance MulAction.instIsPretransitiveElemOrbitToMonoidToDivInvMonoidToSMulInstMulActionElemOrbit {G : Type u} {α : Type v} [Group G] [MulAction G α] (a : α) : MulAction.IsPretransitive G ↑(MulAction.orbit G a)

The action of a group on an orbit is transitive.

Equations

• @MulAction.instIsPretransitiveElemOrbitToMonoidToDivInvMonoidToSMulInstMulActionElemOrbit = @MulAction.instIsPretransitiveElemOrbitToMonoidToDivInvMonoidToSMulInstMulActionElemOrbit.proof_1

abbrev AddAction.orbit_eq_iff.match_1 {G : Type u_2} {α : Type u_1} [AddGroup G] [AddAction G α] {a : α} {b : α} (motive : a ∈ AddAction.orbit G b → Prop) : (x : a ∈ AddAction.orbit G b) → ((w : G) → (hc : (fun m => m +ᵥ b) w = a) → motive (_ : ∃ y, (fun m => m +ᵥ b) y = a)) → motive x

Equations

• AddAction.orbit_eq_iff.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem AddAction.orbit_eq_iff {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] {a : α} {b : α} : AddAction.orbit G a = AddAction.orbit G b ↔ a ∈ AddAction.orbit G b

theorem MulAction.orbit_eq_iff {G : Type u} {α : Type v} [Group G] [MulAction G α] {a : α} {b : α} : MulAction.orbit G a = MulAction.orbit G b ↔ a ∈ MulAction.orbit G b

theorem AddAction.mem_orbit_vadd (G : Type u) {α : Type v} [AddGroup G] [AddAction G α] (g : G) (a : α) : a ∈ AddAction.orbit G (g +ᵥ a)

theorem MulAction.mem_orbit_smul (G : Type u) {α : Type v} [Group G] [MulAction G α] (g : G) (a : α) : a ∈ MulAction.orbit G (g • a)

theorem AddAction.vadd_mem_orbit_vadd (G : Type u) {α : Type v} [AddGroup G] [AddAction G α] (g : G) (h : G) (a : α) : g +ᵥ a ∈ AddAction.orbit G (h +ᵥ a)

theorem MulAction.smul_mem_orbit_smul (G : Type u) {α : Type v} [Group G] [MulAction G α] (g : G) (h : G) (a : α) : g • a ∈ MulAction.orbit G (h • a)

def AddAction.orbitRel (G : Type u) (α : Type v) [AddGroup G] [AddAction G α] : Setoid α

The relation 'in the same orbit'.

Equations

• AddAction.orbitRel G α = { r := fun a b => a ∈ AddAction.orbit G b, iseqv := (_ : Equivalence fun a b => a ∈ AddAction.orbit G b) }

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

def MulAction.orbitRel (G : Type u) (α : Type v) [Group G] [MulAction G α] : Setoid α

The relation 'in the same orbit'.

Equations

• MulAction.orbitRel G α = { r := fun a b => a ∈ MulAction.orbit G b, iseqv := (_ : Equivalence fun a b => a ∈ MulAction.orbit G b) }

theorem AddAction.orbitRel_apply {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] {a : α} {b : α} : Setoid.Rel (AddAction.orbitRel G α) a b ↔ a ∈ AddAction.orbit G b

theorem MulAction.orbitRel_apply {G : Type u} {α : Type v} [Group G] [MulAction G α] {a : α} {b : α} : Setoid.Rel (MulAction.orbitRel G α) a b ↔ a ∈ MulAction.orbit G b

theorem AddAction.quotient_preimage_image_eq_union_add {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] (U : Set α) : Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun x x_1 => x +ᵥ x_1) g '' U

When you take a set U in α, push it down to the quotient, and pull back, you get the union of the orbit of U under G.

theorem MulAction.quotient_preimage_image_eq_union_mul {G : Type u} {α : Type v} [Group G] [MulAction G α] (U : Set α) : Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ (g : G), (fun x x_1 => x • x_1) g '' U

When you take a set U in α, push it down to the quotient, and pull back, you get the union of the orbit of U under G.

theorem AddAction.disjoint_image_image_iff {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] {U : Set α} {V : Set α} : Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g +ᵥ x ∈ V

theorem MulAction.disjoint_image_image_iff {G : Type u} {α : Type v} [Group G] [MulAction G α] {U : Set α} {V : Set α} : Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V

theorem AddAction.image_inter_image_iff {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] (U : Set α) (V : Set α) : Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g +ᵥ x ∈ V

theorem MulAction.image_inter_image_iff {G : Type u} {α : Type v} [Group G] [MulAction G α] (U : Set α) (V : Set α) : Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ (x : α), x ∈ U → ∀ (g : G), ¬g • x ∈ V

@[reducible]

def AddAction.orbitRel.Quotient (G : Type u) (α : Type v) [AddGroup G] [AddAction G α] : Type v

The quotient by AddAction.orbitRel, given a name to enable dot notation.

Equations

• AddAction.orbitRel.Quotient G α = Quotient (AddAction.orbitRel G α)

@[reducible]

def MulAction.orbitRel.Quotient (G : Type u) (α : Type v) [Group G] [MulAction G α] : Type v

The quotient by MulAction.orbitRel, given a name to enable dot notation.

Equations

• MulAction.orbitRel.Quotient G α = Quotient (MulAction.orbitRel G α)

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} {α : Type v} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) : Set α

The orbit corresponding to an element of the quotient by AddAction.orbitRel

Equations

• AddAction.orbitRel.Quotient.orbit x = Quotient.liftOn' x (AddAction.orbit G) (_ : ∀ (x x_1 : α), x ∈ AddAction.orbit G x_1 → AddAction.orbit G x = AddAction.orbit G x_1)

def MulAction.orbitRel.Quotient.orbit {G : Type u} {α : Type v} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) : Set α

The orbit corresponding to an element of the quotient by MulAction.orbitRel

Equations

• MulAction.orbitRel.Quotient.orbit x = Quotient.liftOn' x (MulAction.orbit G) (_ : ∀ (x x_1 : α), x ∈ MulAction.orbit G x_1 → MulAction.orbit G x = MulAction.orbit G x_1)

@[simp]

theorem AddAction.orbitRel.Quotient.orbit_mk {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] (a : α) : AddAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = AddAction.orbit G a

@[simp]

theorem MulAction.orbitRel.Quotient.orbit_mk {G : Type u} {α : Type v} [Group G] [MulAction G α] (a : α) : MulAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = MulAction.orbit G a

theorem AddAction.orbitRel.Quotient.mem_orbit {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] {a : α} {x : AddAction.orbitRel.Quotient G α} : a ∈ AddAction.orbitRel.Quotient.orbit x ↔ Quotient.mk'' a = x

theorem MulAction.orbitRel.Quotient.mem_orbit {G : Type u} {α : Type v} [Group G] [MulAction G α] {a : α} {x : MulAction.orbitRel.Quotient G α} : a ∈ MulAction.orbitRel.Quotient.orbit x ↔ Quotient.mk'' a = x

theorem AddAction.orbitRel.Quotient.orbit_eq_orbit_out {G : Type u} {α : Type v} [AddGroup G] [AddAction G α] (x : AddAction.orbitRel.Quotient G α) {φ : AddAction.orbitRel.Quotient G α → α} (hφ : Function.RightInverse φ Quotient.mk') : AddAction.orbitRel.Quotient.orbit x = AddAction.orbit G (φ x)

Note that hφ = quotient.out_eq' is m useful choice here.

theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out {G : Type u} {α : Type v} [Group G] [MulAction G α] (x : MulAction.orbitRel.Quotient G α) {φ : MulAction.orbitRel.Quotient G α → α} (hφ : Function.RightInverse φ Quotient.mk') : MulAction.orbitRel.Quotient.orbit x = MulAction.orbit G (φ x)

Note that hφ = Quotient.out_eq' is a useful choice here.

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 ∈ AddAction.orbitRel.Quotient.orbit x

def AddAction.selfEquivSigmaOrbits' (G : Type u) (α : Type v) [AddGroup G] [AddAction G α] : α ≃ (ω : AddAction.orbitRel.Quotient G α) × ↑(AddAction.orbitRel.Quotient.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

• One or more equations did not get rendered due to their size.

def MulAction.selfEquivSigmaOrbits' (G : Type u) (α : Type v) [Group G] [MulAction G α] : α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑(MulAction.orbitRel.Quotient.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

• One or more equations did not get rendered due to their size.

theorem AddAction.selfEquivSigmaOrbits.proof_1 (G : Type u_2) (α : Type u_1) [AddGroup G] [AddAction G α] : ∀ (x : AddAction.orbitRel.Quotient G α), AddAction.orbitRel.Quotient.orbit x = AddAction.orbit G (Quotient.out' x)

def AddAction.selfEquivSigmaOrbits (G : Type u) (α : Type v) [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

• One or more equations did not get rendered due to their size.

def MulAction.selfEquivSigmaOrbits (G : Type u) (α : Type v) [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

• One or more equations did not get rendered due to their size.

theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj {G : Type u} {α : Type v} [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} {α : Type v} [Group G] [MulAction G α] {a : α} {b : α} (h : Setoid.Rel (MulAction.orbitRel G α) a b) : { x // x ∈ MulAction.stabilizer G a } ≃* { x // x ∈ MulAction.stabilizer G b }

A bijection between the stabilizers of two elements in the same orbit.

Equations

• One or more equations did not get rendered due to their size.

theorem AddAction.stabilizer_vadd_eq_stabilizer_map_conj (G : Type u) (α : Type v) [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) (α : Type v) [AddGroup G] [AddAction G α] {a : α} {b : α} (h : Setoid.Rel (AddAction.orbitRel G α) a b) : { x // x ∈ AddAction.stabilizer G a } ≃+ { x // x ∈ AddAction.stabilizer G b }

A bijection between the stabilizers of two elements in the same orbit.

Equations

• One or more equations did not get rendered due to their size.

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.