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. Under Group G and MulAction G X, this is equivalent to the classical definition MulAction.IsBlock.def_one

• 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 [Wie64].

theorem MulAction.orbit.eq_or_disjoint {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (a b : X) : orbit G a = orbit G b ∨ Disjoint (orbit G a) (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) : orbit G a = orbit G b ∨ Disjoint (orbit G a) (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) => 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) => 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) => 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) => orbit G a)

Orbits of an element of a partition

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} : 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} : 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} : 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} : 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} : 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} : IsBlock G B ↔ ∀ (g₁ g₂ : G), g₁ +ᵥ B = g₂ +ᵥ B ∨ Disjoint (g₁ +ᵥ B) (g₂ +ᵥ B)

theorem MulAction.IsBlock.smul_eq_smul_of_subset {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} {g₁ g₂ : G} (hB : IsBlock G B) (hg : g₁ • B ⊆ g₂ • B) : g₁ • B = g₂ • B

theorem AddAction.IsBlock.vadd_eq_vadd_of_subset {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} {g₁ g₂ : G} (hB : IsBlock G B) (hg : g₁ +ᵥ B ⊆ g₂ +ᵥ B) : g₁ +ᵥ B = g₂ +ᵥ B

theorem MulAction.IsBlock.not_smul_set_ssubset_smul_set {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} {g₁ g₂ : G} (hB : IsBlock G B) : ¬g₁ • B ⊂ g₂ • B

theorem AddAction.IsBlock.not_vadd_set_ssubset_vadd_set {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} {g₁ g₂ : G} (hB : IsBlock G B) : ¬g₁ +ᵥ B ⊂ g₂ +ᵥ B

theorem MulAction.IsBlock.disjoint_smul_set_smul {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} {s : Set G} {g : G} (hB : IsBlock G B) (hgs : ¬g • B ⊆ s • B) : Disjoint (g • B) (s • B)

theorem AddAction.IsBlock.disjoint_vadd_set_vadd {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} {s : Set G} {g : G} (hB : IsBlock G B) (hgs : ¬g +ᵥ B ⊆ s +ᵥ B) : Disjoint (g +ᵥ B) (s +ᵥ B)

theorem MulAction.IsBlock.disjoint_smul_smul_set {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} {s : Set G} {g : G} (hB : IsBlock G B) (hgs : ¬g • B ⊆ s • B) : Disjoint (s • B) (g • B)

theorem AddAction.IsBlock.disjoint_vadd_vadd_set {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} {s : Set G} {g : G} (hB : IsBlock G B) (hgs : ¬g +ᵥ B ⊆ s +ᵥ B) : Disjoint (s +ᵥ 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} : 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 AddAction.IsBlock.vadd_eq_vadd_of_nonempty {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} : IsBlock G B → ∀ ⦃g₁ g₂ : G⦄, ((g₁ +ᵥ B) ∩ (g₂ +ᵥ B)).Nonempty → g₁ +ᵥ B = g₂ +ᵥ B

theorem MulAction.IsBlock.pairwiseDisjoint_range_smul {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} : 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 AddAction.IsBlock.pairwiseDisjoint_range_vadd {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} : IsBlock G B → (Set.range fun (g : G) => g +ᵥ B).PairwiseDisjoint id

theorem MulAction.IsBlock.smul_eq_smul_or_disjoint {G : Type u_1} {X : Type u_2} [SMul G X] {B : Set X} : 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 AddAction.IsBlock.vadd_eq_vadd_or_disjoint {G : Type u_1} {X : Type u_2} [VAdd G X] {B : Set X} : IsBlock G B → ∀ (g₁ g₂ : G), g₁ +ᵥ B = g₂ +ᵥ B ∨ Disjoint (g₁ +ᵥ B) (g₂ +ᵥ B)

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

The empty set is a block.

@[simp]

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

A fixed block is an invariant block.

theorem MulAction.IsBlock.disjoint_smul_right {M : Type u_1} {X : Type u_2} [Monoid M] [MulAction M X] {B : Set X} {s : Set M} (hB : IsBlock M B) (hs : ¬B ⊆ s • B) : Disjoint B (s • B)

theorem AddAction.IsBlock.disjoint_vadd_right {M : Type u_1} {X : Type u_2} [AddMonoid M] [AddAction M X] {B : Set X} {s : Set M} (hB : IsBlock M B) (hs : ¬B ⊆ s +ᵥ B) : Disjoint B (s +ᵥ B)

