Generic orbit-relation quotient helpers

This file records small generic additions to Mathlib's MulAction.orbitRel.Quotient API.

Main declarations

• TauCeti.MulAction.orbitRelQuotientBotEquiv: the quotient by the trivial subgroup is the original space.
• TauCeti.MulAction.transversalEquivOrbitRelQuotient: a set meeting every orbit, such that a group element carrying one of its points into it fixes that point, is a set of orbit representatives.
• TauCeti.MulAction.card_orbitRelQuotient_eq_one: a pretransitive action on a nonempty type has exactly one orbit.
• TauCeti.MulAction.card_orbitRelQuotient_anti: enlarging the acting subgroup can only decrease the number of orbits.
• TauCeti.MulAction.orbitRelQuotientMapOfLE_bot_eq_iff: equality after the bottom-to-H quotient map is membership in an H-orbit.
• TauCeti.MulAction.orbitRelQuotient_smul_eq_smul_iff_mul_inv_mem: in a cancellative action, two translates have the same H-orbit class exactly when the translators differ on the right by an element of H; this holds for an arbitrary subgroup.
• TauCeti.MulAction.orbitRelQuotient_smul_eq_base_iff: in a cancellative action, a translate has the same H-orbit class as the base point exactly when the translator is in H.
• TauCeti.MulAction.orbitRelQuotient_smul_eq_smul_iff_normalizerQuotientMk_inv_eq: for a normal subgroup, equality of two translates in the H-orbit quotient is equality of the corresponding inverse representatives in N(H) / H.
• TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal: in a free transitive action, the quotient by a normal subgroup is the normalizer quotient N(H) / H.
• TauCeti.MulAction.normalizerOrbitRelQuotientPermHom: the normalizer action on the quotient by H-orbits.
• TauCeti.MulAction.normalizerQuotientOrbitRelQuotientPermHom: the descended action of N(H) / H on the quotient by H-orbits.
• TauCeti.MulAction.normalizerQuotientOrbitRelQuotientIsPretransitive: if the normalizer acts transitively, then the descended N(H) / H action on the H-orbit quotient is transitive.
• TauCeti.MulAction.normalizerQuotientOrbitRelQuotient_smul_eq_smul_iff: if the original action is free, then the descended N(H) / H action on the H-orbit quotient is free.
• TauCeti.MulAction.orbitRelQuotientCongr: an equivalence carrying one action to another along a group isomorphism induces an equivalence of orbit spaces.
• TauCeti.MulAction.stabilizer_sigma_mk: the stabilizer of a sigma point is its fibre stabilizer.
• TauCeti.MulAction.orbitRelQuotientSigmaEquiv: the orbit space of a componentwise sigma action is the sigma type of the fibre orbit spaces.
• TauCeti.MulAction.orbitRelQuotientSumEquiv: the orbit space of an action on X ⊕ Y is the sum of the orbit spaces of X and Y.
• TauCeti.MulAction.equivSubgroupOrbitsQuotientGroup_symm_mk and TauCeti.MulAction.equivSubgroupOrbitsQuotientGroup_mapOfLE: the representative convention of Mathlib's equivSubgroupOrbitsQuotientGroup and its naturality in subgroup inclusions.

noncomputable def TauCeti.MulAction.orbitRelQuotientBotEquiv {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] : MulAction.orbitRel.Quotient (↥⊥) X ≃ X

Quotienting a group action by the trivial subgroup gives back the original space.

Equations

