Properties of group actions involving quotient groups

This file proves properties of group actions which use the quotient group construction, notably

• the orbit-stabilizer theorem card_orbit_mul_card_stabilizer_eq_card_group
• the class formula card_eq_sum_card_group_div_card_stabilizer'
• Burnside's lemma sum_card_fixedBy_eq_card_orbits_mul_card_group

class MulAction.QuotientAction {α : Type u} (β : Type v) [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) : Prop

A typeclass for when a MulAction β α descends to the quotient α ⧸ H.

• inv_mul_mem : ∀ (b : β) {a a' : α}, a⁻¹ * a' ∈ H → (b • a)⁻¹ * b • a' ∈ H

  The action fulfils a normality condition on products that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

theorem MulAction.QuotientAction.inv_mul_mem {α : Type u} {β : Type v} : ∀ {inst : Group α} {inst_1 : Monoid β} {inst_2 : MulAction β α} {H : Subgroup α} [self : MulAction.QuotientAction β H] (b : β) {a a' : α}, a⁻¹ * a' ∈ H → (b • a)⁻¹ * b • a' ∈ H

The action fulfils a normality condition on products that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

class AddAction.QuotientAction {α : Type u} (β : Type v) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) : Prop

A typeclass for when an AddAction β α descends to the quotient α ⧸ H.

• inv_mul_mem : ∀ (b : β) {a a' : α}, -a + a' ∈ H → -(b +ᵥ a) + (b +ᵥ a') ∈ H

  The action fulfils a normality condition on summands that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

theorem AddAction.QuotientAction.inv_mul_mem {α : Type u} {β : Type v} : ∀ {inst : AddGroup α} {inst_1 : AddMonoid β} {inst_2 : AddAction β α} {H : AddSubgroup α} [self : AddAction.QuotientAction β H] (b : β) {a a' : α}, -a + a' ∈ H → -(b +ᵥ a) + (b +ᵥ a') ∈ H

The action fulfils a normality condition on summands that lie in H. This ensures that the action descends to an action on the quotient α ⧸ H.

instance AddAction.left_quotientAction {α : Type u} [AddGroup α] (H : AddSubgroup α) : AddAction.QuotientAction α H

Equations

• ⋯ = ⋯

instance MulAction.left_quotientAction {α : Type u} [Group α] (H : Subgroup α) : MulAction.QuotientAction α H

Equations

• ⋯ = ⋯

instance AddAction.right_quotientAction {α : Type u} [AddGroup α] (H : AddSubgroup α) : AddAction.QuotientAction (↥H.normalizer.op) H

Equations

• ⋯ = ⋯

instance MulAction.right_quotientAction {α : Type u} [Group α] (H : Subgroup α) : MulAction.QuotientAction (↥H.normalizer.op) H

Equations

• ⋯ = ⋯

instance AddAction.right_quotientAction' {α : Type u} [AddGroup α] (H : AddSubgroup α) [hH : H.Normal] : AddAction.QuotientAction αᵃᵒᵖ H

Equations

• ⋯ = ⋯

instance MulAction.right_quotientAction' {α : Type u} [Group α] (H : Subgroup α) [hH : H.Normal] : MulAction.QuotientAction αᵐᵒᵖ H

Equations

• ⋯ = ⋯

theorem AddAction.quotient.proof_2 {α : Type u_1} (β : Type u_2) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (q : α ⧸ H) : 0 +ᵥ q = q

theorem AddAction.quotient.proof_3 {α : Type u_1} (β : Type u_2) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (b' : β) (q : α ⧸ H) : b + b' +ᵥ q = b +ᵥ (b' +ᵥ q)

instance AddAction.quotient {α : Type u} (β : Type v) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] : AddAction β (α ⧸ H)

Equations

• AddAction.quotient β H = AddAction.mk ⋯ ⋯

theorem AddAction.quotient.proof_1 {α : Type u_1} (β : Type u_2) [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) : ∀ (x x_1 : α), Setoid.r x x_1 → Setoid.r ((fun (x : α) => b +ᵥ x) x) ((fun (x : α) => b +ᵥ x) x_1)

instance MulAction.quotient {α : Type u} (β : Type v) [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] : MulAction β (α ⧸ H)

Equations

• MulAction.quotient β H = MulAction.mk ⋯ ⋯

@[simp]

theorem AddAction.Quotient.vadd_mk {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (a : α) : b +ᵥ ↑a = ↑(b +ᵥ a)

@[simp]

theorem MulAction.Quotient.smul_mk {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] (b : β) (a : α) : b • ↑a = ↑(b • a)

@[simp]

theorem AddAction.Quotient.vadd_coe {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (a : α) : b +ᵥ ↑a = ↑(b +ᵥ a)

@[simp]

theorem MulAction.Quotient.smul_coe {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] (b : β) (a : α) : b • ↑a = ↑(b • a)

@[simp]

theorem AddAction.Quotient.mk_vadd_out' {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b +ᵥ Quotient.out' q) = b +ᵥ q

@[simp]

theorem MulAction.Quotient.mk_smul_out' {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b • Quotient.out' q) = b • q

theorem AddAction.Quotient.coe_vadd_out' {α : Type u} {β : Type v} [AddGroup α] [AddMonoid β] [AddAction β α] (H : AddSubgroup α) [AddAction.QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b +ᵥ Quotient.out' q) = b +ᵥ q

theorem MulAction.Quotient.coe_smul_out' {α : Type u} {β : Type v} [Group α] [Monoid β] [MulAction β α] (H : Subgroup α) [MulAction.QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b • Quotient.out' q) = b • q

theorem QuotientGroup.out'_conj_pow_minimalPeriod_mem {α : Type u} [Group α] (H : Subgroup α) (a : α) (q : α ⧸ H) : (Quotient.out' q)⁻¹ * a ^ Function.minimalPeriod (fun (x : α ⧸ H) => a • x) q * Quotient.out' q ∈ H

def MulActionHom.toQuotient {α : Type u} [Group α] (H : Subgroup α) : α →ₑ[id] α ⧸ H

The canonical map to the left cosets.

Equations

• MulActionHom.toQuotient H = { toFun := QuotientGroup.mk, map_smul' := ⋯ }

@[simp]

theorem MulActionHom.toQuotient_apply {α : Type u} [Group α] (H : Subgroup α) (g : α) : (MulActionHom.toQuotient H) g = ↑g

instance AddAction.addLeftCosetsCompSubtypeVal {α : Type u} [AddGroup α] (H : AddSubgroup α) (I : AddSubgroup α) : AddAction (↥I) (α ⧸ H)

Equations

• AddAction.addLeftCosetsCompSubtypeVal H I = AddAction.compHom (α ⧸ H) I.subtype

instance MulAction.mulLeftCosetsCompSubtypeVal {α : Type u} [Group α] (H : Subgroup α) (I : Subgroup α) : MulAction (↥I) (α ⧸ H)

Equations

• MulAction.mulLeftCosetsCompSubtypeVal H I = MulAction.compHom (α ⧸ H) I.subtype

def AddAction.ofQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α ⧸ AddAction.stabilizer α x) : β

The canonical map from the quotient of the stabilizer to the set.

Equations

• AddAction.ofQuotientStabilizer α x g = Quotient.liftOn' g (fun (x_1 : α) => x_1 +ᵥ x) ⋯

theorem AddAction.ofQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [AddGroup α] [AddAction α β] (x : β) (g1 : α) (g2 : α) (H : Setoid.r g1 g2) : g1 +ᵥ x = g2 +ᵥ x

def MulAction.ofQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α ⧸ MulAction.stabilizer α x) : β

The canonical map from the quotient of the stabilizer to the set.

Equations

• MulAction.ofQuotientStabilizer α x g = Quotient.liftOn' g (fun (x_1 : α) => x_1 • x) ⋯

@[simp]

theorem AddAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α) : AddAction.ofQuotientStabilizer α x ↑g = g +ᵥ x

@[simp]

theorem MulAction.ofQuotientStabilizer_mk (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α) : MulAction.ofQuotientStabilizer α x ↑g = g • x

theorem AddAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α ⧸ AddAction.stabilizer α x) : AddAction.ofQuotientStabilizer α x g ∈ AddAction.orbit α x

