Fixing submonoid, fixing subgroup of an action #

In the presence of of an action of a monoid or a group, this file defines the fixing submonoid or the fixing subgroup, and relates it to the set of fixed points via a Galois connection.

Main definitions #

fixingSubmonoid M s : in the presence of MulAction M α (with monoid M) it is the Submonoid M consisting of elements which fix s : Set α pointwise.
fixingSubmonoid_fixedPoints_gc M α is the GaloisConnection that relates fixingSubmonoid with fixedPoints.
fixingSubgroup M s : in the presence of MulAction M α (with Group M) it is the Subgroup M consisting of elements which fix s : Set α pointwise.
fixingSubgroup_fixedPoints_gc M α is the GaloisConnection that relates fixingSubgroup with fixedPoints.

TODO :

Maybe other lemmas are useful
Treat semigroups ?

source

ink

def fixingAddSubmonoid (M : Type u_1) {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M α] (s : Set α) :

AddSubmonoid M

The additive submonoid fixing a set under an AddAction.

Equations

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

source

ink

def fixingAddSubmonoid.proof_1 (M : Type u_1) {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M α] (s : Set α) {x : M} {y : M} (hx : x ∈ { ϕ | ∀ (x : ↑s), ϕ +ᵥ ↑x = ↑x }) (hy : y ∈ { ϕ | ∀ (x : ↑s), ϕ +ᵥ ↑x = ↑x }) (z : ↑s) :

x + y +ᵥ ↑z = ↑z

Equations

(_ : x + y +ᵥ ↑z = ↑z) = (_ : x + y +ᵥ ↑z = ↑z)

source

ink

def fixingAddSubmonoid.proof_2 (M : Type u_2) {α : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] (s : Set α) :

∀ (x : ↑s), 0 +ᵥ ↑x = ↑x

Equations

(_ : 0 +ᵥ ↑x = ↑x) = (_ : 0 +ᵥ ↑x = ↑x)

source

ink

def fixingSubmonoid (M : Type u_1) {α : Type u_2} [inst : Monoid M] [inst : MulAction M α] (s : Set α) :

Submonoid M

The submonoid fixing a set under a MulAction.

Equations

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

source

ink

theorem mem_fixingSubmonoid_iff (M : Type u_2) {α : Type u_1} [inst : Monoid M] [inst : MulAction M α] {s : Set α} {m : M} :

m ∈ fixingSubmonoid M s ↔ ∀ (y : α), y ∈ s → m • y = y

source

ink

theorem fixingSubmonoid_fixedPoints_gc (M : Type u_2) (α : Type u_1) [inst : Monoid M] [inst : MulAction M α] :

