Documentation

Mathlib.GroupTheory.QuotientGroup.Finite

Deducing finiteness of a group. #

theorem AddGroup.fintypeOfKerLeRange.proof_1 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) :
g.ker.Normal
theorem AddGroup.fintypeOfKerLeRange.proof_2 {F : Type u_1} {G : Type u_1} {H : Type u_1} [AddGroup F] [AddGroup G] [AddGroup H] (f : F →+ G) (g : G →+ H) (h : g.ker f.range) :
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 : g.ker f.range) :

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 : g.ker f.range) :

    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 : g.ker = f.range) :

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

      Equations
      Instances For
        theorem AddGroup.fintypeOfKerEqRange.proof_1 {F : Type u_1} {G : Type u_1} {H : Type u_1} [AddGroup F] [AddGroup G] [AddGroup H] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range) :
        g.ker f.range
        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 : g.ker = f.range) :

        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_1 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) :
          g.ker
          noncomputable def AddGroup.fintypeOfKerOfCodom {G : Type u} {H : Type u} [AddGroup G] [AddGroup H] [Fintype H] (g : G →+ H) [Fintype g.ker] :

          If ker(G →+ H) and H are finite, 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 g.ker) :
            ∃ (y : g.ker), (AddSubgroup.topEquiv.toAddMonoidHom.comp (AddSubgroup.inclusion )) y = x
            noncomputable def Group.fintypeOfKerOfCodom {G : Type u} {H : Type u} [Group G] [Group H] [Fintype H] (g : G →* H) [Fintype g.ker] :

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

            Equations
            Instances For
              noncomputable def AddGroup.fintypeOfDomOfCoker {F : Type u} {G : Type u} [AddGroup F] [AddGroup G] [Fintype F] (f : F →+ G) [f.range.Normal] [Fintype (G f.range)] :

              If F and coker(F →+ G) 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) [f.range.Normal] (x : G) :
                x = 0x f.range
                noncomputable def Group.fintypeOfDomOfCoker {F : Type u} {G : Type u} [Group F] [Group G] [Fintype F] (f : F →* G) [f.range.Normal] [Fintype (G f.range)] :

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

                Equations
                Instances For