Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_SchurMultiplierTrivial.lean

definition module

Trivial Schur multiplier via stem extensions

The module introduces, in the Ihara namespace, a predicate expressing that a group has no non-trivial central stem extension. For a type G with a group structure, Ihara.HasTrivialSchurMultiplier G asserts: for every group E in the same universe as G and every homomorphism \pi \colon E \to G that is surjective and whose kernel is contained both in the centre of E and in the commutator subgroup [E,E], the kernel of \pi is trivial. Thus the predicate is a statement about all surjections onto G in one fixed universe, quantified over group structures on types of that universe, and it encodes the vanishing of the Schur multiplier in the form "every stem extension of G splits as the identity", rather than through any homological object; no second homology group is constructed here.

Three lemmas accompany the definition. Ihara.HasTrivialSchurMultiplier.of_mulEquiv transports the predicate backwards along a group isomorphism: if H satisfies it and e \colon G \simeq^* H is an isomorphism, then G satisfies it; the point is that composing a surjection onto G with e leaves the kernel, and the surjectivity, unchanged. Ihara.hasTrivialSchurMultiplier_of_isCyclic proves the predicate for every cyclic group G: given \pi as above with \ker \pi central, the quotient E/\ker\pi \cong G being cyclic forces E to be abelian (Mathlib's commutative_of_cyclic_center_quotient), so [E,E] is trivial and the hypothesis \ker \pi \le [E,E] gives \ker \pi = 1. Ihara.hasTrivialSchurMultiplier_of_subsingleton records the case of a group with at most one element, as an instance of the cyclic case.

Relation to Mathlib

Mathlib supplies the group-theoretic ingredients used (the commutator subgroup, Subgroup.center, and commutative_of_cyclic_center_quotient), but the predicate itself is the project's own: it is a stem-extension formulation, not a Mathlib notion of Schur multiplier or of second group homology.

Where it is used

The predicate is the interface in which the Schur-multiplier input about the groups \mathrm{SL}_2(\mathbb{Z}/q^n) is stated and consumed elsewhere in the development; the cyclic and trivial cases proved here serve as base cases and as reductions along isomorphisms.

References

  1. J. Mennicke, On Ihara's modular group, Annals of Mathematics 85 (1967), 294–297
  2. G. Karpilovsky, The Schur Multiplier, London Mathematical Society Monographs New Series 2, Oxford University Press, 1987
  3. I. Schur, Über die Darstellung der endlichen Gruppen durch gebrochene lineare Substitutionen, Journal für die reine und angewandte Mathematik 127 (1904), 20–50

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_SchurMultiplierTrivial.lean

Declarations

Source

import Mathlib.GroupTheory.Commutator.Basic ↗
import Mathlib.GroupTheory.QuotientGroup.Basic ↗
import Mathlib.GroupTheory.SpecificGroups.Cyclic ↗

open scoped commutatorElement

namespace Ihara

universe u

def HasTrivialSchurMultiplier (G : Type u) [Group G] : Prop :=
  ∀ (E : Type u) [Group E] (π : E →* G), Function.Surjective π →
    MonoidHom.ker π ≤ Subgroup.center E → MonoidHom.ker π ≤ commutator E →
      MonoidHom.ker π = ⊥

theorem HasTrivialSchurMultiplier.of_mulEquiv {G H : Type u} [Group G] [Group H]
    (hH : HasTrivialSchurMultiplier H) (e : G ≃* H) : HasTrivialSchurMultiplier G := by
  intro E _ π hsurj hcent hcomm
  have hker : MonoidHom.ker (e.toMonoidHom.comp π) = MonoidHom.ker π := by
    ext z
    simp only [MonoidHom.mem_ker, MonoidHom.comp_apply, MulEquiv.coe_toMonoidHom,
      MulEquiv.map_eq_one_iff]
  have hsurj' : Function.Surjective (e.toMonoidHom.comp π) := by
    rw [MonoidHom.coe_comp]; exact e.surjective.comp hsurj
  have h := hH E (e.toMonoidHom.comp π) hsurj'
    (by rw [hker]; exact hcent) (by rw [hker]; exact hcomm)
  rw [← hker]; exact h

theorem hasTrivialSchurMultiplier_of_isCyclic {G : Type u} [Group G] [IsCyclic G] :
    HasTrivialSchurMultiplier G := by
  intro E _ π hsurj hcent hcomm
  have hcommutative : ∀ a b : E, a * b = b * a :=
    commutative_of_cyclic_center_quotient π hcent
  have hbot : commutator E = ⊥ := by
    rw [eq_bot_iff, commutator_def, Subgroup.commutator_le]
    intro g₁ _ g₂ _
    rw [Subgroup.mem_bot, commutatorElement_eq_one_iff_mul_comm]
    exact hcommutative g₁ g₂
  rw [eq_bot_iff]; exact hcomm.trans hbot.le

theorem hasTrivialSchurMultiplier_of_subsingleton {G : Type u} [Group G] [Subsingleton G] :
    HasTrivialSchurMultiplier G :=
  hasTrivialSchurMultiplier_of_isCyclic

end Ihara

Statements phrased using this module (13)