SubMulActions on complements of invariant subsets

• We define SubMulAction of an invariant subset in various contexts, especially stabilizers and fixing subgroups : SubMulAction_of_compl, SubMulAction_of_stabilizer, SubMulAction_of_fixingSubgroup.

• We define equivariant maps that relate various of these SubMulActions and permit to manipulate them in a relatively smooth way:

  • SubMulAction.ofFixingSubgroupEmpty_equivariantMap: the identity map, when the set is the empty set.

  • SubMulAction.fixingSubgroupInsertEquiv M a s : the multiplicative equivalence between fixingSubgroup M (insert a s)`` and fixingSubgroup (stabilizer M a) s`

  • SubMulAction.ofFixingSubgroup_insert_map : the equivariant map between SubMulAction.ofFixingSubgroup M (insert a s) and SubMulAction.ofFixingSubgroup (stabilizer M a) s.

  • SubMulAction.fixingSubgroupEquivFixingSubgroup: the multiplicative equivalence between SubMulAction.fixingSubgroup M s and SubMulAction.fixingSubgroup M t induced by g : M such that g • t = s.

  • SubMulAction.conjMap_ofFixingSubgroup: the equivariant map between SubMulAction.ofFixingSubgroup M t and SubMulAction.ofFIxingSubgroup M s induced by g : M such that g • t = s.

  • SubMulAction.ofFixingSubgroup_of_inclusion: the identity from SubMulAction.ofFixingSubgroup M s to SubMulAction.ofFixingSubgroup M t, when t ⊆ s, as an equivariant map.

  • SubMulAction.ofFixingSubgroup_of_singleton: the identity map from SubMulAction.ofStablizer M a to SubMulAction.ofFixingSubgroup M {a}.

  • SubMulAction.ofFixingSubgroup_of_eq: the identity from SubMulAction.ofFixingSubgroup M s to SubMulAction.ofFixingSubgroup M t, when s = t, as an equivariant map.

  • SubMulAction.ofFixingSubgroup.append: appends an enumeration of ofFixingSubgroup M s at the end of an enumeration of s, as an equivariant map.

def SubMulAction.ofFixingSubgroup (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (s : Set α) : SubMulAction (↥(fixingSubgroup M s)) α

The SubMulAction of fixingSubgroup M s on the complement of s.

def SubAddAction.ofFixingAddSubgroup (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] (s : Set α) : SubAddAction (↥(fixingAddSubgroup M s)) α

The SubAddAction of fixingAddSubgroup M s on the complement of s.

@[simp]

theorem SubMulAction.ofFixingSubgroup_carrier (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (s : Set α) : (ofFixingSubgroup M s).carrier = sᶜ

@[simp]

theorem SubAddAction.ofFixingAddSubgroup_carrier (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] (s : Set α) : (ofFixingAddSubgroup M s).carrier = sᶜ

theorem SubMulAction.mem_ofFixingSubgroup_iff (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {x : α} : x ∈ ofFixingSubgroup M s ↔ x ∉ s

theorem SubAddAction.mem_ofFixingAddSubgroup_iff (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {x : α} : x ∈ ofFixingAddSubgroup M s ↔ x ∉ s

theorem SubMulAction.not_mem_of_mem_ofFixingSubgroup {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} (x : ↥(ofFixingSubgroup M s)) : ↑x ∉ s

theorem SubAddAction.not_mem_of_mem_ofFixingAddSubgroup {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} (x : ↥(ofFixingAddSubgroup M s)) : ↑x ∉ s

theorem SubMulAction.disjoint_val_image {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {t : Set ↥(ofFixingSubgroup M s)} : Disjoint s (Subtype.val '' t)

theorem SubAddAction.disjoint_val_image {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {t : Set ↥(ofFixingAddSubgroup M s)} : Disjoint s (Subtype.val '' t)

def SubMulAction.ofFixingSubgroup_equivariantMap (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (s : Set α) : ↥(ofFixingSubgroup M s) →ₑ[⇑(fixingSubgroup M s).subtype] α

The identity map of the SubMulAction of the fixingSubgroup into the ambient set, as an equivariant map.

def SubAddAction.ofFixingAddSubgroup_equivariantMap (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] (s : Set α) : ↥(ofFixingAddSubgroup M s) →ₑ[⇑(fixingAddSubgroup M s).subtype] α

The identity map of the SubAddAction of the fixingAddSubgroup into the ambient set, as an equivariant map.

theorem SubMulAction.ofFixingSubgroup_equivariantMap_injective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} : Function.Injective ⇑(ofFixingSubgroup_equivariantMap M s)

theorem SubAddAction.ofFixingAddSubgroup_equivariantMap_injective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} : Function.Injective ⇑(ofFixingAddSubgroup_equivariantMap M s)

theorem SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] : Function.Bijective ⇑(ofFixingSubgroup_equivariantMap M ∅)

theorem SubAddAction.ofFixingAddSubgroupEmpty_equivariantMap_bijective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] : Function.Bijective ⇑(ofFixingAddSubgroup_equivariantMap M ∅)

theorem SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] : Function.Surjective ⇑(fixingSubgroup M ∅).subtype

theorem SubAddAction.of_fixingAddSubgroupEmpty_mapScalars_surjective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] : Function.Surjective ⇑(fixingAddSubgroup M ∅).subtype

theorem SubMulAction.mem_fixingSubgroup_insert_iff {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {a : α} {s : Set α} {m : M} : m ∈ fixingSubgroup M (insert a s) ↔ m • a = a ∧ m ∈ fixingSubgroup M s

theorem SubAddAction.mem_fixingAddSubgroup_insert_iff {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {a : α} {s : Set α} {m : M} : m ∈ fixingAddSubgroup M (insert a s) ↔ m +ᵥ a = a ∧ m ∈ fixingAddSubgroup M s

theorem SubMulAction.fixingSubgroup_of_insert {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] (a : α) (s : Set ↥(ofStabilizer M a)) : fixingSubgroup M (insert a ((fun (x : ↥(ofStabilizer M a)) => ↑x) '' s)) = Subgroup.map (MulAction.stabilizer M a).subtype (fixingSubgroup (↥(MulAction.stabilizer M a)) s)

theorem SubAddAction.fixingAddSubgroup_of_insert {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] (a : α) (s : Set ↥(ofStabilizer M a)) : fixingAddSubgroup M (insert a ((fun (x : ↥(ofStabilizer M a)) => ↑x) '' s)) = AddSubgroup.map (AddAction.stabilizer M a).subtype (fixingAddSubgroup (↥(AddAction.stabilizer M a)) s)

theorem SubMulAction.mem_ofFixingSubgroup_insert_iff {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {a : α} {s : Set ↥(ofStabilizer M a)} {x : α} : x ∈ ofFixingSubgroup M (insert a ((fun (x : ↥(ofStabilizer M a)) => ↑x) '' s)) ↔ ∃ (hx : x ∈ ofStabilizer M a), ⟨x, hx⟩ ∈ ofFixingSubgroup (↥(MulAction.stabilizer M a)) s

theorem SubAddAction.mem_ofFixingAddSubgroup_insert_iff {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {a : α} {s : Set ↥(ofStabilizer M a)} {x : α} : x ∈ ofFixingAddSubgroup M (insert a ((fun (x : ↥(ofStabilizer M a)) => ↑x) '' s)) ↔ ∃ (hx : x ∈ ofStabilizer M a), ⟨x, hx⟩ ∈ ofFixingAddSubgroup (↥(AddAction.stabilizer M a)) s

def SubMulAction.fixingSubgroupInsertEquiv {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] (a : α) (s : Set ↥(ofStabilizer M a)) : ↥(fixingSubgroup M (insert a (Subtype.val '' s))) ≃* ↥(fixingSubgroup (↥(MulAction.stabilizer M a)) s)

The natural group isomorphism between fixing subgroups.

def SubAddAction.fixingAddSubgroupInsertEquiv {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] (a : α) (s : Set ↥(ofStabilizer M a)) : ↥(fixingAddSubgroup M (insert a (Subtype.val '' s))) ≃+ ↥(fixingAddSubgroup (↥(AddAction.stabilizer M a)) s)

The natural additive group isomorphism between fixing additive subgroups.

def SubMulAction.ofFixingSubgroup_insert_map {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] (a : α) (s : Set ↥(ofStabilizer M a)) : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s))) →ₑ[⇑(fixingSubgroupInsertEquiv a s)] ↥(ofFixingSubgroup (↥(MulAction.stabilizer M a)) s)

The identity map of fixing subgroup of stabilizer into the fixing subgroup of the extended set, as an equivariant map.

def SubAddAction.ofFixingAddSubgroup_insert_map {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] (a : α) (s : Set ↥(ofStabilizer M a)) : ↥(ofFixingAddSubgroup M (insert a (Subtype.val '' s))) →ₑ[⇑(fixingAddSubgroupInsertEquiv a s)] ↥(ofFixingAddSubgroup (↥(AddAction.stabilizer M a)) s)

The identity map of fixing additive subgroup of stabilizer into the fixing additive subgroup of the extended set, as an equivariant map.

@[simp]

theorem SubMulAction.ofFixingSubgroup_insert_map_apply {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {a : α} {s : Set ↥(ofStabilizer M a)} {x : α} (hx : x ∈ ofFixingSubgroup M (insert a (Subtype.val '' s))) : ↑↑((ofFixingSubgroup_insert_map a s) ⟨x, hx⟩) = x

@[simp]

theorem SubAddAction.ofFixingAddSubgroup_insert_map_apply {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {a : α} {s : Set ↥(ofStabilizer M a)} {x : α} (hx : x ∈ ofFixingAddSubgroup M (insert a (Subtype.val '' s))) : ↑↑((ofFixingAddSubgroup_insert_map a s) ⟨x, hx⟩) = x

theorem SubMulAction.ofFixingSubgroup_insert_map_bijective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {a : α} {s : Set ↥(ofStabilizer M a)} : Function.Bijective ⇑(ofFixingSubgroup_insert_map a s)

theorem SubAddAction.ofFixingAddSubgroup_insert_map_bijective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {a : α} {s : Set ↥(ofStabilizer M a)} : Function.Bijective ⇑(ofFixingAddSubgroup_insert_map a s)

theorem Set.conj_mem_fixingSubgroup {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} (hg : g • t = s) {k : M} (hk : k ∈ fixingSubgroup M t) : (MulAut.conj g) k ∈ fixingSubgroup M s

theorem Set.conj_mem_fixingAddSubgroup {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s) {k : M} (hk : k ∈ fixingAddSubgroup M t) : (AddAut.conj g) k ∈ fixingAddSubgroup M s

theorem SubMulAction.fixingSubgroup_map_conj_eq {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} (hg : g • t = s) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M t) = fixingSubgroup M s

theorem SubAddAction.fixingAddSubgroup_map_conj_eq {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s) : AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (fixingAddSubgroup M t) = fixingAddSubgroup M s

theorem SubMulAction.fixingSubgroup_smul_eq_fixingSubgroup_map_conj {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] (s : Set α) (g : M) : fixingSubgroup M (g • s) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)

The fixingSubgroup of g • s is the conjugate of the fixingSubgroup of s by g.

theorem SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] (s : Set α) (g : M) : fixingAddSubgroup M (g +ᵥ s) = AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (fixingAddSubgroup M s)

The fixingAddSubgroup of g +ᵥ s is the conjugate of the fixingAddSubgroup of s by g.

def SubMulAction.fixingSubgroupEquivFixingSubgroup {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} (hg : g • t = s) : ↥(fixingSubgroup M t) ≃* ↥(fixingSubgroup M s)

The equivalence of fixingSubgroup M t with fixingSubgroup M s when s is a translate of t.

def SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s) : ↥(fixingAddSubgroup M t) ≃+ ↥(fixingAddSubgroup M s)

The equivalence of fixingSubgroup M t with fixingSubgroup M s when s is a translate of t.

@[simp]

theorem SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} (hg : g • t = s) (x : ↥(fixingSubgroup M t)) : ↑((fixingSubgroupEquivFixingSubgroup hg) x) = (MulAut.conj g) ↑x

@[simp]

theorem SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup_coe_apply {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s) (x : ↥(fixingAddSubgroup M t)) : ↑((fixingAddSubgroupEquivFixingAddSubgroup hg) x) = (AddAut.conj g) ↑x

def SubMulAction.conjMap_ofFixingSubgroup {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} (hg : g • t = s) : ↥(ofFixingSubgroup M t) →ₑ[⇑(fixingSubgroupEquivFixingSubgroup hg)] ↥(ofFixingSubgroup M s)

Conjugation induces an equivariant map between the SubMulAction of the fixing subgroup of a subset and that of a translate.

def SubAddAction.conjMap_ofFixingAddSubgroup {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s) : ↥(ofFixingAddSubgroup M t) →ₑ[⇑(fixingAddSubgroupEquivFixingAddSubgroup hg)] ↥(ofFixingAddSubgroup M s)

Conjugation induces an equivariant map between the SubAddAction of the fixing subgroup of a subset and that of a translate.

@[simp]

theorem SubMulAction.conjMap_ofFixingSubgroup_coe_apply {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} {hg : g • t = s} (x : ↥(ofFixingSubgroup M t)) : ↑((conjMap_ofFixingSubgroup hg) x) = g • ↑x

@[simp]

theorem SubAddAction.conjMap_ofFixingAddSubgroup_coe_apply {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} {hg : g +ᵥ t = s} (x : ↥(ofFixingAddSubgroup M t)) : ↑((conjMap_ofFixingAddSubgroup hg) x) = g +ᵥ ↑x

theorem SubMulAction.conjMap_ofFixingSubgroup_bijective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} {hst : g • s = t} : Function.Bijective ⇑(conjMap_ofFixingSubgroup hst)

theorem SubAddAction.conjMap_ofFixingAddSubgroup_bijective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} {hst : g +ᵥ s = t} : Function.Bijective ⇑(conjMap_ofFixingAddSubgroup hst)

theorem SubMulAction.mem_fixingSubgroup_union_iff {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {g : M} : g ∈ fixingSubgroup M (s ∪ t) ↔ g ∈ fixingSubgroup M s ∧ g ∈ fixingSubgroup M t

theorem SubAddAction.mem_fixingAddSubgroup_union_iff {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {g : M} : g ∈ fixingAddSubgroup M (s ∪ t) ↔ g ∈ fixingAddSubgroup M s ∧ g ∈ fixingAddSubgroup M t

def SubMulAction.fixingSubgroup_union_to_fixingSubgroup_of_fixingSubgroup {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} : ↥(fixingSubgroup M (s ∪ t)) →* ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t))

The group morphism from fixingSubgroup of a union to the iterated fixingSubgroup.

def SubAddAction.fixingAddSubgroup_union_to_fixingAddSubgroup_of_fixingAddSubgroup {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} : ↥(fixingAddSubgroup M (s ∪ t)) →+ ↥(fixingAddSubgroup (↥(fixingAddSubgroup M s)) (Subtype.val ⁻¹' t))

The additive group morphism from fixingAddSubgroup of a union to the iterated fixingAddSubgroup.

def SubMulAction.map_ofFixingSubgroupUnion (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (s t : Set α) : have ψ := fun (m : ↥(fixingSubgroup M (s ∪ t))) => ⟨⟨↑m, ⋯⟩, ⋯⟩; ↥(ofFixingSubgroup M (s ∪ t)) →ₑ[ψ] ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t))

The identity between the iterated SubMulAction of the fixingSubgroup and the SubMulAction of the fixingSubgroup of the union, as an equivariant map.

def SubAddAction.map_ofFixingAddSubgroupUnion (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] (s t : Set α) : have ψ := fun (m : ↥(fixingAddSubgroup M (s ∪ t))) => ⟨⟨↑m, ⋯⟩, ⋯⟩; ↥(ofFixingAddSubgroup M (s ∪ t)) →ₑ[ψ] ↥(ofFixingAddSubgroup (↥(fixingAddSubgroup M s)) (Subtype.val ⁻¹' t))

The identity between the iterated SubAddAction of the fixingAddSubgroup and the SubAddAction of the fixingAddSubgroup of the union, as an equivariant map.

theorem SubMulAction.map_ofFixingSubgroupUnion_def {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} (x : ↥(ofFixingSubgroup M (s ∪ t))) : ↑↑((map_ofFixingSubgroupUnion M s t) x) = ↑x

theorem SubAddAction.map_ofFixingAddSubgroupUnion_def {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} (x : ↥(ofFixingAddSubgroup M (s ∪ t))) : ↑↑((map_ofFixingAddSubgroupUnion M s t) x) = ↑x

theorem SubMulAction.map_ofFixingSubgroupUnion_bijective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} : Function.Bijective ⇑(map_ofFixingSubgroupUnion M s t)

theorem SubAddAction.map_ofFixingAddSubgroupUnion_bijective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} : Function.Bijective ⇑(map_ofFixingAddSubgroupUnion M s t)

def SubMulAction.ofFixingSubgroup_of_inclusion (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} (hst : t ⊆ s) : ↥(ofFixingSubgroup M s) →ₑ[⇑(Subgroup.inclusion ⋯)] ↥(ofFixingSubgroup M t)

The equivariant map on SubMulAction.ofFixingSubgroup given a set inclusion.

def SubAddAction.ofFixingAddSubgroup_of_inclusion (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} (hst : t ⊆ s) : ↥(ofFixingAddSubgroup M s) →ₑ[⇑(AddSubgroup.inclusion ⋯)] ↥(ofFixingAddSubgroup M t)

The equivariant map on SubAddAction.ofFixingAddSubgroup given a set inclusion.

theorem SubMulAction.ofFixingSubgroup_of_inclusion_injective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {hst : t ⊆ s} : Function.Injective ⇑(ofFixingSubgroup_of_inclusion M hst)

theorem SubAddAction.ofFixingAddSubgroup_of_inclusion_injective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {hst : t ⊆ s} : Function.Injective ⇑(ofFixingAddSubgroup_of_inclusion M hst)

def SubMulAction.ofFixingSubgroup_of_singleton (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (a : α) : have φ := fun (x : ↥(fixingSubgroup M {a})) => match x with | ⟨m, hm⟩ => ⟨m, ⋯⟩; ↥(ofFixingSubgroup M {a}) →ₑ[φ] ↥(ofStabilizer M a)

The equivariant map between SubMulAction.ofStabilizer M a and ofFixingSubgroup M {a}.

def SubAddAction.ofFixingAddSubgroup_of_singleton (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] (a : α) : have φ := fun (x : ↥(fixingAddSubgroup M {a})) => match x with | ⟨m, hm⟩ => ⟨m, ⋯⟩; ↥(ofFixingAddSubgroup M {a}) →ₑ[φ] ↥(ofStabilizer M a)

The equivariant map between SubAddAction.ofStabilizer M a and ofFixingAddSubgroup M {a}.

theorem SubMulAction.ofFixingSubgroup_of_singleton_bijective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {a : α} : Function.Bijective ⇑(ofFixingSubgroup_of_singleton M a)

theorem SubAddAction.ofFixingAddSubgroup_of_singleton_bijective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {a : α} : Function.Bijective ⇑(ofFixingAddSubgroup_of_singleton M a)

def SubMulAction.ofFixingSubgroup_of_eq (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} (hst : s = t) : have φ := MulEquiv.subgroupCongr ⋯; ↥(ofFixingSubgroup M s) →ₑ[⇑φ] ↥(ofFixingSubgroup M t)

The identity between the SubMulActions of fixingSubgroups of equal sets, as an equivariant map.

def SubAddAction.ofFixingAddSubgroup_of_eq (M : Type u_1) {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} (hst : s = t) : have φ := AddEquiv.addSubgroupCongr ⋯; ↥(ofFixingAddSubgroup M s) →ₑ[⇑φ] ↥(ofFixingAddSubgroup M t)

The identity between the SubAddActions of fixingAddSubgroups of equal sets, as an equivariant map.

@[simp]

theorem SubMulAction.ofFixingSubgroup_of_eq_apply {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {hst : s = t} (x : ↥(ofFixingSubgroup M s)) : ↑((ofFixingSubgroup_of_eq M hst) x) = ↑x

@[simp]

theorem SubAddAction.ofFixingAddSubgroup_of_eq_apply {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {hst : s = t} (x : ↥(ofFixingAddSubgroup M s)) : ↑((ofFixingAddSubgroup_of_eq M hst) x) = ↑x

theorem SubMulAction.ofFixingSubgroup_of_eq_bijective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s t : Set α} {hst : s = t} : Function.Bijective ⇑(ofFixingSubgroup_of_eq M hst)

theorem SubAddAction.ofFixingAddSubgroup_of_eq_bijective {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s t : Set α} {hst : s = t} : Function.Bijective ⇑(ofFixingAddSubgroup_of_eq M hst)

noncomputable def SubMulAction.ofFixingSubgroup.append {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {n : ℕ} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingSubgroup M s)) : Fin (s.ncard + n) ↪ α

Append Fin m ↪ ofFixingSubgroup M s at the end of an enumeration of s.

noncomputable def SubAddAction.ofFixingAddSubgroup.append {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {n : ℕ} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingAddSubgroup M s)) : Fin (s.ncard + n) ↪ α

Append Fin m ↪ ofFixingSubgroup M s at the end of an enumeration of s.

theorem SubMulAction.ofFixingSubgroup.append_left {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {n : ℕ} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingSubgroup M s)) (i : Fin s.ncard) : have Hs := ⋯; (append x) (Fin.castAdd n i) = ↑((Classical.choice Hs) i)

theorem SubAddAction.ofFixingAddSubgroup.append_left {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {n : ℕ} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingAddSubgroup M s)) (i : Fin s.ncard) : have Hs := ⋯; (append x) (Fin.castAdd n i) = ↑((Classical.choice Hs) i)

theorem SubMulAction.ofFixingSubgroup.append_right {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {n : ℕ} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingSubgroup M s)) (i : Fin n) : (append x) (Fin.natAdd s.ncard i) = ↑(x i)

theorem SubAddAction.ofFixingAddSubgroup.append_right {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {s : Set α} {n : ℕ} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingAddSubgroup M s)) (i : Fin n) : (append x) (Fin.natAdd s.ncard i) = ↑(x i)