Documentation

Mathlib.GroupTheory.QuotientGroup.Defs

Quotients of groups by normal subgroups #

This file defines the group structure on the quotient by a normal subgroup.

Main definitions #

Tags #

quotient groups

def QuotientAddGroup.con {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :

The additive congruence relation generated by a normal additive subgroup.

Equations
Instances For
    def QuotientGroup.con {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
    Con G

    The congruence relation generated by a normal subgroup.

    Equations
    Instances For
      instance QuotientGroup.Quotient.group {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
      Group (G N)
      Equations
      def QuotientAddGroup.mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
      G →+ G N

      The additive group homomorphism from G to G/N.

      Equations
      Instances For
        def QuotientGroup.mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
        G →* G N

        The group homomorphism from G to G/N.

        Equations
        Instances For
          @[simp]
          theorem QuotientAddGroup.coe_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
          (QuotientAddGroup.mk' N) = QuotientAddGroup.mk
          @[simp]
          theorem QuotientGroup.coe_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          (QuotientGroup.mk' N) = QuotientGroup.mk
          @[simp]
          theorem QuotientAddGroup.mk'_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (x : G) :
          @[simp]
          theorem QuotientGroup.mk'_apply {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (x : G) :
          (QuotientGroup.mk' N) x = x
          theorem QuotientAddGroup.mk'_eq_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {x : G} {y : G} :
          (QuotientAddGroup.mk' N) x = (QuotientAddGroup.mk' N) y zN, x + z = y
          theorem QuotientGroup.mk'_eq_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {x : G} {y : G} :
          (QuotientGroup.mk' N) x = (QuotientGroup.mk' N) y zN, x * z = y
          theorem QuotientAddGroup.addMonoidHom_ext {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] ⦃f : G N →+ M ⦃g : G N →+ M (h : f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)) :
          f = g

          Two AddMonoidHoms from an additive quotient group are equal if their compositions with AddQuotientGroup.mk' are equal.

          See note [partially-applied ext lemmas].

          theorem QuotientGroup.monoidHom_ext_iff {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {M : Type x} [Monoid M] {f : G N →* M} {g : G N →* M} :
          f = g f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)
          theorem QuotientAddGroup.addMonoidHom_ext_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {M : Type x} [AddMonoid M] {f : G N →+ M} {g : G N →+ M} :
          f = g f.comp (QuotientAddGroup.mk' N) = g.comp (QuotientAddGroup.mk' N)
          theorem QuotientGroup.monoidHom_ext {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] ⦃f : G N →* M ⦃g : G N →* M (h : f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)) :
          f = g

          Two MonoidHoms from a quotient group are equal if their compositions with QuotientGroup.mk' are equal.

          See note [partially-applied ext lemmas].

          @[simp]
          theorem QuotientAddGroup.eq_zero_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [N.Normal] (x : G) :
          x = 0 x N
          @[simp]
          theorem QuotientGroup.eq_one_iff {G : Type u} [Group G] {N : Subgroup G} [N.Normal] (x : G) :
          x = 1 x N
          theorem QuotientAddGroup.ker_le_range_iff {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] {I : Type w} [AddGroup I] (f : G →+ H) [f.range.Normal] (g : H →+ I) :
          g.ker f.range (QuotientAddGroup.mk' f.range).comp g.ker.subtype = 0
          theorem QuotientGroup.ker_le_range_iff {G : Type u} [Group G] {H : Type v} [Group H] {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) :
          g.ker f.range (QuotientGroup.mk' f.range).comp g.ker.subtype = 1
          @[simp]
          theorem QuotientAddGroup.ker_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
          @[simp]
          theorem QuotientGroup.ker_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          theorem QuotientAddGroup.eq_iff_sub_mem {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : N.Normal] {x : G} {y : G} :
          x = y x - y N
          theorem QuotientGroup.eq_iff_div_mem {G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {x : G} {y : G} :
          x = y x / y N
          @[simp]
          theorem QuotientAddGroup.mk_zero {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
          0 = 0
          @[simp]
          theorem QuotientGroup.mk_one {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          1 = 1
          @[simp]
          theorem QuotientAddGroup.mk_add {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a + b) = a + b
          @[simp]
          theorem QuotientGroup.mk_mul {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a * b) = a * b
          @[simp]
          theorem QuotientAddGroup.mk_neg {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) :
          (-a) = -a
          @[simp]
          theorem QuotientGroup.mk_inv {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) :
          a⁻¹ = (↑a)⁻¹
          @[simp]
          theorem QuotientAddGroup.mk_sub {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a - b) = a - b
          @[simp]
          theorem QuotientGroup.mk_div {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (b : G) :
          (a / b) = a / b
          @[simp]
          theorem QuotientAddGroup.mk_nsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ) :
          (n a) = n a
          @[simp]
          theorem QuotientGroup.mk_pow {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ) :
          (a ^ n) = a ^ n
          @[simp]
          theorem QuotientAddGroup.mk_zsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (a : G) (n : ) :
          (n a) = n a
          @[simp]
          theorem QuotientGroup.mk_zpow {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ) :
          (a ^ n) = a ^ n
          @[simp]
          @[simp]
          theorem QuotientGroup.map_mk'_self {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
          def QuotientAddGroup.lift {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] (φ : G →+ M) (HN : N φ.ker) :
          G N →+ M

          An AddGroup homomorphism φ : G →+ M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

          Equations
          Instances For
            def QuotientGroup.lift {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N φ.ker) :
            G N →* M

            A group homomorphism φ : G →* M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

            Equations
            Instances For
              @[simp]
              theorem QuotientAddGroup.lift_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N φ.ker) (g : G) :
              (QuotientAddGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientGroup.lift_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N φ.ker) (g : G) :
              (QuotientGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientAddGroup.lift_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N φ.ker) (g : G) :
              (QuotientAddGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientGroup.lift_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N φ.ker) (g : G) :
              (QuotientGroup.lift N φ HN) g = φ g
              @[simp]
              theorem QuotientAddGroup.lift_quot_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N φ.ker) (g : G) :
              @[simp]
              theorem QuotientGroup.lift_quot_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N φ.ker) (g : G) :
              def QuotientAddGroup.map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N AddSubgroup.comap f M) :
              G N →+ H M

              An AddGroup homomorphism f : G →+ H induces a map G/N →+ H/M if N ⊆ f⁻¹(M).

              Equations
              Instances For
                def QuotientGroup.map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N Subgroup.comap f M) :
                G N →* H M

                A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).

                Equations
                Instances For
                  @[simp]
                  theorem QuotientAddGroup.map_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N AddSubgroup.comap f M) (x : G) :
                  (QuotientAddGroup.map N M f h) x = (f x)
                  @[simp]
                  theorem QuotientGroup.map_mk {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N Subgroup.comap f M) (x : G) :
                  (QuotientGroup.map N M f h) x = (f x)
                  theorem QuotientAddGroup.map_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N AddSubgroup.comap f M) (x : G) :
                  (QuotientAddGroup.map N M f h) ((QuotientAddGroup.mk' N) x) = (f x)
                  theorem QuotientGroup.map_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N Subgroup.comap f M) (x : G) :
                  (QuotientGroup.map N M f h) ((QuotientGroup.mk' N) x) = (f x)
                  theorem QuotientAddGroup.map_id_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : optParam (N AddSubgroup.comap (AddMonoidHom.id G) N) ) (x : G N) :
                  theorem QuotientGroup.map_id_apply {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : optParam (N Subgroup.comap (MonoidHom.id G) N) ) (x : G N) :
                  @[simp]
                  @[simp]
                  theorem QuotientGroup.map_id {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : optParam (N Subgroup.comap (MonoidHom.id G) N) ) :
                  @[simp]
                  theorem QuotientAddGroup.map_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N AddSubgroup.comap f M) (hg : M AddSubgroup.comap g O) (hgf : optParam (N AddSubgroup.comap (g.comp f) O) ) (x : G N) :
                  (QuotientAddGroup.map M O g hg) ((QuotientAddGroup.map N M f hf) x) = (QuotientAddGroup.map N O (g.comp f) hgf) x
                  @[simp]
                  theorem QuotientGroup.map_map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N Subgroup.comap f M) (hg : M Subgroup.comap g O) (hgf : optParam (N Subgroup.comap (g.comp f) O) ) (x : G N) :
                  (QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (g.comp f) hgf) x
                  @[simp]
                  theorem QuotientAddGroup.map_comp_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G →+ H) (g : H →+ I) (hf : N AddSubgroup.comap f M) (hg : M AddSubgroup.comap g O) (hgf : optParam (N AddSubgroup.comap (g.comp f) O) ) :
                  (QuotientAddGroup.map M O g hg).comp (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (g.comp f) hgf
                  @[simp]
                  theorem QuotientGroup.map_comp_map {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N Subgroup.comap f M) (hg : M Subgroup.comap g O) (hgf : optParam (N Subgroup.comap (g.comp f) O) ) :
                  (QuotientGroup.map M O g hg).comp (QuotientGroup.map N M f hf) = QuotientGroup.map N O (g.comp f) hgf
                  @[simp]
                  theorem QuotientAddGroup.image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] :
                  QuotientAddGroup.mk '' N = 0
                  @[simp]
                  theorem QuotientGroup.image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] :
                  QuotientGroup.mk '' N = 1
                  theorem QuotientAddGroup.preimage_image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (s : Set G) :
                  QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = N + s
                  theorem QuotientGroup.preimage_image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (s : Set G) :
                  QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = N * s
                  theorem QuotientAddGroup.image_coe_inj {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {s : Set G} {t : Set G} :
                  QuotientAddGroup.mk '' s = QuotientAddGroup.mk '' t N + s = N + t
                  theorem QuotientGroup.image_coe_inj {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {s : Set G} {t : Set G} :
                  QuotientGroup.mk '' s = QuotientGroup.mk '' t N * s = N * t
                  def QuotientAddGroup.congr {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') :
                  G G' ≃+ H H'

                  QuotientAddGroup.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H', given that e maps G to H.

                  Equations
                  Instances For
                    def QuotientGroup.congr {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') :
                    G G' ≃* H H'

                    QuotientGroup.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H', given that e maps G to H.

                    Equations
                    Instances For
                      @[simp]
                      theorem QuotientGroup.congr_mk {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) :
                      (QuotientGroup.congr G' H' e he) x = (e x)
                      theorem QuotientGroup.congr_mk' {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) :
                      (QuotientGroup.congr G' H' e he) ((QuotientGroup.mk' G') x) = (QuotientGroup.mk' H') (e x)
                      @[simp]
                      theorem QuotientGroup.congr_apply {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) :
                      (QuotientGroup.congr G' H' e he) x = (QuotientGroup.mk' H') (e x)
                      @[simp]
                      theorem QuotientGroup.congr_refl {G : Type u} [Group G] (G' : Subgroup G) [G'.Normal] (he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') ) :
                      @[simp]
                      theorem QuotientGroup.congr_symm {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') :
                      (QuotientGroup.congr G' H' e he).symm = QuotientGroup.congr H' G' e.symm