Congruence subgroups for a modulus

StructureCongruence subgroup#✓fully proved

Let \(K\) be a number field and \(\mathfrak m\) a modulus of \(K\). A congruence subgroup for \(\mathfrak m\) is a subgroup \(H\) of the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) such that \(H\) contains the ray group of \(\mathfrak m\).

@[ext] structure CongruenceSubgroup (m : Modulus K) where
  /-- Underlying subgroup of the coprime ideals. -/
  toSubgroup : Subgroup (coprimeFractionalIdeals m)
  /-- The ray group is contained in the subgroup. -/
  rayGroup_le : rayGroup m ≤ toSubgroup

Uses 2 · Used by 16

Statement usesFractional ideals coprime to a modulus · The ray group of a modulus

Used byChange of modulus of a congruence subgroup · The change of modulus is equivalent to the original pair · Ambient subgroup of a change of modulus · Ambient subgroup of a change of modulus to a divisor · Congruence subgroup pair · Criterion for an equivalent congruence subgroup at a divisor of the modulus · Image of a congruence subgroup in the ray class group · Equivalence of congruence subgroup pairs · Criterion for equivalence of congruence subgroup pairs · Largest congruence subgroup · Membership in the image of a congruence subgroup · A congruence subgroup contains the ray group · Equivalence of congruence subgroup pairs is reflexive · Smallest congruence subgroup · Equivalence of congruence subgroup pairs is symmetric · Congruence subgroup as a subgroup of all invertible fractional ideals

DefinitionImage of a congruence subgroup in the ray class group#✓fully proved

Let \(H\) be a congruence subgroup for a modulus \(\mathfrak m\) of a number field \(K\), and let \(\pi\) be the canonical projection from the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) onto the ray class group of \(\mathfrak m\). The image of \(H\) is the subgroup \(\pi(H)\) of the ray class group.

def image (C : CongruenceSubgroup (K := K) m) :
    Subgroup (RayClassGroup m) :=
  C.toSubgroup.map (rayClassMap m)

Uses 5 · Used by 1

Statement usesCongruence subgroup · Ray class group · Fractional ideals coprime to a modulus · Ray class map · The ray group of a modulus

Used byMembership in the image of a congruence subgroup

TheoremMembership in the image of a congruence subgroup#✓fully proved

Let \(H\) be a congruence subgroup for a modulus \(\mathfrak m\) of a number field \(K\), and let \(\pi\) be the canonical projection from the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) onto the ray class group of \(\mathfrak m\). An element \(x\) of the ray class group lies in the image \(\pi(H)\) if and only if \(\pi(y) = x\) for some \(y \in H\).

theorem mem_image_iff (C : CongruenceSubgroup (K := K) m)
    (x : RayClassGroup m) :
    x ∈ C.image ↔ ∃ y ∈ C.toSubgroup, rayClassMap m y = x

Uses 6

Statement usesCongruence subgroup · Image of a congruence subgroup in the ray class group · Ray class group · Fractional ideals coprime to a modulus · Ray class map · The ray group of a modulus

DefinitionCongruence subgroup as a subgroup of all invertible fractional ideals#✓fully proved

For a congruence subgroup \(H\) for a modulus \(\mathfrak m\) of a number field \(K\), this is the image of \(H\) under the inclusion of the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) into the group of all invertible fractional ideals of \(K\).

def toAmbientSubgroup (C : CongruenceSubgroup (K := K) m) :
    Subgroup ((FractionalIdeal (𝓞 K)⁰ K)ˣ) :=
  C.toSubgroup.map (coprimeFractionalIdeals m).subtype

Uses 2 · Used by 10

Statement usesCongruence subgroup · Fractional ideals coprime to a modulus

Used byChange of modulus of a congruence subgroup · The change of modulus is equivalent to the original pair · Ambient subgroup of a change of modulus · Ambient subgroup of a change of modulus to a divisor · Criterion for an equivalent congruence subgroup at a divisor of the modulus · Equivalence of congruence subgroup pairs · Criterion for equivalence of congruence subgroup pairs · A congruence subgroup contains the ray group · Equivalence of congruence subgroup pairs is reflexive · Equivalence of congruence subgroup pairs is symmetric

