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.
theorem
mul_action.supports_of_mem
(G : Type u_1)
{α : Type u_3}
[has_smul G α]
{s : set α}
{a : α}
(ha : a ∈ s) :
mul_action.supports G s a
theorem
add_action.supports_of_mem
(G : Type u_1)
{α : Type u_3}
[has_vadd G α]
{s : set α}
{a : α}
(ha : a ∈ s) :
add_action.supports G s a
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) :
mul_action.supports G t 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) :
add_action.supports G t 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) :
mul_action.supports G (g • s) (g • 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) :
add_action.supports G (g +ᵥ s) (g +ᵥ b)