Deducing finiteness of a group.

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) : Fintype G

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

Equations

• Group.fintypeOfKerLeRange f g h = Fintype.ofEquiv ((G ⧸ g.ker) × ↥g.ker) Subgroup.groupEquivQuotientProdSubgroup.symm

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) : Function.Injective ⇑(AddSubgroup.inclusion h)

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) : Fintype G

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

Equations

• AddGroup.fintypeOfKerLeRange f g h = Fintype.ofEquiv ((G ⧸ g.ker) × ↥g.ker) AddSubgroup.addGroupEquivQuotientProdAddSubgroup.symm

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) : Fintype G

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

Equations

• Group.fintypeOfKerEqRange f g h = Group.fintypeOfKerLeRange f g ⋯

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) : Fintype G

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

Equations

• AddGroup.fintypeOfKerEqRange f g h = AddGroup.fintypeOfKerLeRange f g ⋯

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.fintypeOfKerOfCodom {G : Type u} {H : Type u} [Group G] [Group H] [Fintype H] (g : G →* H) [Fintype ↥g.ker] : Fintype G

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

Equations

• Group.fintypeOfKerOfCodom g = Group.fintypeOfKerLeRange (Subgroup.topEquiv.toMonoidHom.comp (Subgroup.inclusion ⋯)) g ⋯

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

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

Equations

• AddGroup.fintypeOfKerOfCodom g = AddGroup.fintypeOfKerLeRange (AddSubgroup.topEquiv.toAddMonoidHom.comp (AddSubgroup.inclusion ⋯)) g ⋯

theorem AddGroup.fintypeOfKerOfCodom.proof_1 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) : g.ker ≤ ⊤

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)] : Fintype G

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

Equations

• Group.fintypeOfDomOfCoker f = Group.fintypeOfKerLeRange f (QuotientGroup.mk' f.range) ⋯

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)] : Fintype G

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

Equations

• AddGroup.fintypeOfDomOfCoker f = AddGroup.fintypeOfKerLeRange f (QuotientAddGroup.mk' f.range) ⋯

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 = 0 → x ∈ f.range

theorem Finite.of_finite_quot_finite_subgroup {G : Type u} [Group G] {H : Subgroup G} [Finite ↥H] [Finite (G ⧸ H)] : Finite G

theorem Finite.of_finite_quot_finite_addSubgroup {G : Type u} [AddGroup G] {H : AddSubgroup G} [Finite ↥H] [Finite (G ⧸ H)] : Finite G