Blocks

Given SMul G X, an action of a type G on a type X, we define

• the predicate IsBlock G B states that B : Set X is a block, which means that the sets g • B, for g ∈ G, are equal or disjoint.

• a bunch of lemmas that give examples of “trivial” blocks : ⊥, ⊤, singletons, and non trivial blocks: orbit of the group, orbit of a normal subgroup…

The non-existence of nontrivial blocks is the definition of primitive actions.

References

We follow [wieland1964].

theorem MulAction.orbit.eq_or_disjoint {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (a : X) (b : X) : MulAction.orbit G a = MulAction.orbit G b ∨ Disjoint (MulAction.orbit G a) (MulAction.orbit G b)

theorem MulAction.orbit.pairwiseDisjoint {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] : (Set.range fun (x : X) => MulAction.orbit G x).PairwiseDisjoint id

theorem MulAction.IsPartition.of_orbits {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] : Setoid.IsPartition (Set.range fun (a : X) => MulAction.orbit G a)

Orbits of an element form a partition

def MulAction.IsFixedBlock (G : Type u_1) {X : Type u_2} [SMul G X] (B : Set X) : Prop

For SMul G X, a fixed block is a Set X which is fully invariant: g • B = B for all g : G

Equations

• MulAction.IsFixedBlock G B = ∀ (g : G), g • B = B

def MulAction.IsInvariantBlock (G : Type u_1) {X : Type u_2} [SMul G X] (B : Set X) : Prop

For SMul G X, an invariant block is a Set X which is stable: g • B ⊆ B for all g : G

Equations

• MulAction.IsInvariantBlock G B = ∀ (g : G), g • B ⊆ B

def MulAction.IsTrivialBlock {X : Type u_2} (B : Set X) : Prop

A trivial block is a Set X which is either a subsingleton or ⊤ (it is not necessarily a block…)

Equations

• MulAction.IsTrivialBlock B = (B.Subsingleton ∨ B = ⊤)

def MulAction.IsBlock (G : Type u_1) {X : Type u_2} [SMul G X] (B : Set X) : Prop

For SMul G X, a block is a Set X whose translates are pairwise disjoint

Equations

• MulAction.IsBlock G B = (Set.range fun (g : G) => g • B).PairwiseDisjoint id

theorem MulAction.IsBlock.def {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} : MulAction.IsBlock G B ↔ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)

A set B is a block iff for all g, g', the sets g • B and g' • B are either equal or disjoint