theorem MulAction.ofQuotientStabilizer_mem_orbit (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α ⧸ MulAction.stabilizer α x) : MulAction.ofQuotientStabilizer α x g ∈ MulAction.orbit α x

theorem AddAction.ofQuotientStabilizer_vadd (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) (g : α) (g' : α ⧸ AddAction.stabilizer α x) : AddAction.ofQuotientStabilizer α x (g +ᵥ g') = g +ᵥ AddAction.ofQuotientStabilizer α x g'

theorem MulAction.ofQuotientStabilizer_smul (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) (g : α) (g' : α ⧸ MulAction.stabilizer α x) : MulAction.ofQuotientStabilizer α x (g • g') = g • MulAction.ofQuotientStabilizer α x g'

theorem AddAction.injective_ofQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (x : β) : Function.Injective (AddAction.ofQuotientStabilizer α x)

theorem MulAction.injective_ofQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (x : β) : Function.Injective (MulAction.ofQuotientStabilizer α x)

noncomputable def AddAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) : ↑(AddAction.orbit α b) ≃ α ⧸ AddAction.stabilizer α b

Orbit-stabilizer theorem.

Equations

• AddAction.orbitEquivQuotientStabilizer α b = (Equiv.ofBijective (fun (g : α ⧸ AddAction.stabilizer α b) => ⟨AddAction.ofQuotientStabilizer α b g, ⋯⟩) ⋯).symm

