mathlib3 documentation

group_theory.group_action.support

Support of an element under an action action #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given an action of a group G on a type α, we say that a set s : set α supports an element a : α if, for all g that fix s pointwise, g fixes a.

This is crucial in Fourier-Motzkin constructions.

def add_action.supports (G : Type u_1) {α : Type u_3} {β : Type u_4} [has_vadd G α] [has_vadd G β] (s : set α) (b : β) :
Prop

A set s supports b if g +ᵥ b = b whenever g +ᵥ a = a for all a ∈ s.

Equations
def mul_action.supports (G : Type u_1) {α : Type u_3} {β : Type u_4} [has_smul G α] [has_smul G β] (s : set α) (b : β) :
Prop

A set s supports b if g • b = b whenever g • a = a for all a ∈ s.

Equations
theorem mul_action.supports_of_mem (G : Type u_1) {α : Type u_3} [has_smul G α] {s : set α} {a : α} (ha : a s) :
theorem add_action.supports_of_mem (G : Type u_1) {α : Type u_3} [has_vadd G α] {s : set α} {a : α} (ha : a s) :
theorem mul_action.supports.mono {G : Type u_1} {α : Type u_3} {β : Type u_4} [has_smul G α] [has_smul G β] {s t : set α} {b : β} (h : s t) (hs : mul_action.supports G s b) :
theorem add_action.supports.mono {G : Type u_1} {α : Type u_3} {β : Type u_4} [has_vadd G α] [has_vadd G β] {s t : set α} {b : β} (h : s t) (hs : add_action.supports G s b) :
theorem mul_action.supports.smul {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [group H] [has_smul G α] [has_smul G β] [mul_action H α] [has_smul H β] [smul_comm_class G H β] [smul_comm_class G H α] {s : set α} {b : β} (g : H) (h : mul_action.supports G s b) :
theorem add_action.supports.vadd {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [add_group H] [has_vadd G α] [has_vadd G β] [add_action H α] [has_vadd H β] [vadd_comm_class G H β] [vadd_comm_class G H α] {s : set α} {b : β} (g : H) (h : add_action.supports G s b) :