theorem MulAction.IsBlock.mk_notempty {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} : MulAction.IsBlock G B ↔ ∀ (g g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B

Alternate definition of a block

theorem MulAction.IsFixedBlock.isBlock {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} (hfB : MulAction.IsFixedBlock G B) : MulAction.IsBlock G B

A fixed block is a block

theorem MulAction.isBlock_empty {G : Type u_1} (X : Type u_2) [SMul G X] : MulAction.IsBlock G ⊥

The empty set is a block

theorem MulAction.isBlock_singleton {G : Type u_1} {X : Type u_2} [SMul G X] (a : X) : MulAction.IsBlock G {a}

theorem MulAction.isBlock_subsingleton {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} (hB : B.Subsingleton) : MulAction.IsBlock G B

Subsingletons are (trivial) blocks

theorem MulAction.IsBlock.smul_eq_or_disjoint {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} (hB : MulAction.IsBlock G B) (g : G) : g • B = B ∨ Disjoint (g • B) B

theorem MulAction.IsBlock.def_one {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} : MulAction.IsBlock G B ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B

theorem MulAction.IsBlock.mk_notempty_one {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} : MulAction.IsBlock G B ↔ ∀ (g : G), g • B ∩ B ≠ ∅ → g • B = B

theorem MulAction.IsBlock.mk_mem {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} : MulAction.IsBlock G B ↔ ∀ (g : G), ∀ a ∈ B, g • a ∈ B → g • B = B

theorem MulAction.IsBlock.def_mem {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} (hB : MulAction.IsBlock G B) {a : X} {g : G} : a ∈ B → g • a ∈ B → g • B = B

theorem MulAction.IsBlock.mk_subset {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} : MulAction.IsBlock G B ↔ ∀ {g : G} {b : X}, b ∈ B → b ∈ g • B → g • B ⊆ B

theorem MulAction.IsInvariantBlock.isFixedBlock {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} (hfB : MulAction.IsInvariantBlock G B) : MulAction.IsFixedBlock G B

An invariant block is a fixed block

theorem MulAction.IsInvariantBlock.isBlock {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} (hfB : MulAction.IsInvariantBlock G B) : MulAction.IsBlock G B

An invariant block is a block

theorem MulAction.isFixedBlock_orbit {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (a : X) : MulAction.IsFixedBlock G (MulAction.orbit G a)

An orbit is a block

theorem MulAction.isBlock_orbit {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (a : X) : MulAction.IsBlock G (MulAction.orbit G a)

An orbit is a block

theorem MulAction.isFixedBlock_top {G : Type u_1} [Group G] (X : Type u_2) [MulAction G X] : MulAction.IsFixedBlock G ⊤

The full set is a (trivial) block

theorem MulAction.isBlock_top {G : Type u_1} [Group G] (X : Type u_2) [MulAction G X] : MulAction.IsBlock G ⊤

The full set is a (trivial) block

theorem MulAction.IsBlock.subgroup {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} {B : Set X} (hfB : MulAction.IsBlock G B) : MulAction.IsBlock (↥H) B

Is B is a block for an action G, it is a block for the action of any subgroup of G

theorem MulAction.IsBlock.preimage {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Type u_3} {Y : Type u_4} [Group H] [MulAction H Y] {φ : H → G} (j : Y →ₑ[φ] X) {B : Set X} (hB : MulAction.IsBlock G B) : MulAction.IsBlock H (⇑j ⁻¹' B)

theorem MulAction.IsBlock.image {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Type u_3} {Y : Type u_4} [Group H] [MulAction H Y] {φ : G →* H} (j : X →ₑ[⇑φ] Y) (hφ : Function.Surjective ⇑φ) (hj : Function.Injective ⇑j) {B : Set X} (hB : MulAction.IsBlock G B) : MulAction.IsBlock H (⇑j '' B)

theorem MulAction.IsBlock.subtype_val_preimage {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {C : SubMulAction G X} {B : Set X} (hB : MulAction.IsBlock G B) : MulAction.IsBlock G (Subtype.val ⁻¹' B)

theorem MulAction.IsBlock.iff_subtype_val {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {C : SubMulAction G X} {B : Set ↥C} : MulAction.IsBlock G B ↔ MulAction.IsBlock G (Subtype.val '' B)

theorem MulAction.IsBlock.iff_top {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (B : Set X) : MulAction.IsBlock G B ↔ MulAction.IsBlock (↥⊤) B

theorem MulAction.IsBlock.inter {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B₁ : Set X} {B₂ : Set X} (h₁ : MulAction.IsBlock G B₁) (h₂ : MulAction.IsBlock G B₂) : MulAction.IsBlock G (B₁ ∩ B₂)

The intersection of two blocks is a block

theorem MulAction.IsBlock.iInter {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {ι : Type u_3} {B : ι → Set X} (hB : ∀ (i : ι), MulAction.IsBlock G (B i)) : MulAction.IsBlock G (⋂ (i : ι), B i)

An intersection of blocks is a block

theorem MulAction.IsBlock.of_subgroup_of_conjugate {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} {H : Subgroup G} (hB : MulAction.IsBlock (↥H) B) (g : G) : MulAction.IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)

theorem MulAction.IsBlock.translate {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} (g : G) (hB : MulAction.IsBlock G B) : MulAction.IsBlock G (g • B)

A translate of a block is a block

def MulAction.IsBlockSystem (G : Type u_1) [Group G] {X : Type u_2} [MulAction G X] (B : Set (Set X)) : Prop

For SMul G X, a block system of X is a partition of X into blocks for the action of G

Equations

• MulAction.IsBlockSystem G B = (Setoid.IsPartition B ∧ ∀ b ∈ B, MulAction.IsBlock G b)

theorem MulAction.IsBlock.isBlockSystem {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [hGX : MulAction.IsPretransitive G X] {B : Set X} (hB : MulAction.IsBlock G B) (hBe : B.Nonempty) : MulAction.IsBlockSystem G (Set.range fun (g : G) => g • B)

Translates of a block form a block_system

theorem MulAction.smul_orbit_eq_orbit_smul {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (N : Subgroup G) [nN : N.Normal] (a : X) (g : G) : g • MulAction.orbit (↥N) a = MulAction.orbit (↥N) (g • a)

theorem MulAction.orbit.isBlock_of_normal {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {N : Subgroup G} [N.Normal] (a : X) : MulAction.IsBlock G (MulAction.orbit (↥N) a)

An orbit of a normal subgroup is a block

theorem MulAction.IsBlockSystem.of_normal {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {N : Subgroup G} [N.Normal] : MulAction.IsBlockSystem G (Set.range fun (a : X) => MulAction.orbit (↥N) a)

The orbits of a normal subgroup form a block system