Documentation

Mathlib.GroupTheory.QuotientGroup.Basic

Quotients of groups by normal subgroups #

This files develops the basic theory of quotients of groups by normal subgroups. In particular it proves Noether's first and second isomorphism theorems.

Main statements #

Tags #

isomorphism theorems, quotient groups

theorem QuotientGroup.sound {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (U : Set (G N)) (g : N.op) :
theorem QuotientAddGroup.sound {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (U : Set (G N)) (g : N.op) :
@[simp]
theorem QuotientGroup.mk_prod {G : Type u_1} {ι : Type u_2} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ιG} :
(s.prod f) = is, (f i)
@[simp]
theorem QuotientAddGroup.mk_sum {G : Type u_1} {ι : Type u_2} [AddCommGroup G] (N : AddSubgroup G) (s : Finset ι) {f : ιG} :
(s.sum f) = is, (f i)
theorem QuotientGroup.strictMono_comap_prod_map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
def QuotientGroup.kerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
G φ.ker →* H

The induced map from the quotient by the kernel to the codomain.

Equations
Instances For
    def QuotientAddGroup.kerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
    G φ.ker →+ H

    The induced map from the quotient by the kernel to the codomain.

    Equations
    Instances For
      @[simp]
      theorem QuotientGroup.kerLift_mk {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) :
      (QuotientGroup.kerLift φ) g = φ g
      @[simp]
      theorem QuotientAddGroup.kerLift_mk {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) :
      @[simp]
      theorem QuotientGroup.kerLift_mk' {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) :
      (QuotientGroup.kerLift φ) g = φ g
      @[simp]
      theorem QuotientAddGroup.kerLift_mk' {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) :
      def QuotientGroup.rangeKerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
      G φ.ker →* φ.range

      The induced map from the quotient by the kernel to the range.

      Equations
      Instances For
        def QuotientAddGroup.rangeKerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
        G φ.ker →+ φ.range

        The induced map from the quotient by the kernel to the range.

        Equations
        Instances For
          noncomputable def QuotientGroup.quotientKerEquivRange {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
          G φ.ker ≃* φ.range

          Noether's first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

          Equations
          Instances For
            noncomputable def QuotientAddGroup.quotientKerEquivRange {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :
            G φ.ker ≃+ φ.range

            The first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

            Equations
            Instances For
              def QuotientGroup.quotientKerEquivOfRightInverse {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :
              G φ.ker ≃* H

              The canonical isomorphism G/(ker φ) ≃* H induced by a homomorphism φ : G →* H with a right inverse ψ : H → G.

              Equations
              Instances For
                def QuotientAddGroup.quotientKerEquivOfRightInverse {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :
                G φ.ker ≃+ H

                The canonical isomorphism G/(ker φ) ≃+ H induced by a homomorphism φ : G →+ H with a right inverse ψ : H → G.

                Equations
                Instances For
                  @[simp]
                  theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a : G φ.ker) :
                  @[simp]
                  theorem QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a✝ : H) :
                  (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ ).symm a✝ = (QuotientAddGroup.mk ψ) a✝
                  @[simp]
                  theorem QuotientAddGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a : G φ.ker) :
                  @[simp]
                  theorem QuotientGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a✝ : H) :
                  (QuotientGroup.quotientKerEquivOfRightInverse φ ψ ).symm a✝ = (QuotientGroup.mk ψ) a✝

                  The canonical isomorphism G/⊥ ≃* G.

                  Equations
                  Instances For

                    The canonical isomorphism G/⊥ ≃+ G.

                    Equations
                    Instances For
                      @[simp]
                      theorem QuotientGroup.quotientBot_symm_apply {G : Type u} [Group G] (a✝ : G) :
                      QuotientGroup.quotientBot.symm a✝ = a✝
                      @[simp]
                      theorem QuotientAddGroup.quotientBot_apply {G : Type u} [AddGroup G] (a : G (AddMonoidHom.id G).ker) :
                      QuotientAddGroup.quotientBot a = (QuotientAddGroup.kerLift (AddMonoidHom.id G)) a
                      @[simp]
                      theorem QuotientGroup.quotientBot_apply {G : Type u} [Group G] (a : G (MonoidHom.id G).ker) :
                      QuotientGroup.quotientBot a = (QuotientGroup.kerLift (MonoidHom.id G)) a
                      @[simp]
                      theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] (a✝ : G) :
                      QuotientAddGroup.quotientBot.symm a✝ = a✝
                      noncomputable def QuotientGroup.quotientKerEquivOfSurjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (hφ : Function.Surjective φ) :
                      G φ.ker ≃* H

                      The canonical isomorphism G/(ker φ) ≃* H induced by a surjection φ : G →* H.

                      For a computable version, see QuotientGroup.quotientKerEquivOfRightInverse.

                      Equations
                      Instances For
                        noncomputable def QuotientAddGroup.quotientKerEquivOfSurjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (hφ : Function.Surjective φ) :
                        G φ.ker ≃+ H

                        The canonical isomorphism G/(ker φ) ≃+ H induced by a surjection φ : G →+ H. For a computable version, see QuotientAddGroup.quotientKerEquivOfRightInverse.

                        Equations
                        Instances For
                          def QuotientGroup.quotientMulEquivOfEq {G : Type u} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) :
                          G M ≃* G N

                          If two normal subgroups M and N of G are the same, their quotient groups are isomorphic.

                          Equations
                          Instances For
                            def QuotientAddGroup.quotientAddEquivOfEq {G : Type u} [AddGroup G] {M N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) :
                            G M ≃+ G N

                            If two normal subgroups M and N of G are the same, their quotient groups are isomorphic.

                            Equations
                            Instances For
                              @[simp]
                              theorem QuotientGroup.quotientMulEquivOfEq_mk {G : Type u} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) :
                              @[simp]
                              theorem QuotientAddGroup.quotientAddEquivOfEq_mk {G : Type u} [AddGroup G] {M N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) :
                              def QuotientGroup.quotientMapSubgroupOfOfLe {G : Type u} [Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' B') (h : A B) :
                              A A'.subgroupOf A →* B B'.subgroupOf B

                              Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B, then there is a map A / (A' ⊓ A) →* B / (B' ⊓ B) induced by the inclusions.

                              Equations
                              Instances For
                                def QuotientAddGroup.quotientMapAddSubgroupOfOfLe {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' B') (h : A B) :
                                A A'.addSubgroupOf A →+ B B'.addSubgroupOf B

                                Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B, then there is a map A / (A' ⊓ A) →+ B / (B' ⊓ B) induced by the inclusions.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem QuotientGroup.quotientMapSubgroupOfOfLe_mk {G : Type u} [Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' B') (h : A B) (x : A) :
                                  @[simp]
                                  theorem QuotientAddGroup.quotientMapAddSubgroupOfOfLe_mk {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' B') (h : A B) (x : A) :
                                  def QuotientGroup.equivQuotientSubgroupOfOfEq {G : Type u} [Group G] {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal] [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) :
                                  A A'.subgroupOf A ≃* B B'.subgroupOf B

                                  Let A', A, B', B be subgroups of G. If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic.

                                  Applying this equiv is nicer than rewriting along the equalities, since the type of (A'.subgroupOf A : Subgroup A) depends on A.

                                  Equations
                                  Instances For
                                    def QuotientAddGroup.equivQuotientAddSubgroupOfOfEq {G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [hAN : (A'.addSubgroupOf A).Normal] [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B) :
                                    A A'.addSubgroupOf A ≃+ B B'.addSubgroupOf B

                                    Let A', A, B', B be subgroups of G. If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic. Applying this equiv is nicer than rewriting along the equalities, since the type of (A'.addSubgroupOf A : AddSubgroup A) depends on A.

                                    Equations
                                    Instances For
                                      def QuotientGroup.homQuotientZPowOfHom {A B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (n : ) :
                                      A (zpowGroupHom n).range →* B (zpowGroupHom n).range

                                      The map of quotients by powers of an integer induced by a group homomorphism.

                                      Equations
                                      Instances For

                                        The map of quotients by multiples of an integer induced by an additive group homomorphism.

                                        Equations
                                        Instances For
                                          def QuotientGroup.equivQuotientZPowOfEquiv {A B : Type u} [CommGroup A] [CommGroup B] (e : A ≃* B) (n : ) :
                                          A (zpowGroupHom n).range ≃* B (zpowGroupHom n).range

                                          The equivalence of quotients by powers of an integer induced by a group isomorphism.

                                          Equations
                                          Instances For

                                            The equivalence of quotients by multiples of an integer induced by an additive group isomorphism.

                                            Equations
                                            Instances For
                                              noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient {G : Type u} [Group G] (H N : Subgroup G) [N.Normal] :
                                              H N.subgroupOf H ≃* (H N) N.subgroupOf (H N)

                                              Noether's second isomorphism theorem: given two subgroups H and N of a group G, where N is normal, defines an isomorphism between H/(H ∩ N) and (HN)/N.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                noncomputable def QuotientAddGroup.quotientInfEquivSumNormalQuotient {G : Type u} [AddGroup G] (H N : AddSubgroup G) [N.Normal] :
                                                H N.addSubgroupOf H ≃+ (H N) N.addSubgroupOf (H N)

                                                The second isomorphism theorem: given two subgroups H and N of a group G, where N is normal, defines an isomorphism between H/(H ∩ N) and (H + N)/N

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  instance QuotientGroup.map_normal {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] :
                                                  instance QuotientAddGroup.map_normal {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] :
                                                  def QuotientGroup.quotientQuotientEquivQuotientAux {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) :

                                                  The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M.

                                                  Equations
                                                  Instances For
                                                    def QuotientAddGroup.quotientQuotientEquivQuotientAux {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) :

                                                    The map from the third isomorphism theorem for additive groups: (A / N) / (M / N) → A / M.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) (x : G N) :
                                                      @[simp]
                                                      theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) (x : G N) :
                                                      theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) (x : G) :
                                                      theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) (x : G) :
                                                      def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) :

                                                      Noether's third isomorphism theorem for groups: (G / N) / (M / N) ≃* G / M.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def QuotientAddGroup.quotientQuotientEquivQuotient {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N M) :

                                                        Noether's third isomorphism theorem for additive groups: (A / N) / (M / N) ≃+ A / M.

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

                                                          If the quotient by a subgroup gives a singleton then the subgroup is the whole group.

                                                          If the quotient by an additive subgroup gives a singleton then the additive subgroup is the whole additive group.

                                                          @[simp]
                                                          theorem QuotientAddGroup.mk_nat_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ) (a : R) :
                                                          (n * a) = n a
                                                          @[simp]
                                                          theorem QuotientAddGroup.mk_int_mul {R : Type u_1} [NonAssocRing R] (N : AddSubgroup R) [N.Normal] (n : ) (a : R) :
                                                          (n * a) = n a