• TauCeti.MulAction.orbitRelQuotientBotEquiv = { toFun := Quotient.lift (fun (x : X) => x) ⋯, invFun := Quotient.mk'', left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientBotEquiv_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (x : X) : orbitRelQuotientBotEquiv (Quotient.mk'' x) = x

The bottom-subgroup quotient equivalence sends a class to its representative.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientBotEquiv_symm_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (x : X) : orbitRelQuotientBotEquiv.symm x = Quotient.mk'' x

The inverse bottom-subgroup quotient equivalence sends a point to its quotient class.

noncomputable def TauCeti.MulAction.transversalEquivOrbitRelQuotient {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {s : Set X} (hex : ∀ (x : X), ∃ (g : G), g • x ∈ s) (hfix : ∀ x ∈ s, ∀ (g : G), g • x ∈ s → g • x = x) : ↑s ≃ MulAction.orbitRel.Quotient G X

A set s meeting every orbit, such that a group element carrying a point of s into s fixes that point, is a set of orbit representatives: sending a point of s to its orbit is a bijection onto the orbit space.

Equations

• TauCeti.MulAction.transversalEquivOrbitRelQuotient hex hfix = Equiv.ofBijective (fun (x : ↑s) => Quotient.mk'' ↑x) ⋯

@[simp]

theorem TauCeti.MulAction.transversalEquivOrbitRelQuotient_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {s : Set X} (hex : ∀ (x : X), ∃ (g : G), g • x ∈ s) (hfix : ∀ x ∈ s, ∀ (g : G), g • x ∈ s → g • x = x) (x : ↑s) : (transversalEquivOrbitRelQuotient hex hfix) x = Quotient.mk'' ↑x

transversalEquivOrbitRelQuotient sends a point of s to its orbit.

@[simp]

theorem TauCeti.MulAction.transversalEquivOrbitRelQuotient_symm_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {s : Set X} (hex : ∀ (x : X), ∃ (g : G), g • x ∈ s) (hfix : ∀ x ∈ s, ∀ (g : G), g • x ∈ s → g • x = x) (x : ↑s) : (transversalEquivOrbitRelQuotient hex hfix).symm (Quotient.mk'' ↑x) = x

The inverse of transversalEquivOrbitRelQuotient sends the orbit of x ∈ s back to x.

theorem TauCeti.MulAction.transversalEquivOrbitRelQuotient_symm_mk_mem_orbit {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {s : Set X} (hex : ∀ (x : X), ∃ (g : G), g • x ∈ s) (hfix : ∀ x ∈ s, ∀ (g : G), g • x ∈ s → g • x = x) (x : X) : ↑((transversalEquivOrbitRelQuotient hex hfix).symm (Quotient.mk'' x)) ∈ MulAction.orbit G x

The inverse of transversalEquivOrbitRelQuotient picks the point of s in the given orbit.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientBot_mk_eq_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (x y : X) : Quotient.mk'' x = Quotient.mk'' y ↔ x = y

Equality of bottom-subgroup orbit classes is equality of representatives.

theorem TauCeti.MulAction.orbitRel_le_of_subgroup_le {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (hHK : H ≤ K) : MulAction.orbitRel (↥H) X ≤ MulAction.orbitRel (↥K) X

Orbit relations are monotone in the acting subgroup.

@[simp]

theorem TauCeti.MulAction.card_orbitRelQuotient_eq_one {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [Nonempty X] [MulAction.IsPretransitive G X] : Nat.card (MulAction.orbitRel.Quotient G X) = 1

A pretransitive action on a nonempty type has one orbit. This is Mathlib's MulAction.pretransitive_iff_unique_quotient_of_nonempty in counting form.

theorem TauCeti.MulAction.card_orbitRelQuotient_anti {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H K : Subgroup G} (hHK : H ≤ K) [Finite (MulAction.orbitRel.Quotient (↥H) X)] : Nat.card (MulAction.orbitRel.Quotient (↥K) X) ≤ Nat.card (MulAction.orbitRel.Quotient (↥H) X)

Enlarging the acting subgroup can only decrease the number of orbits.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientMapOfLE_bot_eq {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) : Setoid.map_of_le ⋯ = (fun (x : X) => Quotient.mk'' x) ∘ ⇑orbitRelQuotientBotEquiv

The map from the bottom-subgroup quotient to the H-quotient is the H-orbit class map under the bottom quotient equivalence.

theorem TauCeti.MulAction.orbitRelQuotientMapOfLE_bot_eq_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (x y : MulAction.orbitRel.Quotient (↥⊥) X) : Setoid.map_of_le ⋯ x = Setoid.map_of_le ⋯ y ↔ orbitRelQuotientBotEquiv x ∈ MulAction.orbit (↥H) (orbitRelQuotientBotEquiv y)

Equality in an H-orbit quotient can be checked after choosing representatives through the bottom-subgroup quotient.

theorem TauCeti.MulAction.orbitRelQuotient_smul_eq_smul_iff_mul_inv_mem {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] (H : Subgroup G) (x : X) (g k : G) : Quotient.mk'' (g • x) = Quotient.mk'' (k • x) ↔ g * k⁻¹ ∈ H

In a cancellative action, two translates have the same subgroup-orbit quotient class exactly when the translators differ on the right by an element of the subgroup. This holds for an arbitrary subgroup; the normal-subgroup criterion orbitRelQuotient_smul_eq_smul_iff_normalizerQuotientMk_inv_eq follows from it.

theorem TauCeti.MulAction.orbitRelQuotient_smul_eq_base_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] (H : Subgroup G) (g : G) (x : X) : Quotient.mk'' (g • x) = Quotient.mk'' x ↔ g ∈ H

In a cancellative action, a translate has the same subgroup-orbit quotient class as the base point exactly when the translating group element belongs to the subgroup.

theorem TauCeti.MulAction.orbitRelQuotient_smul_eq_smul_iff_normalizerQuotientMk_inv_eq {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] (H : Subgroup G) [H.Normal] (x : X) (g k : G) : Quotient.mk'' (g • x) = Quotient.mk'' (k • x) ↔ H.normalizerQuotientMk ⟨g⁻¹, ⋯⟩ = H.normalizerQuotientMk ⟨k⁻¹, ⋯⟩

In a cancellative action by G, equality of two translates in the quotient by a normal subgroup H is equality of the corresponding inverse representatives in the normalizer quotient N(H) / H.

@[simp]

theorem TauCeti.MulAction.equivSubgroupOrbitsQuotientGroup_symm_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) (x : X) (g : G) : (MulAction.equivSubgroupOrbitsQuotientGroup x H).symm ↑g = Quotient.mk'' (g⁻¹ • x)

Mathlib's subgroup-orbit quotient equivalence sends the coset of g back to the orbit class of g⁻¹ • x. This records the representative convention once, so later lemmas can rewrite through a named theorem rather than relying directly on definitional equality.

@[simp]

theorem TauCeti.MulAction.equivSubgroupOrbitsQuotientGroup_apply_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) (x : X) (g : G) : (MulAction.equivSubgroupOrbitsQuotientGroup x H) (Quotient.mk'' (g • x)) = ↑g⁻¹

The subgroup-orbit quotient equivalence sends the orbit class of g • x to the coset of g⁻¹.

@[simp]

theorem TauCeti.MulAction.equivSubgroupOrbitsQuotientGroup_mapOfLE {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] {H K : Subgroup G} (hHK : H ≤ K) (x₀ : X) (x : MulAction.orbitRel.Quotient (↥H) X) : Subgroup.quotientMapOfLE hHK ((MulAction.equivSubgroupOrbitsQuotientGroup x₀ H) x) = (MulAction.equivSubgroupOrbitsQuotientGroup x₀ K) (Setoid.map_of_le ⋯ x)

The subgroup-orbit quotient equivalence is natural in subgroup inclusions.

def TauCeti.MulAction.normalizerOrbitRelQuotientMap {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) : MulAction.orbitRel.Quotient (↥H) X → MulAction.orbitRel.Quotient (↥H) X

A normalizer representative acts on the quotient by H-orbits.

Equations

• TauCeti.MulAction.normalizerOrbitRelQuotientMap H g = Quotient.map' (fun (x : X) => ↑g • x) ⋯

@[simp]

theorem TauCeti.MulAction.normalizerOrbitRelQuotientMap_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (x : X) : normalizerOrbitRelQuotientMap H g (Quotient.mk'' x) = Quotient.mk'' (↑g • x)

The normalizer action on an orbit quotient sends a class to the class of its translate.

@[simp]

theorem TauCeti.MulAction.normalizerOrbitRelQuotientMap_one {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) : normalizerOrbitRelQuotientMap H ⟨1, ⋯⟩ = id

The normalizer representative 1 acts trivially on the orbit quotient.

@[simp]

theorem TauCeti.MulAction.normalizerOrbitRelQuotientMap_mul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g k : ↥(Subgroup.normalizer ↑H)) : normalizerOrbitRelQuotientMap H (g * k) = normalizerOrbitRelQuotientMap H g ∘ normalizerOrbitRelQuotientMap H k

Normalizer representatives act by composition on the orbit quotient.

def TauCeti.MulAction.normalizerOrbitRelQuotientEquiv {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) : Equiv.Perm (MulAction.orbitRel.Quotient (↥H) X)

A normalizer representative acts on the orbit quotient by a permutation.

Equations

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

@[simp]

theorem TauCeti.MulAction.normalizerOrbitRelQuotientEquiv_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (x : X) : (normalizerOrbitRelQuotientEquiv H g) (Quotient.mk'' x) = Quotient.mk'' (↑g • x)

A normalizer representative permutes orbit classes by translating representatives.

@[simp]

theorem TauCeti.MulAction.normalizerOrbitRelQuotientEquiv_symm_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (x : X) : (Equiv.symm (normalizerOrbitRelQuotientEquiv H g)) (Quotient.mk'' x) = Quotient.mk'' ((↑g)⁻¹ • x)

The inverse normalizer permutation translates representatives by the inverse element.

noncomputable def TauCeti.MulAction.normalizerOrbitRelQuotientPermHom {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) : ↥(Subgroup.normalizer ↑H) →* Equiv.Perm (MulAction.orbitRel.Quotient (↥H) X)

The normalizer action on the orbit quotient as a permutation representation.

Equations

• TauCeti.MulAction.normalizerOrbitRelQuotientPermHom H = { toFun := TauCeti.MulAction.normalizerOrbitRelQuotientEquiv H, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.MulAction.normalizerOrbitRelQuotientPermHom_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (x : X) : ((normalizerOrbitRelQuotientPermHom H) g) (Quotient.mk'' x) = Quotient.mk'' (↑g • x)

The normalizer permutation homomorphism sends representatives to their translates.

theorem TauCeti.MulAction.normalizerOrbitRelQuotientPermHom_eq_one_of_mem {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (hg : ↑g ∈ H) : (normalizerOrbitRelQuotientPermHom H) g = 1

Any normalizer representative whose underlying group element lies in H acts trivially on the quotient by H-orbits.

noncomputable def TauCeti.MulAction.normalizerQuotientOrbitRelQuotientPermHom {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) : H.normalizerQuotient →* Equiv.Perm (MulAction.orbitRel.Quotient (↥H) X)

The action of the normalizer on an orbit quotient descends to N(H) / H.

Equations

• TauCeti.MulAction.normalizerQuotientOrbitRelQuotientPermHom H = H.normalizerQuotientLift (TauCeti.MulAction.normalizerOrbitRelQuotientPermHom H) ⋯

theorem TauCeti.MulAction.normalizerQuotientOrbitRelQuotientPermHom_mk_apply {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (x : X) : ((normalizerQuotientOrbitRelQuotientPermHom H) (H.normalizerQuotientMk g)) (Quotient.mk'' x) = Quotient.mk'' (↑g • x)

The descended normalizer-quotient action sends a normalizer representative to the corresponding translate on orbit classes.

@[implicit_reducible]

noncomputable def TauCeti.MulAction.normalizerQuotientOrbitRelQuotientMulAction {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) : MulAction H.normalizerQuotient (MulAction.orbitRel.Quotient (↥H) X)

The normalizer quotient N(H) / H acts on the quotient by H-orbits.

Equations

• TauCeti.MulAction.normalizerQuotientOrbitRelQuotientMulAction H = MulAction.compHom (MulAction.orbitRel.Quotient (↥H) X) (TauCeti.MulAction.normalizerQuotientOrbitRelQuotientPermHom H)

theorem TauCeti.MulAction.normalizerQuotientOrbitRelQuotient_smul_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) (g : ↥(Subgroup.normalizer ↑H)) (x : X) : H.normalizerQuotientMk g • Quotient.mk'' x = Quotient.mk'' (↑g • x)

A normalizer-quotient representative acts on the orbit quotient by translating representatives.

noncomputable def TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) [H.Normal] (x : X) : MulAction.orbitRel.Quotient (↥H) X ≃ H.normalizerQuotient

In a free transitive action, quotienting by a normal subgroup H identifies the H-orbit quotient with the normalizer quotient N(H) / H. The representative convention is the same as Mathlib's equivSubgroupOrbitsQuotientGroup: the class of g • x corresponds to the class of g⁻¹.

Equations

• TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal H x = (MulAction.equivSubgroupOrbitsQuotientGroup x H).trans H.normalizerQuotientEquivQuotientOfNormal.symm

@[simp]

theorem TauCeti.MulAction.normalizerQuotientEquivQuotientOfNormal_orbitRelQuotientEquivNormalizerQuotientOfNormal {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) [H.Normal] (x₀ : X) (x : MulAction.orbitRel.Quotient (↥H) X) : H.normalizerQuotientEquivQuotientOfNormal ((orbitRelQuotientEquivNormalizerQuotientOfNormal H x₀) x) = (MulAction.equivSubgroupOrbitsQuotientGroup x₀ H) x

The normal-subgroup orbit quotient equivalence, followed by the normalizer quotient's normal-case comparison, is Mathlib's equivalence to G ⧸ H.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal_symm_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) [H.Normal] (x : X) (g : ↥(Subgroup.normalizer ↑H)) : (orbitRelQuotientEquivNormalizerQuotientOfNormal H x).symm ↑g = Quotient.mk'' ((↑g)⁻¹ • x)

The inverse normal-subgroup orbit-quotient equivalence sends a normalizer representative to the orbit class of its inverse acting on the base point.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal_apply_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) [H.Normal] (x : X) (g : G) : (orbitRelQuotientEquivNormalizerQuotientOfNormal H x) (Quotient.mk'' (g • x)) = H.normalizerQuotientMk ⟨g⁻¹, ⋯⟩