DefinitionSmallest congruence subgroup#✓fully proved

For a modulus \(\mathfrak m\) of a number field \(K\), the smallest congruence subgroup for \(\mathfrak m\) is the ray group of \(\mathfrak m\) itself, a subgroup of the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\).

def smallest (m : Modulus K) : CongruenceSubgroup (K := K) m :=
  ⟨rayGroup m, le_rfl⟩

Uses 3

Statement usesCongruence subgroup · Fractional ideals coprime to a modulus · The ray group of a modulus

DefinitionLargest congruence subgroup#✓fully proved

For a modulus \(\mathfrak m\) of a number field \(K\), the largest congruence subgroup for \(\mathfrak m\) is the whole group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\), which contains the ray group of \(\mathfrak m\).

def largest (m : Modulus K) : CongruenceSubgroup (K := K) m :=
  ⟨⊤, le_top⟩

Uses 3

Statement usesCongruence subgroup · Fractional ideals coprime to a modulus · The ray group of a modulus

StructureCongruence subgroup pair#✓fully proved

Let \(K\) be a number field. A congruence subgroup pair for \(K\) consists of a modulus \(\mathfrak m\) of \(K\) together with a congruence subgroup for \(\mathfrak m\), that is, a subgroup of the group of invertible fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) that contains the ray group of \(\mathfrak m\).

structure CongruenceSubgroupPair (K : Type*) [Field K] [NumberField K] where
  /-- The modulus of the pair. -/
  modulus : Modulus K
  /-- The congruence subgroup for `modulus`. -/
  subgroup : CongruenceSubgroup modulus

Uses 1 · Used by 6

Statement usesCongruence subgroup

Used byThe change of modulus is equivalent to the original pair · Criterion for an equivalent congruence subgroup at a divisor of the modulus · Equivalence of congruence subgroup pairs · Criterion for equivalence of congruence subgroup pairs · Equivalence of congruence subgroup pairs is reflexive · Equivalence of congruence subgroup pairs is symmetric

DefinitionEquivalence of congruence subgroup pairs#✓fully proved

Let \(K\) be a number field. For a modulus \(\mathfrak m\) of \(K\), write \(I^{\mathfrak m}\) for the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). Two pairs \((\mathfrak m, H)\) and \((\mathfrak n, H')\), each consisting of a modulus of \(K\) and a congruence subgroup for it, are equivalent when \(I^{\mathfrak m} \cap H' = I^{\mathfrak n} \cap H\), where both congruence subgroups are viewed as subgroups of the group of all nonzero fractional ideals of \(K\).

def IsEquivalent (P Q : CongruenceSubgroupPair K) : Prop :=
  coprimeFractionalIdeals P.modulus ⊓ Q.subgroup.toAmbientSubgroup =
    coprimeFractionalIdeals Q.modulus ⊓ P.subgroup.toAmbientSubgroup

Uses 4 · Used by 5

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Congruence subgroup pair · Fractional ideals coprime to a modulus

Used byThe change of modulus is equivalent to the original pair · Criterion for an equivalent congruence subgroup at a divisor of the modulus · Criterion for equivalence of congruence subgroup pairs · Equivalence of congruence subgroup pairs is reflexive · Equivalence of congruence subgroup pairs is symmetric

TheoremCriterion for equivalence of congruence subgroup pairs#✓fully proved

Let \(K\) be a number field, and for a modulus \(\mathfrak m\) of \(K\) write \(I^{\mathfrak m}\) for the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\). Two pairs \((\mathfrak m, H)\) and \((\mathfrak n, H')\), each consisting of a modulus of \(K\) and a congruence subgroup for it, are equivalent if and only if \(I^{\mathfrak m} \cap H' = I^{\mathfrak n} \cap H\) in the group of all nonzero fractional ideals of \(K\).

theorem isEquivalent_iff (P Q : CongruenceSubgroupPair K) :
    IsEquivalent P Q ↔
      coprimeFractionalIdeals P.modulus ⊓ Q.subgroup.toAmbientSubgroup =
        coprimeFractionalIdeals Q.modulus ⊓ P.subgroup.toAmbientSubgroup

Uses 5 · Used by 1

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Congruence subgroup pair · Equivalence of congruence subgroup pairs · Fractional ideals coprime to a modulus

Used byCriterion for an equivalent congruence subgroup at a divisor of the modulus

TheoremEquivalence of congruence subgroup pairs is reflexive#✓fully proved

Let \(K\) be a number field. Every pair consisting of a modulus of \(K\) and a congruence subgroup for it is equivalent to itself.

theorem IsEquivalent.refl (P : CongruenceSubgroupPair K) :
    IsEquivalent P P

Uses 5

Statement usesCongruence subgroup pair · Equivalence of congruence subgroup pairs

Proof usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Fractional ideals coprime to a modulus

TheoremEquivalence of congruence subgroup pairs is symmetric#✓fully proved

Let \(K\) be a number field. If a pair \(P\), consisting of a modulus of \(K\) and a congruence subgroup for it, is equivalent to such a pair \(Q\), then \(Q\) is equivalent to \(P\).

theorem IsEquivalent.symm {P Q : CongruenceSubgroupPair K} :
    IsEquivalent P Q → IsEquivalent Q P

Uses 5

Statement usesCongruence subgroup pair · Equivalence of congruence subgroup pairs

Proof usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Fractional ideals coprime to a modulus

DefinitionRay group among all fractional ideals#✓fully proved

For a modulus \(\mathfrak m\) of a number field \(K\), the ambient ray group of \(\mathfrak m\) is the image of the ray group of \(\mathfrak m\) under the inclusion of the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m\) into the group of all nonzero fractional ideals of \(K\).

