Documentation

Mathlib.GroupTheory.GroupAction.Blocks

Blocks #

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

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

References #

We follow [wieland1964].

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

Orbits of an element form a partition

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

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

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

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

    Equations
    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 ⊤ (it is not necessarily a block…)

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

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

        Equations
        Instances For
          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) :

          A fixed block is a block

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

          The empty set is a block

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

          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), aB, g a Bg 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 Bg a Bg 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 Bb g Bg B 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) :

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

          An orbit is a block

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

          An orbit is a block

          The full set is a (trivial) block

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

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

          Is B is a block for an action of 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] {φ : HG} (j : Y →ₑ[φ] X) {B : Set X} (hB : MulAction.IsBlock G 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) :
          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} :
          theorem MulAction.IsBlock.iff_top {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (B : Set X) :
          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) :

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

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

          Equations
          Instances For
            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) :

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

            The orbits of a normal subgroup form a block system

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

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

            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] [htGX : MulAction.IsPretransitive G X] {B : Set X} (hB : MulAction.IsBlock G B) {a : X} (ha : 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) :

            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