Documentation

Mathlib.GroupTheory.PushoutI

Pushouts of Monoids and Groups #

This file defines wide pushouts of monoids and groups and proves some properties of the amalgamated product of groups (i.e. the special case where all the maps in the diagram are injective).

Main definitions #

References #

Tags #

amalgamated product, pushout, group

def Monoid.PushoutI.con {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) :

The relation we quotient by to form the pushout

Equations
Instances For
    def Monoid.PushoutI {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) :
    Type (max (max u_1 u_2) u_3)

    The indexed pushout of monoids, which is the pushout in the category of monoids, or the category of groups.

    Equations
    Instances For
      instance Monoid.PushoutI.mul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} :
      Equations
      • Monoid.PushoutI.mul = id inferInstance
      instance Monoid.PushoutI.one {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} :
      Equations
      • Monoid.PushoutI.one = id inferInstance
      instance Monoid.PushoutI.monoid {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} :
      Equations
      • Monoid.PushoutI.monoid = Monoid.mk Monoid.npow
      def Monoid.PushoutI.of {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (i : ι) :

      The map from each indexing group into the pushout

      Equations
      Instances For
        def Monoid.PushoutI.base {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) :

        The map from the base monoid into the pushout

        Equations
        Instances For
          theorem Monoid.PushoutI.of_comp_eq_base {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (i : ι) :
          theorem Monoid.PushoutI.of_apply_eq_base {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] (φ : (i : ι) → H →* G i) (i : ι) (x : H) :
          def Monoid.PushoutI.lift {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), (f i).comp (φ i) = k) :

          Define a homomorphism out of the pushout of monoids be defining it on each object in the diagram

          Equations
          Instances For
            @[simp]
            theorem Monoid.PushoutI.lift_of {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), (f i).comp (φ i) = k) {i : ι} (g : G i) :
            (Monoid.PushoutI.lift f k hf) ((Monoid.PushoutI.of i) g) = (f i) g
            @[simp]
            theorem Monoid.PushoutI.lift_base {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K) (hf : ∀ (i : ι), (f i).comp (φ i) = k) (g : H) :
            theorem Monoid.PushoutI.hom_ext_iff {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} {f : Monoid.PushoutI φ →* K} {g : Monoid.PushoutI φ →* K} :
            f = g (∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) f.comp (Monoid.PushoutI.base φ) = g.comp (Monoid.PushoutI.base φ)
            theorem Monoid.PushoutI.hom_ext {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} {f : Monoid.PushoutI φ →* K} {g : Monoid.PushoutI φ →* K} (h : ∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) (hbase : f.comp (Monoid.PushoutI.base φ) = g.comp (Monoid.PushoutI.base φ)) :
            f = g
            theorem Monoid.PushoutI.hom_ext_nonempty_iff {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} [hn : Nonempty ι] {f : Monoid.PushoutI φ →* K} {g : Monoid.PushoutI φ →* K} :
            f = g ∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)
            theorem Monoid.PushoutI.hom_ext_nonempty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} [hn : Nonempty ι] {f : Monoid.PushoutI φ →* K} {g : Monoid.PushoutI φ →* K} (h : ∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) :
            f = g
            @[simp]
            theorem Monoid.PushoutI.homEquiv_apply_coe {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : Monoid.PushoutI φ →* K) :
            (Monoid.PushoutI.homEquiv f) = (fun (i : ι) => f.comp (Monoid.PushoutI.of i), f.comp (Monoid.PushoutI.base φ))
            @[simp]
            theorem Monoid.PushoutI.homEquiv_symm_apply {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (f : { f : ((i : ι) → G i →* K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }) :
            Monoid.PushoutI.homEquiv.symm f = Monoid.PushoutI.lift (↑f).1 (↑f).2
            def Monoid.PushoutI.homEquiv {ι : Type u_1} {G : ιType u_2} {H : Type u_3} {K : Type u_4} [Monoid K] [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} :
            (Monoid.PushoutI φ →* K) { f : ((i : ι) → G i →* K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }

            The equivalence that is part of the universal property of the pushout. A hom out of the pushout is just a morphism out of all groups in the pushout that satisfies a commutativity condition.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Monoid.PushoutI.ofCoprodI {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} :

              The map from the coproduct into the pushout

              Equations
              • Monoid.PushoutI.ofCoprodI = Monoid.CoprodI.lift Monoid.PushoutI.of
              Instances For
                @[simp]
                theorem Monoid.PushoutI.ofCoprodI_of {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} (i : ι) (g : G i) :
                Monoid.PushoutI.ofCoprodI (Monoid.CoprodI.of g) = (Monoid.PushoutI.of i) g
                theorem Monoid.PushoutI.induction_on {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Monoid (G i)] [Monoid H] {φ : (i : ι) → H →* G i} {motive : Monoid.PushoutI φProp} (x : Monoid.PushoutI φ) (of : ∀ (i : ι) (g : G i), motive ((Monoid.PushoutI.of i) g)) (base : ∀ (h : H), motive ((Monoid.PushoutI.base φ) h)) (mul : ∀ (x y : Monoid.PushoutI φ), motive xmotive ymotive (x * y)) :
                motive x
                instance Monoid.PushoutI.instGroup {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} :
                Equations
                structure Monoid.PushoutI.NormalWord.Transversal {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] (φ : (i : ι) → H →* G i) :
                Type (max u_1 u_2)

                The data we need to pick a normal form for words in the pushout. We need to pick a canonical element of each coset. We also need all the maps in the diagram to be injective

                • injective : ∀ (i : ι), Function.Injective (φ i)

                  All maps in the diagram are injective

                • set : (i : ι) → Set (G i)

                  The underlying set, containing exactly one element of each coset of the base group

                • one_mem : ∀ (i : ι), 1 self.set i

                  The chosen element of the base group itself is the identity

                • compl : ∀ (i : ι), Subgroup.IsComplement (↑(φ i).range) (self.set i)

                  We have exactly one element of each coset of the base group

                Instances For
                  theorem Monoid.PushoutI.NormalWord.Transversal.injective {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι) :

                  All maps in the diagram are injective

                  theorem Monoid.PushoutI.NormalWord.Transversal.one_mem {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι) :
                  1 self.set i

                  The chosen element of the base group itself is the identity

                  theorem Monoid.PushoutI.NormalWord.Transversal.compl {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι) :
                  Subgroup.IsComplement (↑(φ i).range) (self.set i)

                  We have exactly one element of each coset of the base group

                  theorem Monoid.PushoutI.NormalWord.transversal_nonempty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] (φ : (i : ι) → H →* G i) (hφ : ∀ (i : ι), Function.Injective (φ i)) :
                  structure Monoid.PushoutI.NormalWord {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (d : Monoid.PushoutI.NormalWord.Transversal φ) extends Monoid.CoprodI.Word :
                  Type (max (max u_1 u_2) u_3)

                  The normal form for words in the pushout. Every element of the pushout is the product of an element of the base group and a word made up of letters each of which is in the transversal.

                  • toList : List ((i : ι) × G i)
                  • ne_one : lself.toList, l.snd 1
                  • chain_ne : List.Chain' (fun (l l' : (i : ι) × G i) => l.fst l'.fst) self.toList
                  • head : H

                    Every NormalWord is the product of an element of the base group and a word made up of letters each of which is in the transversal. head is that element of the base group.

                  • normalized : ∀ (i : ι) (g : G i), i, g self.toListg d.set i

                    All letter in the word are in the transversal.

                  Instances For
                    theorem Monoid.PushoutI.NormalWord.normalized {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (self : Monoid.PushoutI.NormalWord d) (i : ι) (g : G i) :
                    i, g self.toListg d.set i

                    All letter in the word are in the transversal.

                    structure Monoid.PushoutI.NormalWord.Pair {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (d : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι) extends Monoid.CoprodI.Word.Pair :
                    Type (max u_1 u_2)

                    A Pair d i is a word in the coproduct, Coprod G, the tail, and an element of the group G i, the head. The first letter of the tail must not be an element of G i. Note that the head may be 1 Every letter in the tail must be in the transversal given by d. Similar to Monoid.CoprodI.Pair except every letter must be in the transversal (not including the head letter).

                    • head : G i
                    • fstIdx_ne : self.tail.fstIdx some i
                    • normalized : ∀ (i_1 : ι) (g : G i_1), i_1, g self.tail.toListg d.set i_1

                      All letters in the word are in the transversal.

                    Instances For
                      theorem Monoid.PushoutI.NormalWord.Pair.normalized {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (self : Monoid.PushoutI.NormalWord.Pair d i✝) (i : ι) (g : G i) :
                      i, g self.tail.toListg d.set i

                      All letters in the word are in the transversal.

                      @[simp]
                      theorem Monoid.PushoutI.NormalWord.empty_toList {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :
                      Monoid.PushoutI.NormalWord.empty.toList = []
                      @[simp]
                      theorem Monoid.PushoutI.NormalWord.empty_head {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :
                      Monoid.PushoutI.NormalWord.empty.head = 1
                      def Monoid.PushoutI.NormalWord.empty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :

                      The empty normalized word, representing the identity element of the group.

                      Equations
                      • Monoid.PushoutI.NormalWord.empty = { toWord := Monoid.CoprodI.Word.empty, head := 1, normalized := }
                      Instances For
                        instance Monoid.PushoutI.NormalWord.instInhabited {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :
                        Equations
                        • Monoid.PushoutI.NormalWord.instInhabited = { default := Monoid.PushoutI.NormalWord.empty }
                        instance Monoid.PushoutI.NormalWord.instInhabitedPair {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (i : ι) :
                        Equations
                        theorem Monoid.PushoutI.NormalWord.ext_iff {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {w₁ : Monoid.PushoutI.NormalWord d} {w₂ : Monoid.PushoutI.NormalWord d} :
                        w₁ = w₂ w₁.head = w₂.head w₁.toList = w₂.toList
                        theorem Monoid.PushoutI.NormalWord.ext {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {w₁ : Monoid.PushoutI.NormalWord d} {w₂ : Monoid.PushoutI.NormalWord d} (hhead : w₁.head = w₂.head) (hlist : w₁.toList = w₂.toList) :
                        w₁ = w₂
                        instance Monoid.PushoutI.NormalWord.baseAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :
                        Equations
                        theorem Monoid.PushoutI.NormalWord.base_smul_def' {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (h : H) (w : Monoid.PushoutI.NormalWord d) :
                        h w = { toWord := w.toWord, head := h * w.head, normalized := }
                        def Monoid.PushoutI.NormalWord.prod {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (w : Monoid.PushoutI.NormalWord d) :

                        Take the product of a normal word as an element of the PushoutI. We show that this is bijective, in NormalWord.equiv.

                        Equations
                        Instances For
                          @[simp]
                          theorem Monoid.PushoutI.NormalWord.prod_base_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (h : H) (w : Monoid.PushoutI.NormalWord d) :
                          (h w).prod = (Monoid.PushoutI.base φ) h * w.prod
                          @[simp]
                          theorem Monoid.PushoutI.NormalWord.prod_empty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :
                          Monoid.PushoutI.NormalWord.empty.prod = 1
                          @[simp]
                          theorem Monoid.PushoutI.NormalWord.cons_head {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx some i) (hgr : g(φ i).range) :
                          (Monoid.PushoutI.NormalWord.cons g w hmw hgr).head = (MonoidHom.ofInjective ).symm (.equiv (g * (φ i) w.head)).1
                          @[simp]
                          theorem Monoid.PushoutI.NormalWord.cons_toList {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx some i) (hgr : g(φ i).range) :
                          (Monoid.PushoutI.NormalWord.cons g w hmw hgr).toList = i, (.equiv (g * (φ i) w.head)).2 :: w.toList
                          noncomputable def Monoid.PushoutI.NormalWord.cons {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx some i) (hgr : g(φ i).range) :

                          A constructor that multiplies a NormalWord by an element, with condition to make sure the underlying list does get longer.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem Monoid.PushoutI.NormalWord.prod_cons {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx some i) (hgr : g(φ i).range) :
                            (Monoid.PushoutI.NormalWord.cons g w hmw hgr).prod = (Monoid.PushoutI.of i) g * w.prod
                            theorem Monoid.PushoutI.NormalWord.eq_one_of_smul_normalized {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (w : Monoid.CoprodI.Word G) {i : ι} (h : H) (hw : ∀ (i : ι) (g : G i), i, g w.toListg d.set i) (hφw : ∀ (j : ι) (g : G j), j, g (Monoid.CoprodI.of ((φ i) h) w).toListg d.set j) :
                            h = 1

                            Given a word in CoprodI, if every letter is in the transversal and when we multiply by an element of the base group it still has this property, then the element of the base group we multiplied by was one.

                            theorem Monoid.PushoutI.NormalWord.ext_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {w₁ : Monoid.PushoutI.NormalWord d} {w₂ : Monoid.PushoutI.NormalWord d} (i : ι) (h : Monoid.CoprodI.of ((φ i) w₁.head) w₁.toWord = Monoid.CoprodI.of ((φ i) w₂.head) w₂.toWord) :
                            w₁ = w₂
                            noncomputable def Monoid.PushoutI.NormalWord.rcons {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) (p : Monoid.PushoutI.NormalWord.Pair d i) :

                            Given a pair (head, tail), we can form a word by prepending head to tail, but putting head into normal form first, by making sure it is expressed as an element of the base group multiplied by an element of the transversal.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Monoid.PushoutI.NormalWord.rcons_injective {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} :
                              noncomputable def Monoid.PushoutI.NormalWord.equivPair {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) :

                              The equivalence between NormalWords and pairs. We can turn a NormalWord into a pair by taking the head of the List if it is in G i and multiplying it by the element of the base group.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                noncomputable instance Monoid.PushoutI.NormalWord.summandAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) :
                                Equations
                                theorem Monoid.PushoutI.NormalWord.summand_smul_def' {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) :
                                g w = (Monoid.PushoutI.NormalWord.equivPair i).symm (let __src := (Monoid.PushoutI.NormalWord.equivPair i) w; { head := g * ((Monoid.PushoutI.NormalWord.equivPair i) w).head, tail := __src.tail, fstIdx_ne := , normalized := })
                                noncomputable instance Monoid.PushoutI.NormalWord.mulAction {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] :
                                Equations
                                theorem Monoid.PushoutI.NormalWord.base_smul_def {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (h : H) (w : Monoid.PushoutI.NormalWord d) :
                                (Monoid.PushoutI.base φ) h w = { toWord := w.toWord, head := h * w.head, normalized := }
                                theorem Monoid.PushoutI.NormalWord.summand_smul_def {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) :
                                (Monoid.PushoutI.of i) g w = (Monoid.PushoutI.NormalWord.equivPair i).symm (let __src := (Monoid.PushoutI.NormalWord.equivPair i) w; { head := g * ((Monoid.PushoutI.NormalWord.equivPair i) w).head, tail := __src.tail, fstIdx_ne := , normalized := })
                                theorem Monoid.PushoutI.NormalWord.of_smul_eq_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) :
                                theorem Monoid.PushoutI.NormalWord.base_smul_eq_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (h : H) (w : Monoid.PushoutI.NormalWord d) :
                                noncomputable def Monoid.PushoutI.NormalWord.consRecOn {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {motive : Monoid.PushoutI.NormalWord dSort u_5} (w : Monoid.PushoutI.NormalWord d) (h_empty : motive Monoid.PushoutI.NormalWord.empty) (h_cons : (i : ι) → (g : G i) → (w : Monoid.PushoutI.NormalWord d) → (hmw : w.fstIdx some i) → g d.set i(hgr : g(φ i).range) → w.head = 1motive wmotive (Monoid.PushoutI.NormalWord.cons g w hmw hgr)) (h_base : (h : H) → (w : Monoid.PushoutI.NormalWord d) → w.head = 1motive wmotive ((Monoid.PushoutI.base φ) h w)) :
                                motive w

                                Induction principle for NormalWord, that corresponds closely to inducting on the underlying list.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem Monoid.PushoutI.NormalWord.cons_eq_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx some i) (hgr : g(φ i).range) :
                                  @[simp]
                                  theorem Monoid.PushoutI.NormalWord.prod_summand_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] {i : ι} (g : G i) (w : Monoid.PushoutI.NormalWord d) :
                                  (g w).prod = (Monoid.PushoutI.of i) g * w.prod
                                  @[simp]
                                  theorem Monoid.PushoutI.NormalWord.prod_smul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (g : Monoid.PushoutI φ) (w : Monoid.PushoutI.NormalWord d) :
                                  (g w).prod = g * w.prod
                                  theorem Monoid.PushoutI.NormalWord.prod_smul_empty {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (w : Monoid.PushoutI.NormalWord d) :
                                  w.prod Monoid.PushoutI.NormalWord.empty = w
                                  noncomputable def Monoid.PushoutI.NormalWord.equiv {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] :

                                  The equivalence between normal forms and elements of the pushout

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem Monoid.PushoutI.NormalWord.prod_injective {H : Type u_3} [Group H] {ι : Type u_5} {G : ιType u_6} [(i : ι) → Group (G i)] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :
                                    Function.Injective Monoid.PushoutI.NormalWord.prod
                                    instance Monoid.PushoutI.NormalWord.instFaithfulSMul {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] :
                                    Equations
                                    • =
                                    instance Monoid.PushoutI.NormalWord.instFaithfulSMul_1 {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [DecidableEq ι] [(i : ι) → DecidableEq (G i)] (i : ι) :
                                    Equations
                                    • =
                                    instance Monoid.PushoutI.NormalWord.instFaithfulSMul_2 {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} :
                                    Equations
                                    • =
                                    theorem Monoid.PushoutI.of_injective {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) (i : ι) :

                                    All maps into the PushoutI, or amalgamated product of groups are injective, provided all maps in the diagram are injective.

                                    See also base_injective

                                    theorem Monoid.PushoutI.base_injective {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) :
                                    def Monoid.PushoutI.Reduced {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] (φ : (i : ι) → H →* G i) (w : Monoid.CoprodI.Word G) :

                                    A word in CoprodI is reduced if none of its letters are in the base group.

                                    Equations
                                    Instances For
                                      theorem Monoid.PushoutI.Reduced.exists_normalWord_prod_eq {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (d : Monoid.PushoutI.NormalWord.Transversal φ) {w : Monoid.CoprodI.Word G} (hw : Monoid.PushoutI.Reduced φ w) :
                                      ∃ (w' : Monoid.PushoutI.NormalWord d), w'.prod = Monoid.PushoutI.ofCoprodI w.prod List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
                                      theorem Monoid.PushoutI.Reduced.eq_empty_of_mem_range {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) {w : Monoid.CoprodI.Word G} (hw : Monoid.PushoutI.Reduced φ w) (h : Monoid.PushoutI.ofCoprodI w.prod (Monoid.PushoutI.base φ).range) :
                                      w = Monoid.CoprodI.Word.empty

                                      For any word w in the coproduct, if w is reduced (i.e none its letters are in the image of the base monoid), and nonempty, then w itself is not in the image of the base group.

                                      theorem Monoid.PushoutI.inf_of_range_eq_base_range {ι : Type u_1} {G : ιType u_2} {H : Type u_3} [(i : ι) → Group (G i)] [Group H] {φ : (i : ι) → H →* G i} (hφ : ∀ (i : ι), Function.Injective (φ i)) {i : ι} {j : ι} (hij : i j) :

                                      The intersection of the images of the maps from any two distinct groups in the diagram into the amalgamated product is the image of the map from the base group in the diagram.