Documentation

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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)

Instances For

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

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)

Instances For

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

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)

Instances For

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

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)

Instances For

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) :

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) :

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) :

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) :

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) :

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) :

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₁ : 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 AddAction.IsBlock.inter {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B₁ : Set X} {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) :

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) :

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)) :

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)

Instances For

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.

Instances For

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