Documentation

Mathlib.NumberTheory.HeckeRing.Defs

Hecke rings: definitions #

This file introduces the abstract Hecke ring of a Hecke pair (H, Ξ”) and, more generally, the Hecke coset modules attached to a triple (H₁, Ξ”, Hβ‚‚), following [Shimura][shimura1971], Chapter 3, and [Krieg][krieg1990], Chapter I. It sets up the underlying types: the compatibility conditions IsHeckeTriple Ξ” H₁ Hβ‚‚ on a submonoid Ξ” of a group G and a pair of subgroups of G, the double-coset quotient HeckeCoset Ξ” H₁ Hβ‚‚ of Ξ” by H₁gHβ‚‚ = H₁hHβ‚‚, and the Hecke coset module HeckeCosetModule Ξ” H₁ Hβ‚‚ Z of formal finitely-supported linear combinations of double cosets. The convolution product HeckeCosetModule Ξ” H₁ Hβ‚‚ Z Γ— HeckeCosetModule Ξ” Hβ‚‚ H₃ Z β†’ HeckeCosetModule Ξ” H₁ H₃ Z and the ring structure on the diagonal Hecke ring 𝕋 Ξ” H Z are developed in later files.

The relevance of the submonoid Ξ” may not be immediately obvious; a natural example is H = GLβ‚‚(β„€) inside G = GLβ‚‚(β„š) with Ξ” the submonoid of integral matrices with nonzero determinant, which is the Hecke pair underlying the classical Hecke operators T_n. Mixed subgroups H₁ β‰  Hβ‚‚ arise for Hecke operators between different levels, e.g. H₁ = Ξ“β‚€(N) and Hβ‚‚ = Ξ“β‚€(M) inside the same Ξ”.

Main definitions #

Implementation notes #

The data (Ξ”, H₁, Hβ‚‚) enters unbundled, with the compatibility conditions collected in the Prop-valued class IsHeckeTriple: the types HeckeCoset Ξ” H₁ Hβ‚‚ and HeckeCosetModule Ξ” H₁ Hβ‚‚ Z are built from the data alone and depend on no proofs, and a single ambient Ξ” shared by all levels (as in [Shimura][shimura1971]) means products of double cosets over different subgroups, H₁g₁Hβ‚‚ * Hβ‚‚gβ‚‚H₃ βŠ† Ξ”, need no compatibility hypotheses. The conditions are only needed for the finiteness of the coset decompositions, which enters through the Fintype instance on DoubleCoset.DecompQuotient in later files. Requiring Ξ” to be a submonoid rather than a subsemigroup loses no generality, since H₁ ≀ Ξ” already forces 1 ∈ Ξ”.

References #

source
class IsHeckeTriple {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) :
Prop

A Hecke triple (H₁, Ξ”, Hβ‚‚): the compatibility conditions on a submonoid Ξ” and a pair of subgroups H₁, Hβ‚‚ of G making the double cosets H₁\Ξ”/Hβ‚‚ finite unions of left cosets: both subgroups are contained in Ξ”, they are commensurable, and Ξ” commensurates them. The classical Hecke pair (H, Ξ”) of [Shimura][shimura1971], Chapter 3, is the diagonal case IsHeckeTriple Ξ” H H.

