def Hex.PermGroup.Group.directProduct {n m : Nat} (G : Group n) (H : Group m) : Group (n + m)

Direct product on consecutive disjoint supports, retaining all fixed points and allowing either declared factor degree to be zero.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.Group.direct_left_mem {n m : Nat} (G : Group n) (H : Group m) (p : Perm n) (hp : Generated G.generators p) : Generated (G.directProduct H).generators (p.sum (Perm.id m))

theorem Hex.PermGroup.Group.direct_right_mem {n m : Nat} (G : Group n) (H : Group m) (q : Perm m) (hq : Generated H.generators q) : Generated (G.directProduct H).generators ((Perm.id n).sum q)

theorem Hex.PermGroup.Group.direct_sum_mem {n m : Nat} (G : Group n) (H : Group m) (p : Perm n) (q : Perm m) (hp : Generated G.generators p) (hq : Generated H.generators q) : Generated (G.directProduct H).generators (p.sum q)

theorem Hex.PermGroup.Group.mem_directProduct {n m : Nat} (G : Group n) (H : Group m) (r : Perm (n + m)) : Generated (G.directProduct H).generators r ↔ ∃ (p : Perm n), ∃ (q : Perm m), Generated G.generators p ∧ Generated H.generators q ∧ r = p.sum q

Every generated product element has a factor decomposition; the converse proves that the two embedded factor images generate the full output.

def Hex.PermGroup.DirectProduct.pair {n m : Nat} {G : Group n} {H : Group m} (p : Element G) (q : Element H) : Element (G.directProduct H)

The pair embedding is a bijection onto the constructed product group.

Equations

• Hex.PermGroup.DirectProduct.pair p q = ⟨p.val.sum q.val, ⋯⟩

theorem Hex.PermGroup.DirectProduct.factors {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.directProduct H)) : ∃ (p : Perm n), ∃ (q : Perm m), r.val = p.sum q

def Hex.PermGroup.DirectProduct.fst {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.directProduct H)) : Element G

Equations

• Hex.PermGroup.DirectProduct.fst r = ⟨Hex.Perm.Sum.left r.val ⋯, ⋯⟩

def Hex.PermGroup.DirectProduct.snd {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.directProduct H)) : Element H

Equations

• Hex.PermGroup.DirectProduct.snd r = ⟨Hex.Perm.Sum.right r.val ⋯, ⋯⟩

@[simp]

theorem Hex.PermGroup.DirectProduct.fst_pair {n m : Nat} {G : Group n} {H : Group m} (p : Element G) (q : Element H) : fst (pair p q) = p

@[simp]

theorem Hex.PermGroup.DirectProduct.snd_pair {n m : Nat} {G : Group n} {H : Group m} (p : Element G) (q : Element H) : snd (pair p q) = q

@[simp]

theorem Hex.PermGroup.DirectProduct.pair_factors {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.directProduct H)) : pair (fst r) (snd r) = r

theorem Hex.PermGroup.DirectProduct.pair_injective {n m : Nat} {G : Group n} {H : Group m} {p a : Element G} {q b : Element H} (h : pair p q = pair a b) : p = a ∧ q = b

theorem Hex.PermGroup.DirectProduct.pair_comp {n m : Nat} {G : Group n} {H : Group m} (p a : Element G) (q b : Element H) : pair (p.comp a) (q.comp b) = (pair p q).comp (pair a b)

@[simp]

theorem Hex.PermGroup.DirectProduct.pair_id {n m : Nat} {G : Group n} {H : Group m} : pair (Element.id G) (Element.id H) = Element.id (G.directProduct H)

theorem Hex.PermGroup.DirectProduct.fst_comp {n m : Nat} {G : Group n} {H : Group m} (r s : Element (G.directProduct H)) : fst (r.comp s) = (fst r).comp (fst s)

theorem Hex.PermGroup.DirectProduct.snd_comp {n m : Nat} {G : Group n} {H : Group m} (r s : Element (G.directProduct H)) : snd (r.comp s) = (snd r).comp (snd s)