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.

Results for actions on finite sets

• IsBlock.ncard_block_mul_ncard_orbit_eq : The cardinality of a block multiplied by the number of its translates is the cardinal of the ambient type

• IsBlock.eq_univ_of_card_lt : a too large block is equal to Set.univ

• IsBlock.subsingleton_of_card_lt : a too small block is a subsingleton

• IsBlock.of_subset : the intersections of the translates of a finite subset that contain a given point is a block

References

We follow [Wielandt-1964].

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

theorem AddAction.orbit.eq_or_disjoint {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] (a b : X) : AddAction.orbit G a = AddAction.orbit G b ∨ Disjoint (AddAction.orbit G a) (AddAction.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 AddAction.orbit.pairwiseDisjoint {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] : (Set.range fun (x : X) => AddAction.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

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

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

A set B is a G-fixed block if g • B = B for all g : G.

Equations

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

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

A set B is a G-fixed block if g +ᵥ B = B for all g : G.

Equations

• AddAction.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

A set B is a G-invariant block if g • B ⊆ B for all g : G.

Note: It is not necessarily a block when the action is not by a group.

Equations

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

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

A set B is a G-invariant block if g +ᵥ B ⊆ B for all g : G.

Note: It is not necessarily a block when the action is not by a group.

Equations

• AddAction.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 univ.

Note: It is not necessarily a block when the action is not by a group.

Equations

• MulAction.IsTrivialBlock B = (B.Subsingleton ∨ B = Set.univ)

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

A trivial block is a Set X which is either a subsingleton or univ.

Note: It is not necessarily a block when the action is not by a group.

Equations

• AddAction.IsTrivialBlock B = (B.Subsingleton ∨ B = Set.univ)

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

A set B is a G-block iff the sets of the form g • B are pairwise equal or disjoint.

Equations

• MulAction.IsBlock G B = ∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

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

A set B is a G-block iff the sets of the form g +ᵥ B are pairwise equal or disjoint.

Equations

• AddAction.IsBlock G B = ∀ ⦃g₁ g₂ : G⦄, g₁ +ᵥ B ≠ g₂ +ᵥ B → Disjoint (g₁ +ᵥ B) (g₂ +ᵥ B)

theorem MulAction.isBlock_iff_smul_eq_smul_of_nonempty {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).Nonempty → g₁ • B = g₂ • B

theorem AddAction.isBlock_iff_vadd_eq_vadd_of_nonempty {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} : AddAction.IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, ((g₁ +ᵥ B) ∩ (g₂ +ᵥ B)).Nonempty → g₁ +ᵥ B = g₂ +ᵥ B

theorem MulAction.isBlock_iff_pairwiseDisjoint_range_smul {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} : MulAction.IsBlock G B ↔ (Set.range fun (g : G) => g • B).PairwiseDisjoint id

theorem AddAction.isBlock_iff_pairwiseDisjoint_range_vadd {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} : AddAction.IsBlock G B ↔ (Set.range fun (g : G) => g +ᵥ B).PairwiseDisjoint id

theorem MulAction.isBlock_iff_smul_eq_smul_or_disjoint {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)

theorem AddAction.isBlock_iff_vadd_eq_vadd_or_disjoint {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} : AddAction.IsBlock G B ↔ ∀ (g₁ g₂ : G), g₁ +ᵥ B = g₂ +ᵥ B ∨ Disjoint (g₁ +ᵥ B) (g₂ +ᵥ B)

theorem MulAction.IsBlock.smul_eq_smul_of_nonempty {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).Nonempty → g₁ • B = g₂ • B

Alias of the forward direction of MulAction.isBlock_iff_smul_eq_smul_of_nonempty.

theorem MulAction.IsBlock.pairwiseDisjoint_range_smul {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} : MulAction.IsBlock G B → (Set.range fun (g : G) => g • B).PairwiseDisjoint id

Alias of the forward direction of MulAction.isBlock_iff_pairwiseDisjoint_range_smul.

theorem MulAction.IsBlock.smul_eq_smul_or_disjoint {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)

Alias of the forward direction of MulAction.isBlock_iff_smul_eq_smul_or_disjoint.

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 AddAction.IsFixedBlock.isBlock {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} (hfB : AddAction.IsFixedBlock G B) : AddAction.IsBlock G B

A fixed block is a block.

@[simp]

theorem MulAction.IsBlock.empty {G : Type u_1} {X : Type u_2} [SMul G X] : MulAction.IsBlock G ∅

The empty set is a block.

@[simp]

theorem AddAction.IsBlock.empty {G : Type u_1} {X : Type u_2} [VAdd G X] : AddAction.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}

A singleton is a block.

theorem AddAction.IsBlock.singleton {G : Type u_1} {X : Type u_2} [VAdd G X] {a : X} : AddAction.IsBlock G {a}

A singleton is a block.

theorem MulAction.IsBlock.of_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 AddAction.IsBlock.of_subsingleton {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} (hB : B.Subsingleton) : AddAction.IsBlock G B

Subsingletons are (trivial) blocks.

theorem MulAction.IsFixedBlock.isInvariantBlock {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} (hB : MulAction.IsFixedBlock G B) : MulAction.IsInvariantBlock G B

A fixed block is an invariant block.

theorem AddAction.IsFixedBlock.isInvariantBlock {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} (hB : AddAction.IsFixedBlock G B) : AddAction.IsInvariantBlock G B

A fixed block is an invariant block.

theorem MulAction.isBlock_iff_disjoint_smul_of_ne {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 AddAction.isBlock_iff_disjoint_vadd_of_ne {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B ↔ ∀ ⦃g : G⦄, g +ᵥ B ≠ B → Disjoint (g +ᵥ B) B

theorem MulAction.isBlock_iff_smul_eq_of_nonempty {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).Nonempty → g • B = B

theorem AddAction.isBlock_iff_vadd_eq_of_nonempty {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B ↔ ∀ ⦃g : G⦄, ((g +ᵥ B) ∩ B).Nonempty → g +ᵥ B = B

theorem MulAction.isBlock_iff_smul_eq_or_disjoint {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 AddAction.isBlock_iff_vadd_eq_or_disjoint {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B ↔ ∀ (g : G), g +ᵥ B = B ∨ Disjoint (g +ᵥ B) B

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

theorem AddAction.isBlock_iff_vadd_eq_of_mem {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g +ᵥ a ∈ B → g +ᵥ B = B

theorem MulAction.IsBlock.disjoint_smul_of_ne {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

Alias of the forward direction of MulAction.isBlock_iff_disjoint_smul_of_ne.

theorem AddAction.IsBlock.disjoint_vadd_of_ne {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B → ∀ ⦃g : G⦄, g +ᵥ B ≠ B → Disjoint (g +ᵥ B) B

theorem MulAction.IsBlock.smul_eq_of_nonempty {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).Nonempty → g • B = B

Alias of the forward direction of MulAction.isBlock_iff_smul_eq_of_nonempty.

theorem AddAction.IsBlock.vadd_eq_of_nonempty {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B → ∀ ⦃g : G⦄, ((g +ᵥ B) ∩ B).Nonempty → g +ᵥ B = B

theorem MulAction.IsBlock.smul_eq_or_disjoint {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

Alias of the forward direction of MulAction.isBlock_iff_smul_eq_or_disjoint.

theorem AddAction.IsBlock.vadd_eq_or_disjoint {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B → ∀ (g : G), g +ᵥ B = B ∨ Disjoint (g +ᵥ B) B

theorem MulAction.IsBlock.smul_eq_of_mem {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} : MulAction.IsBlock G B → ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B

Alias of the forward direction of MulAction.isBlock_iff_smul_eq_of_mem.

theorem AddAction.IsBlock.vadd_eq_of_mem {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock G B → ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g +ᵥ a ∈ B → g +ᵥ B = B

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

If B is a G-block, then it is also a H-block for any subgroup H of G.

theorem AddAction.IsBlock.addSubgroup {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} {H : AddSubgroup G} (hB : AddAction.IsBlock G B) : AddAction.IsBlock (↥H) B

If B is a G-block, then it is also a H-block for any subgroup H of G.

theorem MulAction.isInvariantBlock_iff_isFixedBlock {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} : MulAction.IsInvariantBlock G B ↔ MulAction.IsFixedBlock G B

A block of a group action is invariant iff it is fixed.

theorem AddAction.isInvariantBlock_iff_isFixedBlock {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsInvariantBlock G B ↔ AddAction.IsFixedBlock G B

A block of a group action is invariant iff it is fixed.

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

An invariant block of a group action is a fixed block.

theorem AddAction.IsInvariantBlock.isFixedBlock {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsInvariantBlock G B → AddAction.IsFixedBlock G B

An invariant block of a group action is a fixed block.

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

An invariant block of a group action is a block.

theorem AddAction.IsInvariantBlock.isBlock {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} (hB : AddAction.IsInvariantBlock G B) : AddAction.IsBlock G B

An invariant block of a group action is a block.

theorem MulAction.IsFixedBlock.univ {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] : MulAction.IsFixedBlock G Set.univ

The full set is a fixed block.

theorem AddAction.IsFixedBlock.univ {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] : AddAction.IsFixedBlock G Set.univ

The full set is a fixed block.

@[simp]

theorem MulAction.IsBlock.univ {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] : MulAction.IsBlock G Set.univ

The full set is a block.

@[simp]

theorem AddAction.IsBlock.univ {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] : AddAction.IsBlock G Set.univ

The full set is a block.

theorem MulAction.IsBlock.inter {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B₁ 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 AddAction.IsBlock.inter {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B₁ B₂ : Set X} (h₁ : AddAction.IsBlock G B₁) (h₂ : AddAction.IsBlock G B₂) : AddAction.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] {ι : Sort 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 AddAction.IsBlock.iInter {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {ι : Sort u_3} {B : ι → Set X} (hB : ∀ (i : ι), AddAction.IsBlock G (B i)) : AddAction.IsBlock G (⋂ (i : ι), B i)

An intersection of blocks is a block.

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

A trivial block is a block.

theorem AddAction.IsTrivialBlock.isBlock {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} (hB : AddAction.IsTrivialBlock B) : AddAction.IsBlock G B

A trivial 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 fixed block.

theorem AddAction.IsFixedBlock.orbit {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] (a : X) : AddAction.IsFixedBlock G (AddAction.orbit G a)

An orbit is a fixed 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 AddAction.IsBlock.orbit {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] (a : X) : AddAction.IsBlock G (AddAction.orbit G a)

An orbit is a block.

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

theorem AddAction.isBlock_top {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : AddAction.IsBlock (↥⊤) B ↔ AddAction.IsBlock G B

theorem MulAction.IsBlock.preimage {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4} [Group H] [MulAction H Y] {φ : H → G} (j : Y →ₑ[φ] 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] {B : Set 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) (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] {B : Set X} {C : SubMulAction G X} (hB : MulAction.IsBlock G B) : MulAction.IsBlock G (Subtype.val ⁻¹' B)

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

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] (ℬ : 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 ℬ = (Setoid.IsPartition ℬ ∧ ∀ ⦃B : Set X⦄, B ∈ ℬ → MulAction.IsBlock G B)

theorem MulAction.IsBlock.isBlockSystem {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} [hGX : MulAction.IsPretransitive G 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.IsBlock.orbit_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

Annoyingly, it seems like the following two lemmas cannot be unified.

theorem MulAction.isBlock_subgroup {G : Type u_1} [Group G] {S : Type u_3} {H : Type u_4} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} [MulAction G H] [IsScalarTower G H H] : MulAction.IsBlock G ↑s

See MulAction.isBlock_subgroup' for a version that works for the right action of a group on itself.

theorem AddAction.isBlock_addSubgroup {G : Type u_1} [AddGroup G] {S : Type u_3} {H : Type u_4} [AddGroup H] [SetLike S H] [AddSubgroupClass S H] {s : S} [AddAction G H] [VAddAssocClass G H H] : AddAction.IsBlock G ↑s

See AddAction.isBlock_subgroup' for a version that works for the right action of a group on itself.

theorem MulAction.isBlock_subgroup' {G : Type u_1} [Group G] {S : Type u_3} {H : Type u_4} [Group H] [SetLike S H] [SubgroupClass S H] {s : S} [MulAction G H] [IsScalarTower G Hᵐᵒᵖ H] : MulAction.IsBlock G ↑s

See MulAction.isBlock_subgroup for a version that works for the left action of a group on itself.

theorem AddAction.isBlock_addSubgroup' {G : Type u_1} [AddGroup G] {S : Type u_3} {H : Type u_4} [AddGroup H] [SetLike S H] [AddSubgroupClass S H] {s : S} [AddAction G H] [VAddAssocClass G Hᵃᵒᵖ H] : AddAction.IsBlock G ↑s

See AddAction.isBlock_subgroup for a version that works for the left action of a group on itself.

theorem MulAction.IsBlock.of_orbit {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {H : Subgroup G} {a : X} (hH : MulAction.stabilizer G a ≤ H) : MulAction.IsBlock G (MulAction.orbit (↥H) a)

The orbit of a under a subgroup containing the stabilizer of a is a block

theorem MulAction.IsBlock.stabilizer_le {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} (hB : MulAction.IsBlock G B) {a : X} (ha : a ∈ B) : MulAction.stabilizer G a ≤ MulAction.stabilizer G B

If B is a block containing a, then the stabilizer of B contains the stabilizer of a

theorem MulAction.IsBlock.orbit_stabilizer_eq {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} [MulAction.IsPretransitive G X] (hB : MulAction.IsBlock G B) {a : X} (ha : a ∈ B) : MulAction.orbit (↥(MulAction.stabilizer G B)) a = B

A block containing a is the orbit of a under its stabilizer

theorem MulAction.stabilizer_orbit_eq {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {a : X} {H : Subgroup G} (hH : MulAction.stabilizer G a ≤ H) : MulAction.stabilizer G (MulAction.orbit (↥H) a) = H

A subgroup containing the stabilizer of a is the stabilizer of the orbit of a under that subgroup

def MulAction.block_stabilizerOrderIso (G : Type u_1) [Group G] {X : Type u_2} [MulAction G X] [htGX : MulAction.IsPretransitive G X] (a : X) : { B : Set X // a ∈ B ∧ MulAction.IsBlock G B } ≃o ↑(Set.Ici (MulAction.stabilizer G a))

Order equivalence between blocks in X containing a point a and subgroups of G containing the stabilizer of a (Wielandt, th. 7.5)

Equations

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

theorem MulAction.IsBlock.ncard_block_eq_relindex {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [MulAction.IsPretransitive G X] {B : Set X} (hB : MulAction.IsBlock G B) {x : X} (hx : x ∈ B) : B.ncard = (MulAction.stabilizer G x).relindex (MulAction.stabilizer G B)

theorem MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [MulAction.IsPretransitive G X] {B : Set X} (hB : MulAction.IsBlock G B) (hB_ne : B.Nonempty) : B.ncard * (MulAction.orbit G B).ncard = Nat.card X

The cardinality of the ambient space is the product of the cardinality of a block by the cardinality of the set of translates of that block

theorem MulAction.IsBlock.ncard_dvd_card {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [MulAction.IsPretransitive G X] {B : Set X} (hB : MulAction.IsBlock G B) (hB_ne : B.Nonempty) : B.ncard ∣ Nat.card X

The cardinality of a block divides the cardinality of the ambient type

theorem MulAction.IsBlock.eq_univ_of_card_lt {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [MulAction.IsPretransitive G X] {B : Set X} [hX : Finite X] (hB : MulAction.IsBlock G B) (hB' : Nat.card X < B.ncard * 2) : B = Set.univ

A too large block is equal to univ

@[deprecated MulAction.IsBlock.eq_univ_of_card_lt]

theorem MulAction.IsBlock.eq_univ_card_lt {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [MulAction.IsPretransitive G X] {B : Set X} [hX : Finite X] (hB : MulAction.IsBlock G B) (hB' : Nat.card X < B.ncard * 2) : B = Set.univ

Alias of MulAction.IsBlock.eq_univ_of_card_lt.

---

A too large block is equal to univ

theorem MulAction.IsBlock.subsingleton_of_card_lt {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [MulAction.IsPretransitive G X] {B : Set X} [Finite X] (hB : MulAction.IsBlock G B) (hB' : Nat.card X < 2 * (MulAction.orbit G B).ncard) : B.Subsingleton

If a block has too many translates, then it is a (sub)singleton

theorem MulAction.IsBlock.of_subset {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [MulAction.IsPretransitive G X] {B : Set X} (a : X) (hfB : B.Finite) : MulAction.IsBlock G (⋂ (k : G), ⋂ (_ : a ∈ k • B), k • B)

The intersection of the translates of a finite subset which contain a given point is a block (Wielandt, th. 7.3 )