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) :
g (mk' N) ⁻¹' U = (mk' N) ⁻¹' U
theorem QuotientAddGroup.sound {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (U : Set (G N)) (g : N.op) :
g +ᵥ (mk' N) ⁻¹' U = (mk' N) ⁻¹' U
@[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)
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) :
          (kerLift φ) g = φ g
          @[simp]
          theorem QuotientAddGroup.kerLift_mk {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) :
          (kerLift φ) g = φ g
          @[simp]
          theorem QuotientGroup.kerLift_mk' {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) :
          (kerLift φ) g = φ g
          @[simp]
          theorem QuotientAddGroup.kerLift_mk' {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) :
          (kerLift φ) g = φ g
          theorem QuotientGroup.kerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :
          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) ( : 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) ( : 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_symm_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) ( : Function.RightInverse ψ φ) (a✝ : H) :
                                  (quotientKerEquivOfRightInverse φ ψ ).symm a✝ = (mk ψ) a✝
                                  @[simp]
                                  theorem QuotientAddGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) ( : Function.RightInverse ψ φ) (a : G φ.ker) :
                                  @[simp]
                                  theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) ( : Function.RightInverse ψ φ) (a : G φ.ker) :
                                  @[simp]
                                  theorem QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) ( : Function.RightInverse ψ φ) (a✝ : H) :
                                  (quotientKerEquivOfRightInverse φ ψ ).symm a✝ = (mk ψ) a✝

                                  The canonical isomorphism G/⊥ ≃* G.

                                  Equations
                                    Instances For

                                      The canonical isomorphism G/⊥ ≃+ G.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] (a✝ : G) :
                                          quotientBot.symm a✝ = a✝
                                          @[simp]
                                          theorem QuotientGroup.quotientBot_symm_apply {G : Type u} [Group G] (a✝ : G) :
                                          quotientBot.symm a✝ = a✝
                                          noncomputable def QuotientGroup.quotientKerEquivOfSurjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* 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) ( : 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) :
                                                          (quotientMulEquivOfEq h) x = x
                                                          @[simp]
                                                          theorem QuotientAddGroup.quotientAddEquivOfEq_mk {G : Type u} [AddGroup G] {M N : AddSubgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) :
                                                          (quotientAddEquivOfEq h) x = x
                                                          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

                                                                          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

                                                                                  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.quotientInfEquivProdNormalizerQuotient {G : Type u} [Group G] (H N : Subgroup G) (hLE : H N.normalizer) :
                                                                                          H N.subgroupOf H ≃* (HN) N.subgroupOf (HN)

                                                                                          Noether's second isomorphism theorem: given a subgroup N of G and a subgroup H of the normalizer of N in G, defines an isomorphism between H/(H ∩ N) and (HN)/N.

                                                                                          Equations
                                                                                            Instances For
                                                                                              noncomputable def QuotientAddGroup.quotientInfEquivSumNormalizerQuotient {G : Type u} [AddGroup G] (H N : AddSubgroup G) (hLE : H N.normalizer) :
                                                                                              H N.addSubgroupOf H ≃+ (HN) N.addSubgroupOf (HN)

                                                                                              Noether's second isomorphism theorem: given a subgroup N of G and a subgroup H of the normalizer of N in G, defines an isomorphism between H/(H ∩ N) and (H + N)/N

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

                                                                                                  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
                                                                                                    Instances For
                                                                                                      noncomputable def QuotientAddGroup.quotientInfEquivSumNormalQuotient {G : Type u} [AddGroup G] (H N : AddSubgroup G) [hN : N.Normal] :
                                                                                                      H N.addSubgroupOf H ≃+ (HN) N.addSubgroupOf (HN)

                                                                                                      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 (H + N)/N

                                                                                                      Equations
                                                                                                        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) :
                                                                                                          (G N) Subgroup.map (mk' N) M →* G 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) :
                                                                                                              (G N) AddSubgroup.map (mk' N) M →+ G 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) :
                                                                                                                  (quotientQuotientEquivQuotientAux N M h) x = x
                                                                                                                  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) :
                                                                                                                  (quotientQuotientEquivQuotientAux N M h) x = x
                                                                                                                  def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N M) :
                                                                                                                  (G N) Subgroup.map (mk' N) M ≃* G M

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

                                                                                                                  Equations
                                                                                                                    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) :
                                                                                                                      (G N) AddSubgroup.map (mk' N) M ≃+ G M

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

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          theorem QuotientGroup.le_comap_mk' {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (H : Subgroup (G N)) :
                                                                                                                          @[simp]
                                                                                                                          theorem QuotientGroup.comap_map_mk' {G : Type u} [Group G] (N H : Subgroup G) [N.Normal] :
                                                                                                                          Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = NH
                                                                                                                          @[simp]
                                                                                                                          def QuotientGroup.comapMk'OrderIso {G : Type u} [Group G] (N : Subgroup G) [hn : N.Normal] :
                                                                                                                          Subgroup (G N) ≃o { H : Subgroup G // N H }

                                                                                                                          The correspondence theorem, or lattice theorem, or fourth isomorphism theorem for multiplicative groups

                                                                                                                          Equations
                                                                                                                            Instances For

                                                                                                                              The correspondence theorem, or lattice theorem, or fourth isomorphism theorem for additive groups

                                                                                                                              Equations
                                                                                                                                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.

                                                                                                                                  theorem QuotientGroup.comap_comap_center {G : Type u} [Group G] {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G H₁)} [H₂.Normal] :
                                                                                                                                  @[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