def rayGroupAmbient (m : Modulus K) : Subgroup ((FractionalIdeal (𝓞 K)⁰ K)ˣ) :=
  (rayGroup m).map (coprimeFractionalIdeals m).subtype

Uses 2 · Used by 6

Statement usesFractional ideals coprime to a modulus · The ray group of a modulus

Used byThe change of modulus is equivalent to the original pair · Ambient subgroup of a change of modulus · Ambient subgroup of a change of modulus to a divisor · Criterion for an equivalent congruence subgroup at a divisor of the modulus · The ray group consists of coprime ideals · A congruence subgroup contains the ray group

TheoremThe ray group consists of coprime ideals#✓fully proved

For every modulus \(\mathfrak m\) of a number field \(K\), the ray group of \(\mathfrak m\), viewed as a subgroup of the group of nonzero fractional ideals of \(K\), is contained in the group of nonzero fractional ideals coprime to the finite part of \(\mathfrak m\).

theorem rayGroupAmbient_le_coprime (m : Modulus K) :
    rayGroupAmbient m ≤ coprimeFractionalIdeals m

Uses 3

Statement usesFractional ideals coprime to a modulus · Ray group among all fractional ideals

Proof usesThe ray group of a modulus

TheoremA congruence subgroup contains the ray group#✓fully proved

Let \(C\) be a congruence subgroup for a modulus \(\mathfrak m\) of a number field \(K\). Viewed as subgroups of the group of nonzero fractional ideals of \(K\), the ray group of \(\mathfrak m\) is contained in \(C\).

theorem CongruenceSubgroup.rayGroupAmbient_le_toAmbientSubgroup
    {m : Modulus K} (C : CongruenceSubgroup m) :
    rayGroupAmbient m ≤ C.toAmbientSubgroup

Uses 5 · Used by 1

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Ray group among all fractional ideals

Proof usesFractional ideals coprime to a modulus · The ray group of a modulus

Used byCriterion for an equivalent congruence subgroup at a divisor of the modulus

TheoremCoprimality passes to divisors of a modulus#✓fully proved

Let \(\mathfrak m_1\) and \(\mathfrak m_2\) be moduli of a number field \(K\) with \(\mathfrak m_2 \mid \mathfrak m_1\). Then every nonzero fractional ideal of \(K\) coprime to the finite part of \(\mathfrak m_1\) is coprime to the finite part of \(\mathfrak m_2\).

theorem coprimeFractionalIdeals_le_of_dvd {m1 m2 : Modulus K}
    (h : m2 ∣ m1) :
    coprimeFractionalIdeals m1 ≤ coprimeFractionalIdeals m2