theorem AddAction.orbitEquivQuotientStabilizer.proof_1 (α : Type u_1) {β : Type u_2} [AddGroup α] [AddAction α β] (b : β) : (Function.Injective fun (g : α ⧸ AddAction.stabilizer α b) => ⟨AddAction.ofQuotientStabilizer α b g, ⋯⟩) ∧ Function.Surjective fun (g : α ⧸ AddAction.stabilizer α b) => ⟨AddAction.ofQuotientStabilizer α b g, ⋯⟩

noncomputable def MulAction.orbitEquivQuotientStabilizer (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) : ↑(MulAction.orbit α b) ≃ α ⧸ MulAction.stabilizer α b

Orbit-stabilizer theorem.

Equations

• MulAction.orbitEquivQuotientStabilizer α b = (Equiv.ofBijective (fun (g : α ⧸ MulAction.stabilizer α b) => ⟨MulAction.ofQuotientStabilizer α b g, ⋯⟩) ⋯).symm

noncomputable def AddAction.orbitProdStabilizerEquivAddGroup (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) : ↑(AddAction.orbit α b) × ↥(AddAction.stabilizer α b) ≃ α

Orbit-stabilizer theorem.

Equations

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

noncomputable def MulAction.orbitProdStabilizerEquivGroup (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) : ↑(MulAction.orbit α b) × ↥(MulAction.stabilizer α b) ≃ α

Orbit-stabilizer theorem.

Equations

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

theorem AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) [Fintype α] [Fintype ↑(AddAction.orbit α b)] [Fintype ↥(AddAction.stabilizer α b)] : Fintype.card ↑(AddAction.orbit α b) * Fintype.card ↥(AddAction.stabilizer α b) = Fintype.card α

Orbit-stabilizer theorem.

theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) [Fintype α] [Fintype ↑(MulAction.orbit α b)] [Fintype ↥(MulAction.stabilizer α b)] : Fintype.card ↑(MulAction.orbit α b) * Fintype.card ↥(MulAction.stabilizer α b) = Fintype.card α

Orbit-stabilizer theorem.

@[simp]

theorem AddAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [AddGroup α] [AddAction α β] (b : β) (a : α) : ↑((AddAction.orbitEquivQuotientStabilizer α b).symm ↑a) = a +ᵥ b

@[simp]

theorem MulAction.orbitEquivQuotientStabilizer_symm_apply (α : Type u) {β : Type v} [Group α] [MulAction α β] (b : β) (a : α) : ↑((MulAction.orbitEquivQuotientStabilizer α b).symm ↑a) = a • b

@[simp]

