Documentation

Mathlib.GroupTheory.QuotientGroup

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 definitions #

Main statements #

Tags #

isomorphism theorems, quotient groups

The additive congruence relation generated by a normal additive subgroup.

Equations
Instances For
    theorem QuotientAddGroup.con.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (b : G) (c : G) (d : G) (hab : Setoid.r a b) (hcd : Setoid.r c d) :
    Setoid.r (a + c) (b + d)
    def QuotientGroup.con {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] :
    Con G

    The congruence relation generated by a normal subgroup.

    Equations
    Instances For
      theorem QuotientAddGroup.mk'.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) :
      ∀ (x x_1 : G), (x + x_1) = (x + x_1)
      def QuotientAddGroup.mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] :
      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 : Subgroup.Normal N] :
        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 : AddSubgroup.Normal N] :
          (QuotientAddGroup.mk' N) = QuotientAddGroup.mk
          @[simp]
          theorem QuotientGroup.coe_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] :
          (QuotientGroup.mk' N) = QuotientGroup.mk
          @[simp]
          theorem QuotientAddGroup.mk'_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (x : G) :
          @[simp]
          theorem QuotientGroup.mk'_apply {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (x : G) :
          (QuotientGroup.mk' N) x = x
          theorem QuotientAddGroup.mk'_eq_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {x : G} {y : G} :
          (QuotientAddGroup.mk' N) x = (QuotientAddGroup.mk' N) y ∃ z ∈ N, x + z = y
          theorem QuotientGroup.mk'_eq_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {x : G} {y : G} :
          (QuotientGroup.mk' N) x = (QuotientGroup.mk' N) y ∃ z ∈ N, x * z = y
          theorem QuotientAddGroup.addMonoidHom_ext {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] ⦃f : G N →+ M ⦃g : G N →+ M (h : AddMonoidHom.comp f (QuotientAddGroup.mk' N) = AddMonoidHom.comp g (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 {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] ⦃f : G N →* M ⦃g : G N →* M (h : MonoidHom.comp f (QuotientGroup.mk' N) = MonoidHom.comp g (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} [nN : AddSubgroup.Normal N] (x : G) :
          x = 0 x N
          @[simp]
          theorem QuotientGroup.eq_one_iff {G : Type u} [Group G] {N : Subgroup G} [nN : Subgroup.Normal N] (x : G) :
          x = 1 x N
          abbrev QuotientAddGroup.ker_le_range_iff.match_1 {H : Type u_1} [AddGroup H] {I : Type u_2} [AddGroup I] (g : H →+ I) (motive : (AddMonoidHom.ker g)Prop) :
          ∀ (x : (AddMonoidHom.ker g)), (∀ (val : H) (hx : val AddMonoidHom.ker g), motive { val := val, property := hx })motive x
          Equations
          • =
          Instances For
            theorem QuotientAddGroup.eq_iff_sub_mem {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : AddSubgroup.Normal N] {x : G} {y : G} :
            x = y x - y N
            theorem QuotientGroup.eq_iff_div_mem {G : Type u} [Group G] {N : Subgroup G} [nN : Subgroup.Normal N] {x : G} {y : G} :
            x = y x / y N
            theorem QuotientAddGroup.Quotient.addCommGroup.proof_1 {G : Type u_1} [AddCommGroup G] (N : AddSubgroup G) (a : G N) (b : G N) :
            a + b = b + a
            @[simp]
            theorem QuotientAddGroup.mk_zero {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] :
            0 = 0
            @[simp]
            theorem QuotientGroup.mk_one {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] :
            1 = 1
            @[simp]
            theorem QuotientAddGroup.mk_add {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (b : G) :
            (a + b) = a + b
            @[simp]
            theorem QuotientGroup.mk_mul {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (b : G) :
            (a * b) = a * b
            @[simp]
            theorem QuotientAddGroup.mk_neg {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) :
            (-a) = -a
            @[simp]
            theorem QuotientGroup.mk_inv {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) :
            a⁻¹ = (a)⁻¹
            @[simp]
            theorem QuotientAddGroup.mk_sub {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (b : G) :
            (a - b) = a - b
            @[simp]
            theorem QuotientGroup.mk_div {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (b : G) :
            (a / b) = a / b
            @[simp]
            theorem QuotientAddGroup.mk_nsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (n : ) :
            (n a) = n a
            @[simp]
            theorem QuotientGroup.mk_pow {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (n : ) :
            (a ^ n) = a ^ n
            @[simp]
            theorem QuotientAddGroup.mk_zsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (n : ) :
            (n a) = n a
            @[simp]
            theorem QuotientGroup.mk_zpow {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (n : ) :
            (a ^ n) = a ^ n
            @[simp]
            theorem QuotientAddGroup.mk_sum {G : Type u_1} {ι : Type u_2} [AddCommGroup G] (N : AddSubgroup G) (s : Finset ι) {f : ιG} :
            (Finset.sum s f) = Finset.sum s fun (i : ι) => (f i)
            @[simp]
            theorem QuotientGroup.mk_prod {G : Type u_1} {ι : Type u_2} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ιG} :
            (Finset.prod s f) = Finset.prod s fun (i : ι) => (f i)
            theorem QuotientAddGroup.lift.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type u_2} [AddMonoid M] (φ : G →+ M) (HN : N AddMonoidHom.ker φ) (x : G) (y : G) (h : (QuotientAddGroup.con N) x y) :
            (AddCon.ker φ) x y
            def QuotientAddGroup.lift {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] (φ : G →+ M) (HN : N AddMonoidHom.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 : Subgroup.Normal N] {M : Type x} [Monoid M] (φ : G →* M) (HN : N MonoidHom.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 : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N AddMonoidHom.ker φ) (g : G) :
                (QuotientAddGroup.lift N φ HN) g = φ g
                @[simp]
                theorem QuotientGroup.lift_mk {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] {φ : G →* M} (HN : N MonoidHom.ker φ) (g : G) :
                (QuotientGroup.lift N φ HN) g = φ g
                @[simp]
                theorem QuotientAddGroup.lift_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N AddMonoidHom.ker φ) (g : G) :
                (QuotientAddGroup.lift N φ HN) g = φ g
                @[simp]
                theorem QuotientGroup.lift_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] {φ : G →* M} (HN : N MonoidHom.ker φ) (g : G) :
                (QuotientGroup.lift N φ HN) g = φ g
                @[simp]
                theorem QuotientAddGroup.lift_quot_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N AddMonoidHom.ker φ) (g : G) :
                (QuotientAddGroup.lift N φ HN) (Quot.mk Setoid.r g) = φ g
                @[simp]
                theorem QuotientGroup.lift_quot_mk {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] {φ : G →* M} (HN : N MonoidHom.ker φ) (g : G) :
                (QuotientGroup.lift N φ HN) (Quot.mk Setoid.r g) = φ g
                theorem QuotientAddGroup.map.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) {H : Type u_2} [AddGroup H] (M : AddSubgroup H) (f : G →+ H) (h : N AddSubgroup.comap f M) ⦃x : G (hx : x N) :
                (f x) = 0
                def QuotientAddGroup.map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {H : Type v} [AddGroup H] (M : AddSubgroup H) [AddSubgroup.Normal M] (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 : Subgroup.Normal N] {H : Type v} [Group H] (M : Subgroup H) [Subgroup.Normal M] (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 : AddSubgroup.Normal N] {H : Type v} [AddGroup H] (M : AddSubgroup H) [AddSubgroup.Normal M] (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 : Subgroup.Normal N] {H : Type v} [Group H] (M : Subgroup H) [Subgroup.Normal M] (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 : AddSubgroup.Normal N] {H : Type v} [AddGroup H] (M : AddSubgroup H) [AddSubgroup.Normal M] (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 : Subgroup.Normal N] {H : Type v} [Group H] (M : Subgroup H) [Subgroup.Normal M] (f : G →* H) (h : N Subgroup.comap f M) (x : G) :
                    (QuotientGroup.map N M f h) ((QuotientGroup.mk' N) x) = (f x)
                    theorem QuotientGroup.map_id_apply {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (h : optParam (N Subgroup.comap (MonoidHom.id G) N) ) (x : G N) :
                    @[simp]
                    @[simp]
                    theorem QuotientAddGroup.map_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [AddSubgroup.Normal M] [AddSubgroup.Normal O] (f : G →+ H) (g : H →+ I) (hf : N AddSubgroup.comap f M) (hg : M AddSubgroup.comap g O) (hgf : optParam (N AddSubgroup.comap (AddMonoidHom.comp g f) O) ) (x : G N) :
                    @[simp]
                    theorem QuotientGroup.map_map {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [Subgroup.Normal M] [Subgroup.Normal O] (f : G →* H) (g : H →* I) (hf : N Subgroup.comap f M) (hg : M Subgroup.comap g O) (hgf : optParam (N Subgroup.comap (MonoidHom.comp g f) O) ) (x : G N) :
                    (QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (MonoidHom.comp g f) hgf) x
                    @[simp]
                    theorem QuotientGroup.map_comp_map {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [Subgroup.Normal M] [Subgroup.Normal O] (f : G →* H) (g : H →* I) (hf : N Subgroup.comap f M) (hg : M Subgroup.comap g O) (hgf : optParam (N Subgroup.comap (MonoidHom.comp g f) O) ) :
                    @[simp]
                    theorem QuotientAddGroup.image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] :
                    QuotientAddGroup.mk '' N = 0
                    @[simp]
                    theorem QuotientGroup.image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] :
                    QuotientGroup.mk '' N = 1
                    theorem QuotientAddGroup.preimage_image_coe {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (s : Set G) :
                    QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = N + s
                    theorem QuotientGroup.preimage_image_coe {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (s : Set G) :
                    QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = N * s
                    theorem QuotientAddGroup.image_coe_inj {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {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 : Subgroup.Normal N] {s : Set G} {t : Set G} :
                    QuotientGroup.mk '' s = QuotientGroup.mk '' t N * s = N * t
                    theorem QuotientAddGroup.congr.proof_3 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') :
                    G' AddSubgroup.comap (e) H'
                    theorem QuotientAddGroup.congr.proof_6 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') (x : G G') :
                    (QuotientAddGroup.map H' G' (AddEquiv.symm e) ) ((QuotientAddGroup.map G' H' e ) x) = x
                    theorem QuotientAddGroup.congr.proof_5 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') :
                    theorem QuotientAddGroup.congr.proof_8 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') (x : G G') (y : G G') :
                    (QuotientAddGroup.map G' H' e ).toFun (x + y) = (QuotientAddGroup.map G' H' e ).toFun x + (QuotientAddGroup.map G' H' e ).toFun y
                    theorem QuotientAddGroup.congr.proof_7 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') (x : H H') :
                    (QuotientAddGroup.map G' H' e ) ((QuotientAddGroup.map H' G' (AddEquiv.symm e) ) x) = x
                    def QuotientAddGroup.congr {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (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
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem QuotientAddGroup.congr.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (e) G' = H') :
                      G' AddSubgroup.comap (e) H'
                      def QuotientGroup.congr {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H'] (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
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem QuotientGroup.congr_mk {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H'] (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) [Subgroup.Normal G'] [Subgroup.Normal H'] (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) [Subgroup.Normal G'] [Subgroup.Normal H'] (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) [Subgroup.Normal G'] (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) [Subgroup.Normal G'] [Subgroup.Normal H'] (e : G ≃* H) (he : Subgroup.map (e) G' = H') :
                        theorem QuotientAddGroup.kerLift.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (_g : G) :
                        _g AddMonoidHom.ker φφ _g = 0
                        def QuotientAddGroup.kerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) :

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

                        Equations
                        Instances For
                          def QuotientGroup.kerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :

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

                          Equations
                          Instances For
                            @[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) :
                            @[simp]
                            theorem QuotientGroup.kerLift_mk' {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) :
                            (QuotientGroup.kerLift φ) g = φ g

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

                            Equations
                            Instances For
                              theorem QuotientAddGroup.rangeKerLift.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (g : G) (hg : g AddMonoidHom.ker φ) :
                              def QuotientGroup.rangeKerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) :

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

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

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

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

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

                                  Equations
                                  Instances For
                                    theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (x : G AddMonoidHom.ker φ) :
                                    (QuotientAddGroup.mk ψ) ((QuotientAddGroup.kerLift φ) x) = x
                                    def QuotientAddGroup.quotientKerEquivOfRightInverse {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :

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

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem QuotientGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :
                                      ∀ (a : H), (MulEquiv.symm (QuotientGroup.quotientKerEquivOfRightInverse φ ψ )) a = (QuotientGroup.mk ψ) a
                                      @[simp]
                                      theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) (a : G MonoidHom.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), (AddEquiv.symm (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ )) a = (QuotientAddGroup.mk ψ) a
                                      def QuotientGroup.quotientKerEquivOfRightInverse {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : HG) (hφ : Function.RightInverse ψ φ) :

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

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

                                        The canonical isomorphism G/⊥ ≃+ G.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] :
                                          ∀ (a : G), (AddEquiv.symm QuotientAddGroup.quotientBot) a = a
                                          @[simp]
                                          theorem QuotientGroup.quotientBot_apply {G : Type u} [Group G] (a : G MonoidHom.ker (MonoidHom.id G)) :
                                          QuotientGroup.quotientBot a = (QuotientGroup.kerLift (MonoidHom.id G)) a
                                          @[simp]
                                          theorem QuotientGroup.quotientBot_symm_apply {G : Type u} [Group G] :
                                          ∀ (a : G), (MulEquiv.symm QuotientGroup.quotientBot) a = a
                                          @[simp]
                                          theorem QuotientAddGroup.quotientBot_apply {G : Type u} [AddGroup G] (a : G AddMonoidHom.ker (AddMonoidHom.id G)) :
                                          QuotientAddGroup.quotientBot a = (QuotientAddGroup.kerLift (AddMonoidHom.id G)) a

                                          The canonical isomorphism G/⊥ ≃* G.

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

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

                                            Equations
                                            Instances For
                                              noncomputable def QuotientGroup.quotientKerEquivOfSurjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (hφ : Function.Surjective φ) :

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

                                              For a computable version, see QuotientGroup.quotientKerEquivOfRightInverse.

                                              Equations
                                              Instances For

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

                                                Equations
                                                Instances For
                                                  def QuotientGroup.quotientMulEquivOfEq {G : Type u} [Group G] {M : Subgroup G} {N : Subgroup G} [Subgroup.Normal M] [Subgroup.Normal N] (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 : Subgroup G} {N : Subgroup G} [Subgroup.Normal M] [Subgroup.Normal N] (h : M = N) (x : G) :

                                                    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 QuotientGroup.quotientMapSubgroupOfOfLe {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [_hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)] [_hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)] (h' : A' B') (h : A 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' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [_hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)] [_hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)] (h' : A' B') (h : A B) (x : A) :
                                                        theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_1 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {B' : AddSubgroup G} (h' : A' = B') :
                                                        A' B'
                                                        theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_3 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {B' : AddSubgroup G} (h' : A' = B') :
                                                        B' A'

                                                        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 on A.

                                                        Equations
                                                        Instances For
                                                          def QuotientGroup.equivQuotientSubgroupOfOfEq {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)] [hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)] (h' : A' = B') (h : A = 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

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

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              abbrev QuotientAddGroup.homQuotientZSMulOfHom.match_1 {A : Type u_1} [AddCommGroup A] (n : ) (g : A) (motive : g AddMonoidHom.range (zsmulAddGroupHom n)Prop) :
                                                              ∀ (x : g AddMonoidHom.range (zsmulAddGroupHom n)), (∀ (h : A) (hg : n h = g), motive )motive x
                                                              Equations
                                                              • =
                                                              Instances For

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

                                                                Equations
                                                                Instances For

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

                                                                  Equations
                                                                  Instances For

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

                                                                    Equations
                                                                    Instances For

                                                                      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

                                                                        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
                                                                          Equations
                                                                          • =

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

                                                                          Equations
                                                                          Instances For

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

                                                                            Equations
                                                                            Instances For

                                                                              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

                                                                                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

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

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

                                                                                  noncomputable def AddGroup.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : AddMonoidHom.ker g AddMonoidHom.range f) :

                                                                                  If F and H are finite such that ker(G →+ H) ≤ im(F →+ G), then G is finite.

                                                                                  Equations
                                                                                  Instances For
                                                                                    noncomputable def Group.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : MonoidHom.ker g MonoidHom.range f) :

                                                                                    If F and H are finite such that ker(G →* H) ≤ im(F →* G), then G is finite.

                                                                                    Equations
                                                                                    Instances For
                                                                                      noncomputable def AddGroup.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : AddMonoidHom.ker g = AddMonoidHom.range f) :

                                                                                      If F and H are finite such that ker(G →+ H) = im(F →+ G), then G is finite.

                                                                                      Equations
                                                                                      Instances For
                                                                                        noncomputable def Group.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : MonoidHom.ker g = MonoidHom.range f) :

                                                                                        If F and H are finite such that ker(G →* H) = im(F →* G), then G is finite.

                                                                                        Equations
                                                                                        Instances For
                                                                                          theorem AddGroup.fintypeOfKerOfCodom.proof_2 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) (x : G) (hx : x AddMonoidHom.ker g) :
                                                                                          ∃ (y : (AddMonoidHom.ker g)), (AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddSubgroup.topEquiv) (AddSubgroup.inclusion )) y = x
                                                                                          noncomputable def AddGroup.fintypeOfKerOfCodom {G : Type u} {H : Type u} [AddGroup G] [AddGroup H] [Fintype H] (g : G →+ H) [Fintype (AddMonoidHom.ker g)] :

                                                                                          If ker(G →+ H) and H are finite, then G is finite.

                                                                                          Equations
                                                                                          Instances For
                                                                                            noncomputable def Group.fintypeOfKerOfCodom {G : Type u} {H : Type u} [Group G] [Group H] [Fintype H] (g : G →* H) [Fintype (MonoidHom.ker g)] :

                                                                                            If ker(G →* H) and H are finite, then G is finite.

                                                                                            Equations
                                                                                            Instances For
                                                                                              theorem AddGroup.fintypeOfDomOfCoker.proof_1 {F : Type u_1} {G : Type u_1} [AddGroup F] [AddGroup G] (f : F →+ G) [AddSubgroup.Normal (AddMonoidHom.range f)] (x : G) :
                                                                                              x = 0x AddMonoidHom.range f

                                                                                              If F and coker(F →+ G) are finite, then G is finite.

                                                                                              Equations
                                                                                              Instances For
                                                                                                noncomputable def Group.fintypeOfDomOfCoker {F : Type u} {G : Type u} [Group F] [Group G] [Fintype F] (f : F →* G) [Subgroup.Normal (MonoidHom.range f)] [Fintype (G MonoidHom.range f)] :

                                                                                                If F and coker(F →* G) are finite, then G is finite.

                                                                                                Equations
                                                                                                Instances For