Mathlib.GroupTheory.QuotientGroup.Finite

Group.fintypeOfKerLeRange definition

(h : g.ker ≤ f.range) : Fintype G

Full source

/-- If `F` and `H` are finite such that `ker(G →* H) ≤ im(F →* G)`, then `G` is finite. -/
@[to_additive "If `F` and `H` are finite such that `ker(G →+ H) ≤ im(F →+ G)`, then `G` is finite."]
noncomputable def fintypeOfKerLeRange (h : g.ker ≤ f.range) : Fintype G :=
  @Fintype.ofEquiv _ _
    (@instFintypeProd _ _ (Fintype.ofInjective _ <| kerLift_injective g) <|
      Fintype.ofInjective _ <| inclusion_injective h)
    groupEquivQuotientProdSubgroup.symm

Finiteness of a group via kernel containment in image

Informal description

If $F$ and $H$ are finite groups and the kernel of a group homomorphism $g \colon G \to H$ is contained in the image of a group homomorphism $f \colon F \to G$, then $G$ is finite.

Group.fintypeOfKerEqRange definition

(h : g.ker = f.range) : Fintype G

Full source

/-- If `F` and `H` are finite such that `ker(G →* H) = im(F →* G)`, then `G` is finite. -/
@[to_additive "If `F` and `H` are finite such that `ker(G →+ H) = im(F →+ G)`, then `G` is finite."]
noncomputable def fintypeOfKerEqRange (h : g.ker = f.range) : Fintype G :=
  fintypeOfKerLeRange _ _ h.le

Finiteness of a group via kernel-image equality

Informal description

If $F$ and $H$ are finite groups and the kernel of a group homomorphism $g \colon G \to H$ is equal to the image of a group homomorphism $f \colon F \to G$, then $G$ is finite.

Group.fintypeOfKerOfCodom definition

[Fintype g.ker] : Fintype G

Full source

/-- If `ker(G →* H)` and `H` are finite, then `G` is finite. -/
@[to_additive "If `ker(G →+ H)` and `H` are finite, then `G` is finite."]
noncomputable def fintypeOfKerOfCodom [Fintype g.ker] : Fintype G :=
  fintypeOfKerLeRange ((topEquiv : _ ≃* G).toMonoidHom.comp <| inclusion le_top) g fun x hx =>
    ⟨⟨x, hx⟩, rfl⟩

Finiteness of a group via finite kernel

Informal description

If the kernel of a group homomorphism $g \colon G \to H$ is finite, then $G$ is finite.

Group.fintypeOfDomOfCoker definition

[Normal f.range] [Fintype <| G ⧸ f.range] : Fintype G

Full source

/-- If `F` and `coker(F →* G)` are finite, then `G` is finite. -/
@[to_additive "If `F` and `coker(F →+ G)` are finite, then `G` is finite."]
noncomputable def fintypeOfDomOfCoker [Normal f.range] [Fintype <| G ⧸ f.range] : Fintype G :=
  fintypeOfKerLeRange _ (mk' f.range) fun x => (eq_one_iff x).mp

Finiteness of a group via finite domain and finite cokernel

Informal description

If $F$ is a finite group and the cokernel of a group homomorphism $f \colon F \to G$ is finite, then $G$ is finite. Here, the cokernel is the quotient group $G / \text{range}(f)$, and $\text{range}(f)$ is required to be a normal subgroup of $G$.

Finite.of_finite_quot_finite_subgroup theorem

{H : Subgroup G} [Finite H] [Finite (G ⧸ H)] : Finite G

Full source

@[to_additive]
lemma _root_.Finite.of_finite_quot_finite_subgroup {H : Subgroup G} [Finite H] [Finite (G ⧸ H)] :
    Finite G :=
  Finite.of_equiv _ (groupEquivQuotientProdSubgroup (s := H)).symm

Finiteness of a Group via Finite Subgroup and Quotient

Informal description

Let $G$ be a group and $H$ a subgroup of $G$. If both $H$ and the quotient group $G/H$ are finite, then $G$ itself is finite.