Documentation

HexPermGroup.Product.Maps

source
def Hex.PermGroup.DirectProduct.inl {n m : Nat} {G : Group n} (H : Group m) (p : Element G) :
Element (G.directProduct H)
Equations
Instances For
    source
    def Hex.PermGroup.DirectProduct.inr {n m : Nat} {H : Group m} (G : Group n) (q : Element H) :
    Element (G.directProduct H)
    Equations
    Instances For
      source
      @[simp]
      theorem Hex.PermGroup.DirectProduct.fst_inl {n m : Nat} {G : Group n} {H : Group m} (p : Element G) :
      fst (inl H p) = p
      source
      @[simp]
      theorem Hex.PermGroup.DirectProduct.snd_inl {n m : Nat} {G : Group n} {H : Group m} (p : Element G) :
      snd (inl H p) = Element.id H
      source
      @[simp]
      theorem Hex.PermGroup.DirectProduct.fst_inr {n m : Nat} {G : Group n} {H : Group m} (q : Element H) :
      fst (inr G q) = Element.id G
      source
      @[simp]
      theorem Hex.PermGroup.DirectProduct.snd_inr {n m : Nat} {G : Group n} {H : Group m} (q : Element H) :
      snd (inr G q) = q
      source
      theorem Hex.PermGroup.DirectProduct.inl_injective {n m : Nat} {G : Group n} {H : Group m} {p q : Element G} (h : inl H p = inl H q) :
      p = q
      source
      theorem Hex.PermGroup.DirectProduct.inr_injective {n m : Nat} {G : Group n} {H : Group m} {p q : Element H} (h : inr G p = inr G q) :
      p = q
      source
      theorem Hex.PermGroup.DirectProduct.inl_comp {n m : Nat} {G : Group n} {H : Group m} (p q : Element G) :
      inl H (p.comp q) = (inl H p).comp (inl H q)
      source
      theorem Hex.PermGroup.DirectProduct.inr_comp {n m : Nat} {G : Group n} {H : Group m} (p q : Element H) :
      inr G (p.comp q) = (inr G p).comp (inr G q)
      source
      theorem Hex.PermGroup.DirectProduct.inl_inr {n m : Nat} {G : Group n} {H : Group m} (p : Element G) (q : Element H) :
      (inl H p).comp (inr G q) = pair p q
      source
      theorem Hex.PermGroup.DirectProduct.commute {n m : Nat} {G : Group n} {H : Group m} (p : Element G) (q : Element H) :
      (inl H p).comp (inr G q) = (inr G q).comp (inl H p)
      source
      theorem Hex.PermGroup.DirectProduct.intersection {n m : Nat} {G : Group n} {H : Group m} {p : Element G} {q : Element H} (h : inl H p = inr G q) :
      p = Element.id G ∧ q = Element.id H

      The two embedded factor images intersect only at the identity.

      source
      theorem Hex.PermGroup.DirectProduct.decomposition {n m : Nat} {G : Group n} {H : Group m} (r : Element (G.directProduct H)) :
      (inl H (fst r)).comp (inr G (snd r)) = r
      source
      theorem Hex.PermGroup.DirectProduct.unique {n m : Nat} {G : Group n} {H : Group m} {r : Element (G.directProduct H)} {p : Element G} {q : Element H} (h : (inl H p).comp (inr G q) = r) :
      p = fst r ∧ q = snd r