theorem AddAction.stabilizer_quotient {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : AddAction.stabilizer G ↑0 = H

@[simp]

theorem MulAction.stabilizer_quotient {G : Type u_1} [Group G] (H : Subgroup G) : MulAction.stabilizer G ↑1 = H

noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] {φ : Quotient (AddAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : β ≃ (ω : Quotient (AddAction.orbitRel α β)) × α ⧸ AddAction.stabilizer α (φ ω)

Class formula : given G an additive group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbit_rel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be Quotient.out', so we provide AddAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

Equations

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

noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer' (α : Type u) (β : Type v) [Group α] [MulAction α β] {φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : β ≃ (ω : Quotient (MulAction.orbitRel α β)) × α ⧸ MulAction.stabilizer α (φ ω)

Class formula : given G a group acting on X and φ a function mapping each orbit of X under this action (that is, each element of the quotient of X by the relation orbitRel G X) to an element in this orbit, this gives a (noncomputable) bijection between X and the disjoint union of G/Stab(φ(ω)) over all orbits ω. In most cases you'll want φ to be Quotient.out', so we provide MulAction.selfEquivSigmaOrbitsQuotientStabilizer' as a special case.

Equations

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

theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer' (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (AddAction.orbitRel α β))] [(b : β) → Fintype ↥(AddAction.stabilizer α b)] {φ : Quotient (AddAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : Fintype.card β = ∑ ω : Quotient (AddAction.orbitRel α β), Fintype.card α / Fintype.card ↥(AddAction.stabilizer α (φ ω))

Class formula for a finite group acting on a finite type. See AddAction.card_eq_sum_card_addGroup_div_card_stabilizer for a specialized version using Quotient.out'.

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer' (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (MulAction.orbitRel α β))] [(b : β) → Fintype ↥(MulAction.stabilizer α b)] {φ : Quotient (MulAction.orbitRel α β) → β} (hφ : Function.LeftInverse Quotient.mk'' φ) : Fintype.card β = ∑ ω : Quotient (MulAction.orbitRel α β), Fintype.card α / Fintype.card ↥(MulAction.stabilizer α (φ ω))

Class formula for a finite group acting on a finite type. See MulAction.card_eq_sum_card_group_div_card_stabilizer for a specialized version using Quotient.out'.

noncomputable def AddAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] : β ≃ (ω : Quotient (AddAction.orbitRel α β)) × α ⧸ AddAction.stabilizer α ω.out'

Class formula. This is a special case of AddAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out'.

Equations

• AddAction.selfEquivSigmaOrbitsQuotientStabilizer α β = AddAction.selfEquivSigmaOrbitsQuotientStabilizer' α β ⋯

theorem AddAction.selfEquivSigmaOrbitsQuotientStabilizer.proof_1 (α : Type u_2) (β : Type u_1) [AddGroup α] [AddAction α β] (q : Quotient (AddAction.orbitRel α β)) : Quotient.mk'' q.out' = q

noncomputable def MulAction.selfEquivSigmaOrbitsQuotientStabilizer (α : Type u) (β : Type v) [Group α] [MulAction α β] : β ≃ (ω : Quotient (MulAction.orbitRel α β)) × α ⧸ MulAction.stabilizer α ω.out'

Class formula. This is a special case of MulAction.self_equiv_sigma_orbits_quotient_stabilizer' with φ = Quotient.out'.

Equations

• MulAction.selfEquivSigmaOrbitsQuotientStabilizer α β = MulAction.selfEquivSigmaOrbitsQuotientStabilizer' α β ⋯

theorem AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (AddAction.orbitRel α β))] [(b : β) → Fintype ↥(AddAction.stabilizer α b)] : Fintype.card β = ∑ ω : Quotient (AddAction.orbitRel α β), Fintype.card α / Fintype.card ↥(AddAction.stabilizer α ω.out')

Class formula for a finite group acting on a finite type.

theorem MulAction.card_eq_sum_card_group_div_card_stabilizer (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [Fintype β] [Fintype (Quotient (MulAction.orbitRel α β))] [(b : β) → Fintype ↥(MulAction.stabilizer α b)] : Fintype.card β = ∑ ω : Quotient (MulAction.orbitRel α β), Fintype.card α / Fintype.card ↥(MulAction.stabilizer α ω.out')

Class formula for a finite group acting on a finite type.

noncomputable def AddAction.sigmaFixedByEquivOrbitsProdAddGroup (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] : (a : α) × ↑(AddAction.fixedBy β a) ≃ Quotient (AddAction.orbitRel α β) × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is an additive group acting on X and X/Gdenotes the quotient of X by the relation orbitRel G X.

Equations

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

theorem AddAction.sigmaFixedByEquivOrbitsProdAddGroup.proof_1 (α : Type u_1) (β : Type u_2) [AddGroup α] [AddAction α β] : ∀ (x : α × β), x.1 +ᵥ x.2 = x.2 ↔ x.1 +ᵥ x.2 = x.2

noncomputable def MulAction.sigmaFixedByEquivOrbitsProdGroup (α : Type u) (β : Type v) [Group α] [MulAction α β] : (a : α) × ↑(MulAction.fixedBy β a) ≃ Quotient (MulAction.orbitRel α β) × α

Burnside's lemma : a (noncomputable) bijection between the disjoint union of all {x ∈ X | g • x = x} for g ∈ G and the product G × X/G, where G is a group acting on X and X/G denotes the quotient of X by the relation orbitRel G X.

Equations

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

theorem AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup (α : Type u) (β : Type v) [AddGroup α] [AddAction α β] [Fintype α] [(a : α) → Fintype ↑(AddAction.fixedBy β a)] [Fintype (Quotient (AddAction.orbitRel α β))] : ∑ a : α, Fintype.card ↑(AddAction.fixedBy β a) = Fintype.card (Quotient (AddAction.orbitRel α β)) * Fintype.card α

Burnside's lemma : given a finite additive group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

theorem MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group (α : Type u) (β : Type v) [Group α] [MulAction α β] [Fintype α] [(a : α) → Fintype ↑(MulAction.fixedBy β a)] [Fintype (Quotient (MulAction.orbitRel α β))] : ∑ a : α, Fintype.card ↑(MulAction.fixedBy β a) = Fintype.card (Quotient (MulAction.orbitRel α β)) * Fintype.card α

Burnside's lemma : given a finite group G acting on a set X, the average number of elements fixed by each g ∈ G is the number of orbits.

instance AddAction.isPretransitive_quotient (G : Type u_1) [AddGroup G] (H : AddSubgroup G) : AddAction.IsPretransitive G (G ⧸ H)

Equations

• ⋯ = ⋯

instance MulAction.isPretransitive_quotient (G : Type u_1) [Group G] (H : Subgroup G) : MulAction.IsPretransitive G (G ⧸ H)

Equations

• ⋯ = ⋯

instance AddAction.finite_quotient_of_pretransitive_of_finite_quotient {α : Type u} (β : Type v) [AddGroup α] [AddAction α β] [AddAction.IsPretransitive α β] {H : AddSubgroup α} [Finite (α ⧸ H)] : Finite (AddAction.orbitRel.Quotient (↥H) β)

Equations

• ⋯ = ⋯

instance MulAction.finite_quotient_of_pretransitive_of_finite_quotient {α : Type u} (β : Type v) [Group α] [MulAction α β] [MulAction.IsPretransitive α β] {H : Subgroup α} [Finite (α ⧸ H)] : Finite (MulAction.orbitRel.Quotient (↥H) β)

Equations

• ⋯ = ⋯

theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_4 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (H : AddSubgroup α) (ω : Quotient (AddAction.orbitRel α β)) (a : { x : β // x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω} }) (b : { x : β // x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω} }) (h : Setoid.r a b) : (fun (x : { x : β // x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω} }) => ⟦⟨↑x, ⋯⟩⟧) a = (fun (x : { x : β // x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω} }) => ⟦⟨↑x, ⋯⟩⟧) b

theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_1 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (ω : Quotient (AddAction.orbitRel α β)) (x : ↑(AddAction.orbitRel.Quotient.orbit ω)) : ↑x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω}

noncomputable def AddAction.equivAddSubgroupOrbitsSetoidComap {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (H : AddSubgroup α) (ω : Quotient (AddAction.orbitRel α β)) : AddAction.orbitRel.Quotient ↥H ↑(AddAction.orbitRel.Quotient.orbit ω) ≃ Quotient (Setoid.comap Subtype.val (AddAction.orbitRel (↥H) β))

A bijection between the quotient of the action of an additive subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

Equations

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

theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_3 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (ω : Quotient (AddAction.orbitRel α β)) (x : { x : β // x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω} }) : ↑x ∈ AddAction.orbitRel.Quotient.orbit ω

theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_5 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (H : AddSubgroup α) (ω : Quotient (AddAction.orbitRel α β)) : Function.LeftInverse (fun (q : Quotient (Setoid.comap Subtype.val (AddAction.orbitRel (↥H) β))) => q.liftOn' (fun (x : { x : β // x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω} }) => ⟦⟨↑x, ⋯⟩⟧) ⋯) fun (q : AddAction.orbitRel.Quotient ↥H ↑(AddAction.orbitRel.Quotient.orbit ω)) => Quotient.liftOn' q (fun (x : ↑(AddAction.orbitRel.Quotient.orbit ω)) => ⟦⟨↑x, ⋯⟩⟧) ⋯

theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_6 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (H : AddSubgroup α) (ω : Quotient (AddAction.orbitRel α β)) : Function.RightInverse (fun (q : Quotient (Setoid.comap Subtype.val (AddAction.orbitRel (↥H) β))) => q.liftOn' (fun (x : { x : β // x ∈ Quotient.mk (AddAction.orbitRel α β) ⁻¹' {ω} }) => ⟦⟨↑x, ⋯⟩⟧) ⋯) fun (q : AddAction.orbitRel.Quotient ↥H ↑(AddAction.orbitRel.Quotient.orbit ω)) => Quotient.liftOn' q (fun (x : ↑(AddAction.orbitRel.Quotient.orbit ω)) => ⟦⟨↑x, ⋯⟩⟧) ⋯

theorem AddAction.equivAddSubgroupOrbitsSetoidComap.proof_2 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (H : AddSubgroup α) (ω : Quotient (AddAction.orbitRel α β)) (a : ↑(AddAction.orbitRel.Quotient.orbit ω)) (b : ↑(AddAction.orbitRel.Quotient.orbit ω)) (h : Setoid.r a b) : (fun (x : ↑(AddAction.orbitRel.Quotient.orbit ω)) => ⟦⟨↑x, ⋯⟩⟧) a = (fun (x : ↑(AddAction.orbitRel.Quotient.orbit ω)) => ⟦⟨↑x, ⋯⟩⟧) b

noncomputable def MulAction.equivSubgroupOrbitsSetoidComap {α : Type u} {β : Type v} [Group α] [MulAction α β] (H : Subgroup α) (ω : Quotient (MulAction.orbitRel α β)) : MulAction.orbitRel.Quotient ↥H ↑(MulAction.orbitRel.Quotient.orbit ω) ≃ Quotient (Setoid.comap Subtype.val (MulAction.orbitRel (↥H) β))

A bijection between the quotient of the action of a subgroup H on an orbit, and a corresponding quotient expressed in terms of Setoid.comap Subtype.val.

Equations

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

noncomputable def AddAction.equivAddSubgroupOrbits {α : Type u} (β : Type v) [AddGroup α] [AddAction α β] (H : AddSubgroup α) : AddAction.orbitRel.Quotient (↥H) β ≃ (ω : Quotient (AddAction.orbitRel α β)) × AddAction.orbitRel.Quotient ↥H ↑(AddAction.orbitRel.Quotient.orbit ω)

A bijection between the orbits under the action of an additive subgroup H on β, and the orbits under the action of H on each orbit under the action of G.

Equations

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

noncomputable def MulAction.equivSubgroupOrbits {α : Type u} (β : Type v) [Group α] [MulAction α β] (H : Subgroup α) : MulAction.orbitRel.Quotient (↥H) β ≃ (ω : Quotient (MulAction.orbitRel α β)) × MulAction.orbitRel.Quotient ↥H ↑(MulAction.orbitRel.Quotient.orbit ω)

A bijection between the orbits under the action of a subgroup H on β, and the orbits under the action of H on each orbit under the action of G.

Equations

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

instance AddAction.finite_quotient_of_finite_quotient_of_finite_quotient {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] {H : AddSubgroup α} [Finite (AddAction.orbitRel.Quotient α β)] [Finite (α ⧸ H)] : Finite (AddAction.orbitRel.Quotient (↥H) β)

Equations

• ⋯ = ⋯

instance MulAction.finite_quotient_of_finite_quotient_of_finite_quotient {α : Type u} {β : Type v} [Group α] [MulAction α β] {H : Subgroup α} [Finite (MulAction.orbitRel.Quotient α β)] [Finite (α ⧸ H)] : Finite (MulAction.orbitRel.Quotient (↥H) β)

Equations

• ⋯ = ⋯

noncomputable def AddAction.equivAddSubgroupOrbitsQuotientAddGroup {α : Type u} {β : Type v} [AddGroup α] [AddAction α β] (x : β) [AddAction.IsPretransitive α β] (free : ∀ (y : β), AddAction.stabilizer α y = ⊥) (H : AddSubgroup α) : AddAction.orbitRel.Quotient (↥H) β ≃ α ⧸ H

Given an additive group acting freely and transitively, an equivalence between the orbits under the action of an additive subgroup and the quotient group.

Equations

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

theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_3 {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (x : β) (H : AddSubgroup α) (g₁ : α) (g₂ : α) (h : Setoid.r g₁ g₂) : (fun (g : α) => ⟦-g +ᵥ x⟧) g₁ = (fun (g : α) => ⟦-g +ᵥ x⟧) g₂

theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_4 {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (x : β) [AddAction.IsPretransitive α β] (free : ∀ (y : β), AddAction.stabilizer α y = ⊥) (H : AddSubgroup α) (y : AddAction.orbitRel.Quotient (↥H) β) : (fun (q : α ⧸ H) => Quotient.liftOn' q (fun (g : α) => ⟦-g +ᵥ x⟧) ⋯) ((fun (q : AddAction.orbitRel.Quotient (↥H) β) => Quotient.liftOn' q (fun (y : β) => ↑⋯.choose) ⋯) y) = y

theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_5 {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (x : β) [AddAction.IsPretransitive α β] (free : ∀ (y : β), AddAction.stabilizer α y = ⊥) (H : AddSubgroup α) (g : α ⧸ H) : (fun (q : AddAction.orbitRel.Quotient (↥H) β) => Quotient.liftOn' q (fun (y : β) => ↑⋯.choose) ⋯) ((fun (q : α ⧸ H) => Quotient.liftOn' q (fun (g : α) => ⟦-g +ᵥ x⟧) ⋯) g) = g

theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_2 {α : Type u_2} {β : Type u_1} [AddGroup α] [AddAction α β] (x : β) [AddAction.IsPretransitive α β] (free : ∀ (y : β), AddAction.stabilizer α y = ⊥) (H : AddSubgroup α) (y₁ : β) (y₂ : β) (h : Setoid.r y₁ y₂) : (fun (y : β) => ↑⋯.choose) y₁ = (fun (y : β) => ↑⋯.choose) y₂

theorem AddAction.equivAddSubgroupOrbitsQuotientAddGroup.proof_1 {α : Type u_1} {β : Type u_2} [AddGroup α] [AddAction α β] (x : β) [AddAction.IsPretransitive α β] (y : β) : ∃ (m : α), m +ᵥ y = x

noncomputable def MulAction.equivSubgroupOrbitsQuotientGroup {α : Type u} {β : Type v} [Group α] [MulAction α β] (x : β) [MulAction.IsPretransitive α β] (free : ∀ (y : β), MulAction.stabilizer α y = ⊥) (H : Subgroup α) : MulAction.orbitRel.Quotient (↥H) β ≃ α ⧸ H

Given a group acting freely and transitively, an equivalence between the orbits under the action of a subgroup and the quotient group.

Equations

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

theorem ConjClasses.card_carrier {G : Type u_1} [Group G] [Fintype G] (g : G) [Fintype ↑(ConjClasses.mk g).carrier] [Fintype ↥(MulAction.stabilizer (ConjAct G) g)] : Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

theorem Subgroup.normalCore_eq_ker {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker

noncomputable def Subgroup.quotientCentralizerEmbedding {G : Type u_1} [Group G] (g : G) : G ⧸ Subgroup.centralizer ↑(Subgroup.zpowers g) ↪ ↑(commutatorSet G)

Cosets of the centralizer of an element embed into the set of commutators.

Equations

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

theorem Subgroup.quotientCentralizerEmbedding_apply {G : Type u_1} [Group G] (g : G) (x : G) : (Subgroup.quotientCentralizerEmbedding g) ↑x = ⟨⁅x, g⁆, ⋯⟩

noncomputable def Subgroup.quotientCenterEmbedding {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ⊤) : G ⧸ Subgroup.center G ↪ ↑S → ↑(commutatorSet G)

If G is generated by S, then the quotient by the center embeds into S-indexed sequences of commutators.

Equations

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

theorem Subgroup.quotientCenterEmbedding_apply {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ⊤) (g : G) (s : ↑S) : (Subgroup.quotientCenterEmbedding hS) (↑g) s = ⟨⁅g, ↑s⁆, ⋯⟩