The normal-subgroup orbit-quotient equivalence sends the class of g • x to the normalizer-quotient class of g⁻¹.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal_map_smul_eq_mul_inv {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) [H.Normal] (x₀ : X) (a : H.normalizerQuotient) (x : MulAction.orbitRel.Quotient (↥H) X) : (orbitRelQuotientEquivNormalizerQuotientOfNormal H x₀) (a • x) = (orbitRelQuotientEquivNormalizerQuotientOfNormal H x₀) x * a⁻¹

Under the normal-subgroup orbit-quotient equivalence, the descended normalizer-quotient action is right multiplication by the inverse.

theorem TauCeti.MulAction.orbitRelQuotientEquivNormalizerQuotientOfNormal_symm_mul_inv {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] [IsCancelSMul G X] (H : Subgroup G) [H.Normal] (x₀ : X) (a y : H.normalizerQuotient) : (orbitRelQuotientEquivNormalizerQuotientOfNormal H x₀).symm (y * a⁻¹) = a • (orbitRelQuotientEquivNormalizerQuotientOfNormal H x₀).symm y

Applying the inverse normal-subgroup orbit-quotient equivalence after right multiplication by a⁻¹ is the same as acting by a on the orbit quotient.

theorem TauCeti.MulAction.normalizerQuotientOrbitRelQuotientIsPretransitive {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (H : Subgroup G) [MulAction.IsPretransitive (↥(Subgroup.normalizer ↑H)) X] : MulAction.IsPretransitive H.normalizerQuotient (MulAction.orbitRel.Quotient (↥H) X)

If the normalizer of H acts transitively on X, then the descended N(H) / H action on the quotient by H-orbits is transitive.

theorem TauCeti.MulAction.normalizerQuotientOrbitRelQuotientIsPretransitiveOfNormal {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MulAction.IsPretransitive G X] (H : Subgroup G) [H.Normal] : MulAction.IsPretransitive H.normalizerQuotient (MulAction.orbitRel.Quotient (↥H) X)

If H is normal and G acts transitively on X, then the descended N(H) / H action on the quotient by H-orbits is transitive.

@[simp]

theorem TauCeti.MulAction.normalizerQuotientOrbitRelQuotient_smul_eq_smul_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] (H : Subgroup G) (a c : H.normalizerQuotient) (x : MulAction.orbitRel.Quotient (↥H) X) : a • x = c • x ↔ a = c

