Deducing finiteness of a 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 : 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
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)
:
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
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)
:
Fintype G
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 : 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 ⋯
Instances For
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 ⋯
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]
:
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 ⋯
Instances For
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) ⋯