GaloisConnection (↑OrderDual.toDual ∘ fixingSubmonoid M) ((fun P => MulAction.fixedPoints { x // x ∈ P } α) ∘ ↑OrderDual.ofDual)

The Galois connection between fixing submonoids and fixed points of a monoid action

source

ink

theorem fixingSubmonoid_antitone (M : Type u_2) (α : Type u_1) [inst : Monoid M] [inst : MulAction M α] :

Antitone fun s => fixingSubmonoid M s

source

ink

theorem fixedPoints_antitone (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst : MulAction M α] :

Antitone fun P => MulAction.fixedPoints { x // x ∈ P } α

source

ink

theorem fixingSubmonoid_union (M : Type u_2) (α : Type u_1) [inst : Monoid M] [inst : MulAction M α] {s : Set α} {t : Set α} :

fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t

Fixing submonoid of union is intersection

source

ink

theorem fixingSubmonoid_unionᵢ (M : Type u_3) (α : Type u_2) [inst : Monoid M] [inst : MulAction M α] {ι : Sort u_1} {s : ι → Set α} :

fixingSubmonoid M (Set.unionᵢ fun i => s i) = ⨅ i, fixingSubmonoid M (s i)

Fixing submonoid of unionᵢ is intersection

source

ink

theorem fixedPoints_submonoid_sup (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst : MulAction M α] {P : Submonoid M} {Q : Submonoid M} :

MulAction.fixedPoints { x // x ∈ P ⊔ Q } α = MulAction.fixedPoints { x // x ∈ P } α ∩ MulAction.fixedPoints { x // x ∈ Q } α

Fixed points of sup of submonoids is intersection

source

ink

theorem fixedPoints_submonoid_supᵢ (M : Type u_2) (α : Type u_3) [inst : Monoid M] [inst : MulAction M α] {ι : Sort u_1} {P : ι → Submonoid M} :

MulAction.fixedPoints { x // x ∈ supᵢ P } α = Set.interᵢ fun i => MulAction.fixedPoints { x // x ∈ P i } α

Fixed points of supᵢ of submonoids is intersection

source

ink

def fixingAddSubgroup.proof_2 (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst : AddAction M α] (s : Set α) :

∀ {x : M}, x ∈ { toAddSubsemigroup := (fixingAddSubmonoid M s).toAddSubsemigroup, zero_mem' := (_ : 0 ∈ (fixingAddSubmonoid M s).toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier → ∀ (z : ↑s), -x +ᵥ ↑z = ↑z

Equations

(_ : -x +ᵥ ↑z = ↑z) = (_ : -x +ᵥ ↑z = ↑z)

source

ink

def fixingAddSubgroup (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst : AddAction M α] (s : Set α) :

AddSubgroup M

The additive subgroup fixing a set under an AddAction.

Equations

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

source

ink

def fixingAddSubgroup.proof_1 (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst : AddAction M α] (s : Set α) :

0 ∈ (fixingAddSubmonoid M s).toAddSubsemigroup.carrier

Equations

(_ : 0 ∈ (fixingAddSubmonoid M s).toAddSubsemigroup.carrier) = (_ : 0 ∈ (fixingAddSubmonoid M s).toAddSubsemigroup.carrier)

source

ink

def fixingSubgroup (M : Type u_1) {α : Type u_2} [inst : Group M] [inst : MulAction M α] (s : Set α) :

Subgroup M

The subgroup fixing a set under a MulAction.

Equations

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

source

ink

theorem mem_fixingSubgroup_iff (M : Type u_2) {α : Type u_1} [inst : Group M] [inst : MulAction M α] {s : Set α} {m : M} :

m ∈ fixingSubgroup M s ↔ ∀ (y : α), y ∈ s → m • y = y

source

ink

theorem fixingSubgroup_fixedPoints_gc (M : Type u_2) (α : Type u_1) [inst : Group M] [inst : MulAction M α] :

GaloisConnection (↑OrderDual.toDual ∘ fixingSubgroup M) ((fun P => MulAction.fixedPoints { x // x ∈ P } α) ∘ ↑OrderDual.ofDual)

The Galois connection between fixing subgroups and fixed points of a group action

source

ink

theorem fixingSubgroup_antitone (M : Type u_2) (α : Type u_1) [inst : Group M] [inst : MulAction M α] :

Antitone (fixingSubgroup M)

source

ink

theorem fixedPoints_subgroup_antitone (M : Type u_1) (α : Type u_2) [inst : Group M] [inst : MulAction M α] :

Antitone fun P => MulAction.fixedPoints { x // x ∈ P } α

source

ink

theorem fixingSubgroup_union (M : Type u_2) (α : Type u_1) [inst : Group M] [inst : MulAction M α] {s : Set α} {t : Set α} :

fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t

Fixing subgroup of union is intersection

source

ink

theorem fixingSubgroup_unionᵢ (M : Type u_3) (α : Type u_2) [inst : Group M] [inst : MulAction M α] {ι : Sort u_1} {s : ι → Set α} :

fixingSubgroup M (Set.unionᵢ fun i => s i) = ⨅ i, fixingSubgroup M (s i)

Fixing subgroup of unionᵢ is intersection

source

ink

theorem fixedPoints_subgroup_sup (M : Type u_1) (α : Type u_2) [inst : Group M] [inst : MulAction M α] {P : Subgroup M} {Q : Subgroup M} :

MulAction.fixedPoints { x // x ∈ P ⊔ Q } α = MulAction.fixedPoints { x // x ∈ P } α ∩ MulAction.fixedPoints { x // x ∈ Q } α

Fixed points of sup of subgroups is intersection

source

ink

theorem fixedPoints_subgroup_supᵢ (M : Type u_2) (α : Type u_3) [inst : Group M] [inst : MulAction M α] {ι : Sort u_1} {P : ι → Subgroup M} :

MulAction.fixedPoints { x // x ∈ supᵢ P } α = Set.interᵢ fun i => MulAction.fixedPoints { x // x ∈ P i } α

Fixed points of supᵢ of subgroups is intersection