Documentation

HexPermGroup.Product.WreathPerm

source
def Hex.Perm.Wreath.act {m n : Nat} (f : Fin m → Perm n) (h : Perm m) (x : Fin (n * m)) :
Fin (n * m)

The imprimitive action uses the base factor at the destination block: (f,h)(i,j) = (f(h(j))(i), h(j)).

Equations
Instances For
    source
    @[simp]
    theorem Hex.Perm.Wreath.act_index {m n : Nat} (f : Fin m → Perm n) (h : Perm m) (i : Fin n) (j : Fin m) :
    act f h (index i j) = index ((f (h.get j)).get i) (h.get j)
    source
    def Hex.Perm.Wreath.inverse {m n : Nat} (f : Fin m → Perm n) (h : Perm m) :
    Fin m → Perm n
    Equations
    Instances For
      source
      @[simp]
      theorem Hex.Perm.Wreath.inv_act {m n : Nat} (f : Fin m → Perm n) (h : Perm m) (x : Fin (n * m)) :
      act (inverse f h) h.inv (act f h x) = x
      source
      @[simp]
      theorem Hex.Perm.Wreath.act_inv {m n : Nat} (f : Fin m → Perm n) (h : Perm m) (x : Fin (n * m)) :
      act f h (act (inverse f h) h.inv x) = x
      source
      def Hex.Perm.Wreath.perm {m n : Nat} (f : Fin m → Perm n) (h : Perm m) :
      Perm (n * m)
      Equations
      Instances For
        source
        def Hex.Perm.Wreath.permImpl {m n : Nat} (f : Fin m → Perm n) (h : Perm m) :
        Perm (n * m)

        Cache each base permutation once before materializing the point action. In particular, identity base factors in copies and lifts are not rebuilt at every point of their block.

        Equations
        Instances For
          source
          @[csimp]
          theorem Hex.Perm.Wreath.perm_eq :
          @perm = @permImpl

          Native materialization caches the supplied base functions; kernel reduction retains the original point-action definition.

          source
          @[simp]
          theorem Hex.Perm.Wreath.perm_index {m n : Nat} (f : Fin m → Perm n) (h : Perm m) (i : Fin n) (j : Fin m) :
          (perm f h).get (index i j) = index ((f (h.get j)).get i) (h.get j)
          source
          @[simp]
          theorem Hex.Perm.Wreath.perm_id {m n : Nat} :
          perm (fun (x : Fin m) => Perm.id n) (Perm.id m) = Perm.id (n * m)
          source
          theorem Hex.Perm.Wreath.perm_comp {m n : Nat} (f g : Fin m → Perm n) (h k : Perm m) :
          (perm f h).comp (perm g k) = perm (fun (j : Fin m) => (f j).comp (g (h.inv.get j))) (h.comp k)

          Multiplication is (f,h)(g,k) = (j ↦ f(j)*g(h⁻¹(j)), h*k).

          source
          theorem Hex.Perm.Wreath.perm_inv {m n : Nat} (f : Fin m → Perm n) (h : Perm m) :
          (perm f h).inv = perm (inverse f h) h.inv
          source
          theorem Hex.Perm.Wreath.perm_injective {n m : Nat} (hn : 0 < n) {f g : Fin m → Perm n} {h k : Perm m} (he : perm f h = perm g k) :
          (∀ (j : Fin m), f j = g j) ∧ h = k

          Nonempty blocks are necessary for the top permutation to be recoverable. The base factors are then uniquely recoverable from the point action too.