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 (stablizer M a) s`

  • SubMulAction.ofFixingSubgroup_insert_map : the equivariant map between SubMulAction.ofFixingSubgroup M (insert a s) and SubMulAction.ofFixingSubgroup (stablizer 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.

Equations

• SubMulAction.ofFixingSubgroup M s = { carrier := sᶜ, smul_mem' := ⋯ }

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.

Equations

• SubAddAction.ofFixingAddSubgroup M s = { carrier := sᶜ, vadd_mem' := ⋯ }

@[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

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.

Equations

• SubMulAction.ofFixingSubgroup_equivariantMap M s = { toFun := fun (x : ↥(SubMulAction.ofFixingSubgroup M s)) => ↑x, map_smul' := ⋯ }

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.

Equations

• SubAddAction.ofFixingAddSubgroup_equivariantMap M s = { toFun := fun (x : ↥(SubAddAction.ofFixingAddSubgroup M s)) => ↑x, map_vadd' := ⋯ }

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.

Equations

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

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.

Equations

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

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 M 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.

Equations

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

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 M 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.

Equations

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

@[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 M 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 M 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 M 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 M 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.

Equations

• SubMulAction.fixingSubgroupEquivFixingSubgroup M α hg = (MulEquiv.subgroupMap (MulAut.conj g) (fixingSubgroup M t)).trans (MulEquiv.subgroupCongr ⋯)

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.

Equations

• SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup M α hg = (AddEquiv.addSubgroupMap (AddAut.conj g) (fixingAddSubgroup M t)).trans (AddEquiv.addSubgroupCongr ⋯)

@[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 M α 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 M α 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 M α hg)] ↥(ofFixingSubgroup M s)

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

Equations

• SubMulAction.conjMap_ofFixingSubgroup M α hg = { toFun := fun (x : ↥(SubMulAction.ofFixingSubgroup M t)) => match x with | ⟨x, hx⟩ => ⟨g • x, ⋯⟩, map_smul' := ⋯ }

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 M α hg)] ↥(ofFixingAddSubgroup M s)

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

Equations

• SubAddAction.conjMap_ofFixingAddSubgroup M α hg = { toFun := fun (x : ↥(SubAddAction.ofFixingAddSubgroup M t)) => match x with | ⟨x, hx⟩ => ⟨g +ᵥ x, ⋯⟩, map_vadd' := ⋯ }

@[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 M α 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 M α 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 M α 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 M α hst)

def SubMulAction.map_ofFixingSubgroupUnion (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] (s t : Set α) : let ψ := 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.

Equations

• SubMulAction.map_ofFixingSubgroupUnion M α s t = { toFun := fun (x : ↥(SubMulAction.ofFixingSubgroup M (s ∪ t))) => ⟨⟨↑x, ⋯⟩, ⋯⟩, map_smul' := ⋯ }

def SubAddAction.map_ofFixingAddSubgroupUnion (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] (s t : Set α) : let ψ := 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.

Equations

• SubAddAction.map_ofFixingAddSubgroupUnion M α s t = { toFun := fun (x : ↥(SubAddAction.ofFixingAddSubgroup M (s ∪ t))) => ⟨⟨↑x, ⋯⟩, ⋯⟩, map_vadd' := ⋯ }

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.

Equations

• SubMulAction.ofFixingSubgroup_of_inclusion M α hst = { toFun := fun (y : ↥(SubMulAction.ofFixingSubgroup M s)) => ⟨↑y, ⋯⟩, map_smul' := ⋯ }

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.

Equations

• SubAddAction.ofFixingAddSubgroup_of_inclusion M α hst = { toFun := fun (y : ↥(SubAddAction.ofFixingAddSubgroup M s)) => ⟨↑y, ⋯⟩, map_vadd' := ⋯ }

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 : α) : let φ := 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}.

Equations

• SubMulAction.ofFixingSubgroup_of_singleton M α a = { toFun := fun (x : ↥(SubMulAction.ofFixingSubgroup M {a})) => ⟨↑x, ⋯⟩, map_smul' := ⋯ }

def SubAddAction.ofFixingAddSubgroup_of_singleton (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] (a : α) : let φ := 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}.

Equations

• SubAddAction.ofFixingAddSubgroup_of_singleton M α a = { toFun := fun (x : ↥(SubAddAction.ofFixingAddSubgroup M {a})) => ⟨↑x, ⋯⟩, map_vadd' := ⋯ }

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) : let φ := MulEquiv.subgroupCongr ⋯; ↥(ofFixingSubgroup M s) →ₑ[⇑φ] ↥(ofFixingSubgroup M t)

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

Equations

• SubMulAction.ofFixingSubgroup_of_eq M α hst = { toFun := fun (x : ↥(SubMulAction.ofFixingSubgroup M s)) => match x with | ⟨x, hx⟩ => ⟨x, ⋯⟩, map_smul' := ⋯ }

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

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

Equations

• SubAddAction.ofFixingAddSubgroup_of_eq M α hst = { toFun := fun (x : ↥(SubAddAction.ofFixingAddSubgroup M s)) => match x with | ⟨x, hx⟩ => ⟨x, ⋯⟩, map_vadd' := ⋯ }

@[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 α] {n : ℕ} {s : Set α} [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.

Equations

• SubMulAction.ofFixingSubgroup.append x = Fin.Embedding.append ⋯

noncomputable def SubAddAction.ofFixingAddSubgroup.append {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {n : ℕ} {s : Set α} [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.

Equations

• SubAddAction.ofFixingAddSubgroup.append x = Fin.Embedding.append ⋯

theorem SubMulAction.ofFixingSubgroup.append_left {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {n : ℕ} {s : Set α} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingSubgroup M s)) (i : Fin s.ncard) : let 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 α] {n : ℕ} {s : Set α} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingAddSubgroup M s)) (i : Fin s.ncard) : let 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 α] {n : ℕ} {s : Set α} [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 α] {n : ℕ} {s : Set α} [Finite ↑s] (x : Fin n ↪ ↥(ofFixingAddSubgroup M s)) (i : Fin n) : (append x) (Fin.natAdd s.ncard i) = ↑(x i)