Equality after the descended N(H) / H action on an H-orbit quotient is equality of normalizer-quotient elements, provided the original action is free.

theorem TauCeti.MulAction.normalizerQuotientOrbitRelQuotientIsCancelSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsCancelSMul G X] (H : Subgroup G) : IsCancelSMul H.normalizerQuotient (MulAction.orbitRel.Quotient (↥H) X)

If a group acts freely on X, then the descended N(H) / H action on the quotient of X by H-orbits is free. This packages normalizerQuotientOrbitRelQuotient_smul_eq_smul_iff as the cancellativity of the descended action.

def TauCeti.MulAction.orbitRelQuotientCongr {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H : Type u_3} {Y : Type u_4} [Group H] [MulAction H Y] (φ : G ≃* H) (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = φ g • e x) : MulAction.orbitRel.Quotient G X ≃ MulAction.orbitRel.Quotient H Y

An equivariant equivalence induces an equivalence of orbit spaces: if e : X ≃ Y carries the G-action to the H-action along a group isomorphism φ : G ≃* H, it maps the G-orbits onto the H-orbits.

Equations

• TauCeti.MulAction.orbitRelQuotientCongr φ e he = Quotient.congr e ⋯

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientCongr_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H : Type u_3} {Y : Type u_4} [Group H] [MulAction H Y] (φ : G ≃* H) (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = φ g • e x) (x : X) : (orbitRelQuotientCongr φ e he) (Quotient.mk'' x) = Quotient.mk'' (e x)

