Other results
Results named in the rest of Tau Ceti's TauCeti.GroupTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremArtin's identity for fixed points#
weighting the permutation character of G ⧸ C by
C.artinCoeff * |C| and summing over all subgroups gives |G|, at every g : G.
TauCeti.sum_artinCoeff_mul_card_fixedBy.{u_1} {G : Type u_1} [Group G] [Finite G] (g : G) :
∑ᶠ (C : Subgroup G), C.artinCoeff * ↑(Nat.card ↥C) * ↑(Nat.card ↑(MulAction.fixedBy (G ⧸ C) g)) =
↑(Nat.card G)
TheoremEuler's theorem on an n-th root of unity#
if x ^ n = 1 in a monoid and q is prime to
n, then x ^ q ^ φ(n) = x, since q ^ φ(n) ≡ 1 [MOD n].
TauCeti.pow_pow_totient_eq_self.{u_1} {M : Type u_1} [Monoid M] {q n : ℕ} (hq : q.Coprime n) {x : M}
(hx : x ^ n = 1) : x ^ q ^ n.totient = x
Used by 15
m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · Hilbert reciprocity · Quadratic reciprocity is Hilbert reciprocity for two odd primes · The global class formation · The global invariant · The global invariant is injective · Serre's mass formula for quadratic extensions in odd residue characteristic · Serre's mass formula for the quadratic extensions of ℚ_2 · The totally ramified quadratic extensions of ℚ_2 · Iwasawa's theorem · Tame inertia is procyclic · Tame inertia is the prime-to-p Tate module · Hilbert's product formula · The Kronecker–Weber theorem · The finite level of the generator theorem (NSW, proof of (7.4.1))TheoremFurtwängler's theorem, the group-theoretic principal ideal theorem#
if the commutator
subgroup G' of G is finitely generated and of finite index (for instance if G is finite),
the transfer G → A of every homomorphism ϕ : G' →* A to a commutative group is trivial. For
ϕ the abelianization map, this says that the transfer G → G' ⧸ G'' is trivial.
MonoidHom.transfer_commutator_eq_one.{u_1} {G : Type} [Group G] [Group.FG ↥(commutator G)]
[(commutator G).FiniteIndex] {A : Type u_1} [CommGroup A] (ϕ : ↥(commutator G) →* A) :
ϕ.transfer = 1
Uses 1 · Used by 1
ℤTheoremGaschütz's counting lemma#
For a subgroup K of a finite group G, the number of
ι-tuples that generate K and lift a given generating tuple of H along f does not depend on
that generating tuple.
MonoidHom.card_comp_eq_and_closure_range_eq_congr.{u_1, u_2, u_3} {G : Type u_1} {H : Type u_2}
{ι : Type u_3} [Group G] [Group H] (f : G →* H) [Finite G] [Finite ι] (K : Subgroup G)
{h h' : ι → H} (hh : Subgroup.closure (Set.range h) = ⊤)
(hh' : Subgroup.closure (Set.range h') = ⊤) :
Nat.card { x // ⇑f ∘ x = h ∧ Subgroup.closure (Set.range x) = K } =
Nat.card { x // ⇑f ∘ x = h' ∧ Subgroup.closure (Set.range x) = K }
Lean
Formalized in Tau Ceti as MonoidHom.card_comp_eq_and_closure_range_eq_congr.
Sources
Used by 1
TheoremGaschütz's lemma#
Let f : G →* H be a surjective homomorphism from a finite group, and
let G be generated by an ι-tuple. Then every generating ι-tuple of H lifts along f to a
generating ι-tuple of G.
MonoidHom.exists_comp_eq_and_closure_range_eq_top_of_surjective.{u_1, u_2, u_3} {G : Type u_1}
{H : Type u_2} {ι : Type u_3} [Group G] [Group H] (f : G →* H) [Finite G] [Finite ι]
(hf : Function.Surjective ⇑f) {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) {h : ι → H}
(hh : Subgroup.closure (Set.range h) = ⊤) :
∃ g', ⇑f ∘ g' = h ∧ Subgroup.closure (Set.range g') = ⊤
Lean
Formalized in Tau Ceti as MonoidHom.exists_comp_eq_and_closure_range_eq_top_of_surjective.
Sources
Uses 1 · Used by 1
TheoremGrün's lemma for the recipe#
when the derived subgroup is perfect, the derived central quotient has trivial centre.
This is the reason the two steps compose in the stated order: the centre is removed once and for all, and does not reappear.
TauCeti.DerivedCentralQuotient.center_eq_bot.{u_1} {G : Type u_1} [Group G]
[Group.IsPerfect ↥(commutator G)] : Subgroup.center (TauCeti.DerivedCentralQuotient G) = ⊥
TheoremHowson's theorem#
in a free group, the intersection of two finitely generated subgroups is finitely generated.
Subgroup.FG.inf_of_isFreeGroup.{u_1} {G : Type u_1} [Group G] [IsFreeGroup G] {H K : Subgroup G}
(hH : H.FG) (hK : K.FG) : (H ⊓ K).FG
TheoremMalcev's theorem#
A surjective endomorphism of a finitely generated residually finite group is injective: such a group is Hopfian.
Group.ResiduallyFinite.injective_of_surjective.{u_1} {G : Type u_1} [Group G] [Group.FG G]
[Group.ResiduallyFinite G] {f : G →* G} (hf : Function.Surjective ⇑f) : Function.Injective ⇑f
TheoremSchreier's index formula#
If H has finite index n in a group generated by a finite set
S of d elements, then H is generated by at most 1 + n * (d - 1) elements. This sharpens
Mathlib's Subgroup.exists_finset_card_le_mul, which gives n * d.
Subgroup.exists_finset_card_le_one_add_index_mul.{u_1} {G : Type u_1} [Group G] (H : Subgroup G)
[H.FiniteIndex] {S : Finset G} (hS : Subgroup.closure ↑S = ⊤) :
∃ T, T.card ≤ 1 + H.index * (S.card - 1) ∧ Subgroup.closure ↑T = ⊤
Lean
Formalized in Tau Ceti as Subgroup.exists_finset_card_le_one_add_index_mul.
Other forms
Schreier's index formula for Group.rank. Formalized in Tau Ceti as Subgroup.rank_le_one_add_index_mul_rank_sub_one.
Subgroup.rank_le_one_add_index_mul_rank_sub_one.{u_1} {G : Type u_1} [Group G] {H : Subgroup G}
[Group.FG G] [H.FiniteIndex] : Group.rank ↥H ≤ 1 + H.index * (Group.rank G - 1)
Sources
Used by 1
TheoremTarski's alternative#
a discrete group is amenable exactly when it is not paradoxical for its left regular action.
TauCeti.amenable_iff_not_paradoxical_univ.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
[IsTopologicalGroup G] [DiscreteTopology G] : TauCeti.Amenable G ↔ ¬TauCeti.Paradoxical G Set.univ
Lean
Formalized in Tau Ceti as TauCeti.amenable_iff_not_paradoxical_univ.
Other forms
Tarski's alternative, topology-free form. Formalized in Tau Ceti as TauCeti.hasFoelnerSets_iff_not_paradoxical_univ.
TauCeti.hasFoelnerSets_iff_not_paradoxical_univ.{u_1} {G : Type u_1} [Group G] :
TauCeti.HasFoelnerSets G ↔ ¬TauCeti.Paradoxical G Set.univ
Sources
DefinitionThe third isomorphism theorem for coset spaces#
For a normal N and an arbitrary
subgroup H, the cosets of the image of H in G ⧸ N are the cosets of H ⊔ N in G, both
directions sending the class of g to the class of g.
Mathlib's QuotientGroup.quotientQuotientEquivQuotient is the group isomorphism this
generalises: it asks for N ≤ M with M normal, so that both sides are groups and the map is a
homomorphism. Here neither side need be a group — H is unconstrained — and what survives is the
bijection of coset spaces, which is what a coset-indexed sum or family needs.
QuotientGroup.quotientQuotientEquivQuotientSup.{u_1} {G : Type u_1} [Group G] (H N : Subgroup G)
[N.Normal] : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) H ≃ G ⧸ H ⊔ N
Lean
Formalized in Tau Ceti as QuotientGroup.quotientQuotientEquivQuotientSup.
Other forms
The third isomorphism theorem for coset spaces, additive version. Formalized in Tau Ceti as QuotientAddGroup.quotientQuotientEquivQuotientSup.
QuotientAddGroup.quotientQuotientEquivQuotientSup.{u_1} {G : Type u_1} [AddGroup G]
(H N : AddSubgroup G) [N.Normal] :
(G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) H ≃ G ⧸ H ⊔ N
Sources
Used by 15
A(L) · A newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue a_p(f) · Global existence (Milne VII, Theorem 9.5) · The Kronecker–Weber theorem · Hasse--Arf in prime degree · The finite level of the generator theorem (NSW, proof of (7.4.1)) · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3) · The Petersson adjoint formula in the second argument · Lagrange's theorem for profinite groups · The existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10)) · The necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1)Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.