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.

ink

def AddAction.Supports (G : Type u_1) {α : Type u_2} {β : Type u_3} [inst : VAdd G α] [inst : VAdd G β] (s : Set α) (b : β) : Prop

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

Equations

• AddAction.Supports G s b = ∀ (g : G), (∀ ⦃a : α⦄, a ∈ s → g +ᵥ a = a) → g +ᵥ b = b

ink

def MulAction.Supports (G : Type u_1) {α : Type u_2} {β : Type u_3} [inst : SMul G α] [inst : SMul G β] (s : Set α) (b : β) : Prop

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

Equations

• MulAction.Supports G s b = ∀ (g : G), (∀ ⦃a : α⦄, a ∈ s → g • a = a) → g • b = b

ink

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

ink

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

ink

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

ink

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

ink

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)

ink

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)