theorem MulAction.IsBlock.disjoint_smul_left {M : Type u_1} {X : Type u_2} [Monoid M] [MulAction M X] {B : Set X} {s : Set M} (hB : IsBlock M B) (hs : ¬B ⊆ s • B) : Disjoint (s • B) B

theorem AddAction.IsBlock.disjoint_vadd_left {M : Type u_1} {X : Type u_2} [AddMonoid M] [AddAction M X] {B : Set X} {s : Set M} (hB : IsBlock M B) (hs : ¬B ⊆ s +ᵥ B) : Disjoint (s +ᵥ B) B

theorem MulAction.isBlock_iff_disjoint_smul_of_ne {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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} : 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 : IsBlock G B) : 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 : IsBlock G B) : 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} : IsInvariantBlock G B ↔ 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} : IsInvariantBlock G B ↔ 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} : IsInvariantBlock G B → 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} : IsInvariantBlock G B → 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 : IsInvariantBlock G B) : 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 : IsInvariantBlock G B) : 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] : 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] : 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] : 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] : 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₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) : 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₁ : IsBlock G B₁) (h₂ : IsBlock G B₂) : 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 : ι), IsBlock G (B i)) : 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 : ι), IsBlock G (B i)) : 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 : IsTrivialBlock B) : 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 : IsTrivialBlock B) : 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) : IsFixedBlock G (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) : IsFixedBlock G (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) : IsBlock G (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) : IsBlock G (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} : IsBlock (↥⊤) B ↔ IsBlock G B

theorem AddAction.isBlock_top {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} : IsBlock (↥⊤) B ↔ 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 : IsBlock G B) : IsBlock H (⇑j ⁻¹' B)

theorem AddAction.IsBlock.preimage {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4} [AddGroup H] [AddAction H Y] {φ : H → G} (j : Y →ₑ[φ] X) (hB : IsBlock G B) : 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 : IsBlock G B) : IsBlock H (⇑j '' B)

theorem AddAction.IsBlock.image {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4} [AddGroup H] [AddAction H Y] {φ : G →+ H} (j : X →ₑ[⇑φ] Y) (hφ : Function.Surjective ⇑φ) (hj : Function.Injective ⇑j) (hB : IsBlock G B) : 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 : IsBlock G B) : IsBlock G (Subtype.val ⁻¹' B)

theorem AddAction.IsBlock.subtype_val_preimage {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} {C : SubAddAction G X} (hB : IsBlock G B) : 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} : IsBlock G (Subtype.val '' B) ↔ IsBlock G B

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

theorem AddAction.IsBlock.of_addSubgroup_of_conjugate {G : Type u_3} [AddGroup G] {X : Type u_4} [AddAction G X] {B : Set X} {H : AddSubgroup G} (hB : IsBlock (↥H) B) (g : G) : IsBlock (↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) H)) (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 : IsBlock (↥H) B) (g : G) : IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)

theorem AddAction.IsBlock.translate {G : Type u_3} [AddGroup G] {X : Type u_4} [AddAction G X] (B : Set X) (g : G) (hB : IsBlock G B) : IsBlock G (g +ᵥ B)

A translate of a block is a block

theorem MulAction.IsBlock.translate {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} (g : G) (hB : IsBlock G B) : 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)

def AddAction.IsBlockSystem (G : Type u_1) [AddGroup G] {X : Type u_2} [AddAction G X] (ℬ : Set (Set X)) : Prop

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

Equations

• AddAction.IsBlockSystem G ℬ = (Setoid.IsPartition ℬ ∧ ∀ ⦃B : Set X⦄, B ∈ ℬ → AddAction.IsBlock G B)

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

Translates of a block form a block system

theorem AddAction.IsBlock.isBlockSystem {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} [hGX : IsPretransitive G X] (hB : IsBlock G B) (hBe : B.Nonempty) : 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 • orbit (↥N) a = orbit (↥N) (g • a)

theorem AddAction.vadd_orbit_eq_orbit_vadd {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] (N : AddSubgroup G) [nN : N.Normal] (a : X) (g : G) : g +ᵥ orbit (↥N) a = 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) : IsBlock G (orbit (↥N) a)

