Support of an element under an action action #
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
AddAction.supports_of_mem
(G : Type u_2)
{α : Type u_1}
[inst : VAdd G α]
{s : Set α}
{a : α}
(ha : a ∈ s)
:
AddAction.Supports G s a
theorem
MulAction.supports_of_mem
(G : Type u_2)
{α : Type u_1}
[inst : SMul G α]
{s : Set α}
{a : α}
(ha : a ∈ s)
:
MulAction.Supports G s a
theorem
AddAction.Supports.mono
{G : Type u_2}
{α : Type u_1}
{β : Type u_3}
[inst : VAdd G α]
[inst : VAdd G β]
{s : Set α}
{t : Set α}
{b : β}
(h : s ⊆ t)
(hs : AddAction.Supports G s b)
:
AddAction.Supports G t b
theorem
MulAction.Supports.mono
{G : Type u_2}
{α : Type u_1}
{β : Type u_3}
[inst : SMul G α]
[inst : SMul G β]
{s : Set α}
{t : Set α}
{b : β}
(h : s ⊆ t)
(hs : MulAction.Supports G s b)
:
MulAction.Supports G t b
theorem
AddAction.Supports.vadd
{G : Type u_1}
{H : Type u_4}
{α : Type u_2}
{β : Type u_3}
[inst : AddGroup H]
[inst : VAdd G α]
[inst : VAdd G β]
[inst : AddAction H α]
[inst : VAdd H β]
[inst : VAddCommClass G H β]
[inst : VAddCommClass G H α]
{s : Set α}
{b : β}
(g : H)
(h : AddAction.Supports G s b)
:
AddAction.Supports G (g +ᵥ s) (g +ᵥ b)
theorem
MulAction.Supports.smul
{G : Type u_1}
{H : Type u_4}
{α : Type u_2}
{β : Type u_3}
[inst : Group H]
[inst : SMul G α]
[inst : SMul G β]
[inst : MulAction H α]
[inst : SMul H β]
[inst : SMulCommClass G H β]
[inst : SMulCommClass G H α]
{s : Set α}
{b : β}
(g : H)
(h : MulAction.Supports G s b)
:
MulAction.Supports G (g • s) (g • b)