Documentation

HexPermGroup.Product.Projection

source
def Hex.Perm.Sum.leftPoint {n m : Nat} (r : Perm (n + m)) (h : ∃ (p : Perm n), ∃ (q : Perm m), r = p.sum q) (i : Fin n) :
Fin n

Restrict to the first consecutive support. The existence proof supplies only bounds; the executable map reads the original permutation array.

Equations
Instances For
    source
    def Hex.Perm.Sum.rightPoint {n m : Nat} (r : Perm (n + m)) (h : ∃ (p : Perm n), ∃ (q : Perm m), r = p.sum q) (i : Fin m) :
    Fin m

    Restrict to the second support and remove its declared offset.

    Equations
    Instances For
      source
      @[simp]
      theorem Hex.Perm.Sum.leftPoint_sum {n m : Nat} (p : Perm n) (q : Perm m) (h : ∃ (p_1 : Perm n), ∃ (q_1 : Perm m), p.sum q = p_1.sum q_1) (i : Fin n) :
      leftPoint (p.sum q) h i = p.get i
      source
      @[simp]
      theorem Hex.Perm.Sum.rightPoint_sum {n m : Nat} (p : Perm n) (q : Perm m) (h : ∃ (p_1 : Perm n), ∃ (q_1 : Perm m), p.sum q = p_1.sum q_1) (i : Fin m) :
      rightPoint (p.sum q) h i = q.get i
      source
      def Hex.Perm.Sum.left {n m : Nat} (r : Perm (n + m)) (h : ∃ (p : Perm n), ∃ (q : Perm m), r = p.sum q) :
      Perm n
      Equations
      Instances For
        source
        def Hex.Perm.Sum.right {n m : Nat} (r : Perm (n + m)) (h : ∃ (p : Perm n), ∃ (q : Perm m), r = p.sum q) :
        Perm m
        Equations
        Instances For
          source
          @[simp]
          theorem Hex.Perm.Sum.left_sum {n m : Nat} (p : Perm n) (q : Perm m) (h : ∃ (p_1 : Perm n), ∃ (q_1 : Perm m), p.sum q = p_1.sum q_1) :
          left (p.sum q) h = p
          source
          @[simp]
          theorem Hex.Perm.Sum.right_sum {n m : Nat} (p : Perm n) (q : Perm m) (h : ∃ (p_1 : Perm n), ∃ (q_1 : Perm m), p.sum q = p_1.sum q_1) :
          right (p.sum q) h = q
          source
          theorem Hex.Perm.Sum.reconstruct {n m : Nat} (r : Perm (n + m)) (h : ∃ (p : Perm n), ∃ (q : Perm m), r = p.sum q) :
          (left r h).sum (right r h) = r