Documentation

TauCeti.NumberTheory.NumberField.NarrowClassGroup.ElementaryTwoQuotient

The elementary-2 quotient of the narrow class group #

For a number field K, genus theory computes the maximal elementary-2 quotient

Cl⁺(K) / Cl⁺(K)²

of the narrow class group. This quotient, rather than the ordinary class-group quotient, is the object whose dimension is t - 1 for a real quadratic field with t ramified rational primes. For a totally complex field the positivity condition is vacuous, so the narrow and ordinary elementary-2 quotients are linearly equivalent and their 2-ranks agree.

The underlying construction is the general TauCeti.ElementaryTwoQuotient. This file specializes it to the finite group NarrowClassGroup K, records its induced map to TauCeti.ClassGroup.ElementaryTwoQuotient (𝓞 K), and exposes the rank statements used by the genus-field milestone of TauCetiRoadmap/Multiquadratic/README.md.

Main definitions and results #

References #

source
@[reducible, inline]
abbrev NumberField.NarrowClassGroup.ElementaryTwoQuotient (K : Type u_1) [Field K] [NumberField K] :
Type u_1

The maximal elementary-2 quotient of the narrow class group, Cl⁺(K) / Cl⁺(K)². This is a finite-dimensional vector space over ZMod 2.

Equations
Instances For
    source
    noncomputable def NumberField.NarrowClassGroup.toClassGroupElementaryTwoQuotient (K : Type u_1) [Field K] [NumberField K] :
    ElementaryTwoQuotient K →ₗ[ZMod 2] TauCeti.ClassGroup.ElementaryTwoQuotient (RingOfIntegers K)

    Forgetting positivity induces a ZMod 2-linear map Cl⁺(K) / Cl⁺(K)² → Cl(K) / Cl(K)².

    Equations
    Instances For
      source
      @[simp]
      theorem NumberField.NarrowClassGroup.toClassGroupElementaryTwoQuotient_mk (K : Type u_1) [Field K] [NumberField K] (C : NarrowClassGroup K) :
      (toClassGroupElementaryTwoQuotient K) (TauCeti.elementaryTwoQuotientMk C) = TauCeti.elementaryTwoQuotientMk (toClassGroup C)

      The map on elementary-2 quotients induced by forgetting positivity sends the class of C to the square class of its image in the ordinary class group.

      source
      theorem NumberField.NarrowClassGroup.toClassGroupElementaryTwoQuotient_surjective (K : Type u_1) [Field K] [NumberField K] :
      Function.Surjective ⇑(toClassGroupElementaryTwoQuotient K)

      The induced map Cl⁺(K) / Cl⁺(K)² → Cl(K) / Cl(K)² is surjective.

      source
      noncomputable def NumberField.NarrowClassGroup.twoRank (K : Type u_1) [Field K] [NumberField K] :
      ℕ

      The narrow class-group 2-rank: the dimension over ZMod 2 of Cl⁺(K) / Cl⁺(K)².

      Equations
      Instances For
        source
        @[simp]
        theorem NumberField.NarrowClassGroup.twoRank_def (K : Type u_1) [Field K] [NumberField K] :
        twoRank K = Module.finrank (ZMod 2) (ElementaryTwoQuotient K)

        The narrow class-group 2-rank is the dimension of its maximal elementary-2 quotient.

        source
        theorem NumberField.NarrowClassGroup.card_elementaryTwoQuotient_eq_two_pow_twoRank (K : Type u_1) [Field K] [NumberField K] :
        Nat.card (ElementaryTwoQuotient K) = 2 ^ twoRank K

        The maximal elementary-2 quotient of the narrow class group has 2 ^ twoRank K elements.

        source
        theorem NumberField.NarrowClassGroup.card_eq_two_pow_twoRank_of_classNumber_eq_one (K : Type u_1) [Field K] [NumberField K] (hclass : classNumber K = 1) :
        Nat.card (NarrowClassGroup K) = 2 ^ twoRank K

        A class-number-one field has narrow class number 2 to the narrow 2-rank. When the ordinary class group is trivial, every narrow class lies in the kernel of Cl⁺(K) → Cl(K) and hence has square one. Thus Cl⁺(K) is its own maximal elementary-2 quotient.

        source
        theorem NumberField.NarrowClassGroup.classGroupTwoRank_le_twoRank (K : Type u_1) [Field K] [NumberField K] :
        TauCeti.ClassGroup.twoRank (RingOfIntegers K) ≤ twoRank K

        The ordinary class-group 2-rank is at most the narrow class-group 2-rank. The inequality can be strict for real fields because forgetting positivity is only a surjection.

        source
        noncomputable def NumberField.NarrowClassGroup.toClassGroupElementaryTwoQuotientEquiv (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] :
        ElementaryTwoQuotient K ≃ₗ[ZMod 2] TauCeti.ClassGroup.ElementaryTwoQuotient (RingOfIntegers K)

        For a totally complex field, the elementary-2 quotients of the narrow and ordinary class groups are linearly equivalent over ZMod 2.

        Equations
        Instances For
          source
          @[simp]
          theorem NumberField.NarrowClassGroup.toClassGroupElementaryTwoQuotientEquiv_apply (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (x : ElementaryTwoQuotient K) :
          (toClassGroupElementaryTwoQuotientEquiv K) x = (toClassGroupElementaryTwoQuotient K) x

          For a totally complex field, the elementary-2 quotient equivalence is the linear map induced by forgetting positivity.

          source
          theorem NumberField.NarrowClassGroup.twoRank_eq_classGroupTwoRank_of_injective (K : Type u_1) [Field K] [NumberField K] (h : Function.Injective ⇑toClassGroup) :
          twoRank K = TauCeti.ClassGroup.twoRank (RingOfIntegers K)

          An injective forgetful map makes the narrow and ordinary class-group 2-ranks agree. Since forgetting positivity is always surjective, injectivity makes it an isomorphism Cl⁺(K) ≃ Cl(K), and isomorphic groups have the same 2-rank.

          source
          theorem NumberField.NarrowClassGroup.twoRank_eq_classGroupTwoRank (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] :
          twoRank K = TauCeti.ClassGroup.twoRank (RingOfIntegers K)

          For a totally complex field, the narrow and ordinary class-group 2-ranks agree. The totally complex case of twoRank_eq_classGroupTwoRank_of_injective, where positivity is vacuous.