Uses 2 · Used by 3

Statement usesFractional ideals coprime to a modulus

Proof usesPrimes dividing a modulus

Used byThe change of modulus is equivalent to the original pair · Ambient subgroup of a change of modulus to a divisor · Criterion for an equivalent congruence subgroup at a divisor of the modulus

DefinitionChange of modulus of a congruence subgroup#✓fully proved

Let \(C_1\) be a congruence subgroup for a modulus \(\mathfrak m_1\) of a number field \(K\), viewed as a subgroup of the group of nonzero fractional ideals of \(K\), and let \(\mathfrak m_2\) be any modulus of \(K\). Write \(I^{\mathfrak m_2}\) for the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m_2\) and \(P_{\mathfrak m_2} \subseteq I^{\mathfrak m_2}\) for the ray group of \(\mathfrak m_2\). The change of modulus of \(C_1\) to \(\mathfrak m_2\) is the congruence subgroup for \(\mathfrak m_2\) generated, inside \(I^{\mathfrak m_2}\), by \(C_1 \cap I^{\mathfrak m_2}\) and \(P_{\mathfrak m_2}\).

def changeModulus {m1 : Modulus K} (C1 : CongruenceSubgroup m1)
    (m2 : Modulus K) : CongruenceSubgroup m2 where
  toSubgroup :=
    C1.toAmbientSubgroup.comap (coprimeFractionalIdeals m2).subtype ⊔
      rayGroup m2
  rayGroup_le := le_sup_right

Uses 4 · Used by 4

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Fractional ideals coprime to a modulus · The ray group of a modulus

Used byThe change of modulus is equivalent to the original pair · Ambient subgroup of a change of modulus · Ambient subgroup of a change of modulus to a divisor · Criterion for an equivalent congruence subgroup at a divisor of the modulus

TheoremAmbient subgroup of a change of modulus#✓fully proved

Let \(\mathfrak m_1\) and \(\mathfrak m_2\) be moduli of a number field \(K\) and let \(C_1\) be a congruence subgroup for \(\mathfrak m_1\). Write \(I^{\mathfrak m_2}\) for the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m_2\) and \(P_{\mathfrak m_2}\) for the ray group of \(\mathfrak m_2\). Viewing all of these as subgroups of the group of nonzero fractional ideals of \(K\), the change of modulus of \(C_1\) to \(\mathfrak m_2\) is the subgroup generated by \(C_1 \cap I^{\mathfrak m_2}\) and \(P_{\mathfrak m_2}\).

theorem changeModulus_toAmbientSubgroup {m1 m2 : Modulus K}
    (C1 : CongruenceSubgroup m1) :
    (changeModulus C1 m2).toAmbientSubgroup =
      (C1.toAmbientSubgroup ⊓ coprimeFractionalIdeals m2) ⊔
        rayGroupAmbient m2

Uses 6 · Used by 1

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Change of modulus of a congruence subgroup · Fractional ideals coprime to a modulus · Ray group among all fractional ideals

Proof usesThe ray group of a modulus

Used byAmbient subgroup of a change of modulus to a divisor

TheoremAmbient subgroup of a change of modulus to a divisor#✓fully proved

Let \(\mathfrak m_1\) and \(\mathfrak m_2\) be moduli of a number field \(K\) with \(\mathfrak m_2 \mid \mathfrak m_1\), and let \(C_1\) be a congruence subgroup for \(\mathfrak m_1\). Viewed as subgroups of the group of nonzero fractional ideals of \(K\), the change of modulus of \(C_1\) to \(\mathfrak m_2\) equals the subgroup generated by \(C_1\) and the ray group \(P_{\mathfrak m_2}\) of \(\mathfrak m_2\).

theorem changeModulus_toAmbientSubgroup_of_dvd {m1 m2 : Modulus K}
    (C1 : CongruenceSubgroup m1) (hdiv : m2 ∣ m1) :
    (changeModulus C1 m2).toAmbientSubgroup =
      C1.toAmbientSubgroup ⊔ rayGroupAmbient m2