Instances
    source
    theorem IsHeckeTriple.of_diagonal {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H : Subgroup G} (h : H.toSubmonoid ≀ Ξ”) (hc : Ξ” ≀ (Subgroup.Commensurable.commensurator H).toSubmonoid) :
    IsHeckeTriple Ξ” H H

    The Hecke triple (H, Ξ”, H) coming from a pair (H, Ξ”) with H ≀ Ξ” ≀ commensurator H.

    source
    theorem IsHeckeTriple.mem_of_mem_left {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ : Subgroup G} (Hβ‚‚ : Subgroup G) [IsHeckeTriple Ξ” H₁ Hβ‚‚] {x : G} (hx : x ∈ H₁) :
    x ∈ Ξ”

    Elements of the left subgroup lie in Ξ”.

    source
    theorem IsHeckeTriple.mem_of_mem_right {G : Type u_1} [Group G] {Ξ” : Submonoid G} {Hβ‚‚ : Subgroup G} (H₁ : Subgroup G) [IsHeckeTriple Ξ” H₁ Hβ‚‚] {x : G} (hx : x ∈ Hβ‚‚) :
    x ∈ Ξ”

    Elements of the right subgroup lie in Ξ”.

    source
    theorem IsHeckeTriple.le_commensurator_left {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ : Subgroup G} (Hβ‚‚ : Subgroup G) [h : IsHeckeTriple Ξ” H₁ Hβ‚‚] :
    Ξ” ≀ (Subgroup.Commensurable.commensurator H₁).toSubmonoid

    The submonoid Ξ” lies in the commensurator of the left subgroup.

    source
    theorem IsHeckeTriple.mem_commensurator_right {G : Type u_1} [Group G] {Ξ” : Submonoid G} {Hβ‚‚ : Subgroup G} (H₁ : Subgroup G) [IsHeckeTriple Ξ” H₁ Hβ‚‚] (g : β†₯Ξ”) :
    ↑g ∈ Subgroup.Commensurable.commensurator Hβ‚‚

    Elements of Ξ” lie in the commensurator of the right subgroup.

    source
    theorem IsHeckeTriple.mem_commensurator_left {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ : Subgroup G} (Hβ‚‚ : Subgroup G) [IsHeckeTriple Ξ” H₁ Hβ‚‚] (g : β†₯Ξ”) :
    ↑g ∈ Subgroup.Commensurable.commensurator H₁

    Elements of Ξ” lie in the commensurator of the left subgroup.

    source
    theorem IsHeckeTriple.commensurable_conjAct_right {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ : Subgroup G} [IsHeckeTriple Ξ” H₁ Hβ‚‚] (g : β†₯Ξ”) :
    (ConjAct.toConjAct ↑g β€’ Hβ‚‚).Commensurable H₁

    Conjugating the right subgroup of a Hecke triple (H₁, Ξ”, Hβ‚‚) by an element of Ξ” gives a subgroup commensurable with the left one.

    source
    theorem IsHeckeTriple.trans {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ H₃ : Subgroup G} [IsHeckeTriple Ξ” H₁ Hβ‚‚] [IsHeckeTriple Ξ” Hβ‚‚ H₃] :
    IsHeckeTriple Ξ” H₁ H₃

    Hecke coset module data compose. Not an instance, since the middle subgroup cannot be inferred from the goal.

    source
    theorem IsHeckeTriple.diag_left {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ : Subgroup G} [IsHeckeTriple Ξ” H₁ Hβ‚‚] :
    IsHeckeTriple Ξ” H₁ H₁

    The left diagonal datum (H₁, Ξ”, H₁). Not an instance, since Hβ‚‚ cannot be inferred.

    source
    theorem IsHeckeTriple.diag_right {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ : Subgroup G} [IsHeckeTriple Ξ” H₁ Hβ‚‚] :
    IsHeckeTriple Ξ” Hβ‚‚ Hβ‚‚

    The right diagonal datum (Hβ‚‚, Ξ”, Hβ‚‚). Not an instance, since H₁ cannot be inferred.

    source
    @[reducible, inline]
    abbrev HeckeCoset.setoid {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) :
    Setoid β†₯Ξ”

    The setoid on Ξ” identifying elements with the same double coset H₁gHβ‚‚ = H₁hHβ‚‚, pulled back from DoubleCoset.setoid along the inclusion Ξ” β†ͺ G.

    This is an abbrev rather than a global instance: the subgroups H₁, Hβ‚‚ cannot be inferred from the submonoid Ξ”, so this cannot participate in instance search (and a global instance would also create a Setoid diamond on β†₯Ξ” with the left-coset setoid). The quotient map is HeckeCoset.mk.

    Equations
    Instances For
      source
      def HeckeCoset {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) :
      Type u_1

      A Hecke double coset: an equivalence class of Ξ”-elements under H₁gHβ‚‚ = H₁hHβ‚‚. This is the basis type for the HeckeCosetModule.

      Equations
      Instances For
        source
        def HeckeCoset.mk {G : Type u_1} [Group G] {Ξ” : Submonoid G} (H₁ Hβ‚‚ : Subgroup G) (g : β†₯Ξ”) :
        HeckeCoset Ξ” H₁ Hβ‚‚

        The double coset H₁gHβ‚‚ of an element g : Ξ”.

        Equations
        Instances For
          source
          @[implicit_reducible]
          instance HeckeCoset.instInhabited {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) :
          Inhabited (HeckeCoset Ξ” H₁ Hβ‚‚)
          Equations
          source
          @[implicit_reducible]
          instance HeckeCoset.instOne {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H : Subgroup G) :
          One (HeckeCoset Ξ” H H)

          The identity double coset H1H = H of the diagonal (Hecke pair) case.

          Equations
          source
          theorem HeckeCoset.one_def {G : Type u_1} [Group G] {Ξ” : Submonoid G} (H : Subgroup G) :
          1 = mk H H ⟨1, β‹―βŸ©
          source
          def HeckeCosetModule {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) (Z : Type u_2) [Zero Z] :
          Type (max u_2 u_1)

          The Hecke coset module with coefficients in Z: the finitely-supported Z-linear combinations of double cosets H₁\Ξ”/Hβ‚‚. For H₁ = Hβ‚‚ this is the underlying module of the Hecke ring 𝕋 Ξ” H Z (see HeckeRing). The coefficients Z need only carry a Zero for the type to make sense; algebraic structure is added by the instances below at the weakest level each requires.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev HeckeRing {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H : Subgroup G) (Z : Type u_2) [Zero Z] :
            Type (max u_2 u_1)

            The Hecke ring 𝕋 Ξ” H Z with coefficients in Z: the diagonal Hecke coset module HeckeCosetModule Ξ” H H Z, the finitely-supported Z-linear combinations of double cosets H\Ξ”/H. The convolution product making it a ring is developed in later files.

            Equations
            Instances For
              source
              def HeckeCosetModule.term𝕋 :
              Lean.ParserDescr

              The Hecke ring 𝕋 Ξ” H Z with coefficients in Z: the diagonal Hecke coset module HeckeCosetModule Ξ” H H Z, the finitely-supported Z-linear combinations of double cosets H\Ξ”/H. The convolution product making it a ring is developed in later files.

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance HeckeCosetModule.instFunLikeHeckeCoset {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) (Z : Type u_2) [Zero Z] :
                FunLike (HeckeCosetModule Ξ” H₁ Hβ‚‚ Z) (HeckeCoset Ξ” H₁ Hβ‚‚) Z

                Elements of HeckeCosetModule Ξ” H₁ Hβ‚‚ Z are functions HeckeCoset Ξ” H₁ Hβ‚‚ β†’ Z (finitely supported).

                Equations
                source
                @[implicit_reducible]
                noncomputable instance HeckeCosetModule.instAddCommMonoid {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) (Z : Type u_2) [AddCommMonoid Z] :
                AddCommMonoid (HeckeCosetModule Ξ” H₁ Hβ‚‚ Z)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                @[implicit_reducible]
                noncomputable instance HeckeCosetModule.instAddCommGroup {G : Type u_1} [Group G] (Ξ” : Submonoid G) (H₁ Hβ‚‚ : Subgroup G) (Z : Type u_2) [AddCommGroup Z] :
                AddCommGroup (HeckeCosetModule Ξ” H₁ Hβ‚‚ Z)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                def HeckeCosetModule.of {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ : Subgroup G} {Z : Type u_3} [Zero Z] :
                (HeckeCoset Ξ” H₁ Hβ‚‚ β†’β‚€ Z) ≃ HeckeCosetModule Ξ” H₁ Hβ‚‚ Z

                The sanctioned constructor of HeckeCosetModule Ξ” H₁ Hβ‚‚ Z from a finitely-supported function on double cosets. Build elements through of rather than relying on the definitional unfolding HeckeCosetModule Ξ” H₁ Hβ‚‚ Z = (HeckeCoset Ξ” H₁ Hβ‚‚ β†’β‚€ Z).

                Equations
                Instances For
                  source
                  @[simp]
                  theorem HeckeCosetModule.of_apply {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ : Subgroup G} {Z : Type u_3} [Zero Z] (f : HeckeCoset Ξ” H₁ Hβ‚‚ β†’β‚€ Z) (D : HeckeCoset Ξ” H₁ Hβ‚‚) :
                  (of f) D = f D
                  source
                  theorem HeckeCosetModule.ext {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ : Subgroup G} {Z : Type u_3} [Zero Z] {f g : HeckeCosetModule Ξ” H₁ Hβ‚‚ Z} (h : βˆ€ (D : HeckeCoset Ξ” H₁ Hβ‚‚), f D = g D) :
                  f = g
                  source
                  theorem HeckeCosetModule.ext_iff {G : Type u_1} [Group G] {Ξ” : Submonoid G} {H₁ Hβ‚‚ : Subgroup G} {Z : Type u_3} [Zero Z] {f g : HeckeCosetModule Ξ” H₁ Hβ‚‚ Z} :
                  f = g ↔ βˆ€ (D : HeckeCoset Ξ” H₁ Hβ‚‚), f D = g D