An orbit of a normal subgroup is a block

theorem AddAction.IsBlock.orbit_of_normal {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {N : AddSubgroup G} [N.Normal] (a : X) : IsBlock G (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] : IsBlockSystem G (Set.range fun (a : X) => orbit (↥N) a)

The orbits of a normal subgroup form a block system

theorem AddAction.IsBlockSystem.of_normal {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {N : AddSubgroup G} [N.Normal] : IsBlockSystem G (Set.range fun (a : X) => 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] : 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] : 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] : 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] : 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 : stabilizer G a ≤ H) : IsBlock G (orbit (↥H) a)

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

theorem AddAction.IsBlock.of_orbit {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {H : AddSubgroup G} {a : X} (hH : stabilizer G a ≤ H) : IsBlock G (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 : IsBlock G B) {a : X} (ha : a ∈ B) : stabilizer G a ≤ stabilizer G B

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

theorem AddAction.IsBlock.stabilizer_le {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} (hB : IsBlock G B) {a : X} (ha : a ∈ B) : stabilizer G a ≤ 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} [IsPretransitive G X] (hB : IsBlock G B) {a : X} (ha : a ∈ B) : orbit (↥(stabilizer G B)) a = B

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

theorem AddAction.IsBlock.orbit_stabilizer_eq {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} [IsPretransitive G X] (hB : IsBlock G B) {a : X} (ha : a ∈ B) : orbit (↥(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 : stabilizer G a ≤ H) : stabilizer G (orbit (↥H) a) = H

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

theorem AddAction.stabilizer_orbit_eq {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {a : X} {H : AddSubgroup G} (hH : stabilizer G a ≤ H) : stabilizer G (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 : IsPretransitive G X] (a : X) : { B : Set X // a ∈ B ∧ IsBlock G B } ≃o ↑(Set.Ici (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.

def AddAction.block_stabilizerOrderIso (G : Type u_1) [AddGroup G] {X : Type u_2} [AddAction G X] [htGX : IsPretransitive G X] (a : X) : { B : Set X // a ∈ B ∧ IsBlock G B } ≃o ↑(Set.Ici (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] [IsPretransitive G X] {B : Set X} (hB : IsBlock G B) {x : X} (hx : x ∈ B) : B.ncard = (stabilizer G x).relindex (stabilizer G B)

theorem AddAction.IsBlock.ncard_block_eq_relindex {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] [IsPretransitive G X] {B : Set X} (hB : IsBlock G B) {x : X} (hx : x ∈ B) : B.ncard = (stabilizer G x).relindex (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] [IsPretransitive G X] {B : Set X} (hB : IsBlock G B) (hB_ne : B.Nonempty) : B.ncard * (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 AddAction.IsBlock.ncard_block_add_ncard_orbit_eq {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] [IsPretransitive G X] {B : Set X} (hB : IsBlock G B) (hB_ne : B.Nonempty) : B.ncard * (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] [IsPretransitive G X] {B : Set X} (hB : 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 AddAction.IsBlock.ncard_dvd_card {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] [IsPretransitive G X] {B : Set X} (hB : 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] [IsPretransitive G X] {B : Set X} [hX : Finite X] (hB : IsBlock G B) (hB' : Nat.card X < B.ncard * 2) : B = Set.univ

A too large block is equal to univ

theorem AddAction.IsBlock.eq_univ_of_card_lt {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] [IsPretransitive G X] {B : Set X} [hX : Finite X] (hB : 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 (since := "2024-10-29")]

theorem MulAction.IsBlock.eq_univ_card_lt {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] [IsPretransitive G X] {B : Set X} [hX : Finite X] (hB : 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] [IsPretransitive G X] {B : Set X} [Finite X] (hB : IsBlock G B) (hB' : Nat.card X < 2 * (orbit G B).ncard) : B.Subsingleton

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

theorem AddAction.IsBlock.subsingleton_of_card_lt {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] [IsPretransitive G X] {B : Set X} [Finite X] (hB : IsBlock G B) (hB' : Nat.card X < 2 * (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] [IsPretransitive G X] {B : Set X} (a : X) (hfB : B.Finite) : 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)

theorem AddAction.IsBlock.of_subset {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] [IsPretransitive G X] {B : Set X} (a : X) (hfB : B.Finite) : 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)