Uses 7 · Used by 1

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Change of modulus of a congruence subgroup · Ray group among all fractional ideals

Proof usesAmbient subgroup of a change of modulus · Fractional ideals coprime to a modulus · Coprimality passes to divisors of a modulus

Used byThe change of modulus is equivalent to the original pair

TheoremThe change of modulus is equivalent to the original pair#✓fully proved

Let \(\mathfrak m_1\) and \(\mathfrak m_2\) be moduli of a number field \(K\) with \(\mathfrak m_2 \mid \mathfrak m_1\), and let \(C_1\) be a congruence subgroup for \(\mathfrak m_1\). Write \(I^{\mathfrak m_1}\) for the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m_1\) and \(P_{\mathfrak m_2}\) for the ray group of \(\mathfrak m_2\), and view all of these as subgroups of the group of nonzero fractional ideals of \(K\). If \(I^{\mathfrak m_1} \cap P_{\mathfrak m_2} \subseteq C_1\), then the pair \((\mathfrak m_1, C_1)\) is equivalent to the pair \((\mathfrak m_2, C_2)\), where \(C_2\) is the change of modulus of \(C_1\) to \(\mathfrak m_2\).

theorem changeModulus_isEquivalent {m1 m2 : Modulus K}
    (C1 : CongruenceSubgroup m1) (hdiv : m2 ∣ m1)
    (hcond : coprimeFractionalIdeals m1 ⊓ rayGroupAmbient m2 ≤
      C1.toAmbientSubgroup) :
    CongruenceSubgroupPair.IsEquivalent
      { modulus := m1, subgroup := C1 }
      { modulus := m2, subgroup := changeModulus C1 m2 }

Uses 9 · Used by 1

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Congruence subgroup pair · Equivalence of congruence subgroup pairs · Change of modulus of a congruence subgroup · Fractional ideals coprime to a modulus · Ray group among all fractional ideals

Proof usesAmbient subgroup of a change of modulus to a divisor · Coprimality passes to divisors of a modulus

Used byCriterion for an equivalent congruence subgroup at a divisor of the modulus

TheoremCriterion for an equivalent congruence subgroup at a divisor of the modulus#✓fully proved

Let \(\mathfrak m_1\) and \(\mathfrak m_2\) be moduli of a number field \(K\) with \(\mathfrak m_2 \mid \mathfrak m_1\), and let \(C_1\) be a congruence subgroup for \(\mathfrak m_1\). Write \(I^{\mathfrak m_1}\) for the group of nonzero fractional ideals of \(K\) coprime to the finite part of \(\mathfrak m_1\) and \(P_{\mathfrak m_2}\) for the ray group of \(\mathfrak m_2\), and view all of these as subgroups of the group of nonzero fractional ideals of \(K\). Then there is a congruence subgroup \(C_2\) for \(\mathfrak m_2\) such that the pair \((\mathfrak m_1, C_1)\) is equivalent to the pair \((\mathfrak m_2, C_2)\) if and only if \(I^{\mathfrak m_1} \cap P_{\mathfrak m_2} \subseteq C_1\).

theorem exists_equivalent_iff_changeModulus {m1 : Modulus K}
    (C1 : CongruenceSubgroup m1) {m2 : Modulus K} (hdiv : m2 ∣ m1) :
    (∃ C2 : CongruenceSubgroup m2,
      CongruenceSubgroupPair.IsEquivalent
        { modulus := m1, subgroup := C1 }
        { modulus := m2, subgroup := C2 }) ↔
      coprimeFractionalIdeals m1 ⊓ rayGroupAmbient m2 ≤
        C1.toAmbientSubgroup

Sources

• ATLAS NumberTheoryI item N422, Lemma 22.5.

Uses 11

Statement usesCongruence subgroup · Congruence subgroup as a subgroup of all invertible fractional ideals · Congruence subgroup pair · Equivalence of congruence subgroup pairs · Fractional ideals coprime to a modulus · Ray group among all fractional ideals

Proof usesA congruence subgroup contains the ray group · Criterion for equivalence of congruence subgroup pairs · Change of modulus of a congruence subgroup · The change of modulus is equivalent to the original pair · Coprimality passes to divisors of a modulus

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.