orbitRelQuotientCongr φ e he sends the orbit of x to the orbit of e x.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientCongr_symm_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H : Type u_3} {Y : Type u_4} [Group H] [MulAction H Y] (φ : G ≃* H) (e : X ≃ Y) (he : ∀ (g : G) (x : X), e (g • x) = φ g • e x) (y : Y) : (orbitRelQuotientCongr φ e he).symm (Quotient.mk'' y) = Quotient.mk'' (e.symm y)

The inverse of orbitRelQuotientCongr φ e he sends the orbit of y to the orbit of e.symm y.

def TauCeti.MulAction.orbitRelQuotientSumEquiv {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {Y : Type u_3} [MulAction G Y] : MulAction.orbitRel.Quotient G (X ⊕ Y) ≃ MulAction.orbitRel.Quotient G X ⊕ MulAction.orbitRel.Quotient G Y

The orbits of an action on a sum are those of the two summands: G acts on X ⊕ Y summandwise, so its orbit space is the sum of the orbit spaces of X and Y.

Equations

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

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientSumEquiv_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {Y : Type u_3} [MulAction G Y] (x : X ⊕ Y) : orbitRelQuotientSumEquiv (Quotient.mk'' x) = Sum.map Quotient.mk'' Quotient.mk'' x

orbitRelQuotientSumEquiv sends the orbit of x : X ⊕ Y to the orbit of its summand: the orbit of Sum.inl a goes to Sum.inl of the orbit of a, and that of Sum.inr b to Sum.inr of the orbit of b.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientSumEquiv_symm_inl_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {Y : Type u_3} [MulAction G Y] (x : X) : orbitRelQuotientSumEquiv.symm (Sum.inl (Quotient.mk'' x)) = Quotient.mk'' (Sum.inl x)

The inverse of orbitRelQuotientSumEquiv sends Sum.inl of the orbit of x to the orbit of Sum.inl x.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientSumEquiv_symm_inr_mk {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {Y : Type u_3} [MulAction G Y] (y : Y) : orbitRelQuotientSumEquiv.symm (Sum.inr (Quotient.mk'' y)) = Quotient.mk'' (Sum.inr y)

The inverse of orbitRelQuotientSumEquiv sends Sum.inr of the orbit of y to the orbit of Sum.inr y.

@[simp]

theorem TauCeti.MulAction.stabilizer_sigma_mk {G : Type u_1} [Group G] {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → MulAction G (Y i)] (i : ι) (y : Y i) : MulAction.stabilizer G ⟨i, y⟩ = MulAction.stabilizer G y

The stabilizer of a point in a sigma type is its stabilizer in its fibre.

def TauCeti.MulAction.orbitRelQuotientSigmaEquiv {G : Type u_1} [Group G] {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → MulAction G (Y i)] : MulAction.orbitRel.Quotient G ((i : ι) × Y i) ≃ (i : ι) × MulAction.orbitRel.Quotient G (Y i)

The orbit space of a componentwise sigma action is the sigma type of the fibre orbit spaces. No transitivity or nonemptiness hypotheses are needed.

Equations

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

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientSigmaEquiv_mk {G : Type u_1} [Group G] {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → MulAction G (Y i)] (y : (i : ι) × Y i) : orbitRelQuotientSigmaEquiv (Quotient.mk'' y) = ⟨y.fst, Quotient.mk'' y.snd⟩

The sigma orbit equivalence sends a point to its fibre index and its fibre orbit.

@[simp]

theorem TauCeti.MulAction.orbitRelQuotientSigmaEquiv_symm_mk {G : Type u_1} [Group G] {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → MulAction G (Y i)] (i : ι) (y : Y i) : orbitRelQuotientSigmaEquiv.symm ⟨i, Quotient.mk'' y⟩ = Quotient.mk'' ⟨i, y⟩

The inverse sends a fibre orbit to the orbit of the corresponding sigma point.