Documentation

GQ2.UnitFiltrationCounts

B13-3 β€” the residue field of the unit ball #

This file proves the B13-3 component of dyadicUnitFiltration. For a finite extension k/β„šβ‚‚ it builds the residue field O/π”ͺ of the valuation ring O = {β€–xβ€– ≀ 1} and records its cardinality:

The graded isomorphisms and the two Nat.card counts against these (B13-4), and the capstone (B13-5), append to this file. Imports GQ2.UnitFiltrationTop (B13-1) + Mathlib.

source
theorem GQ2.UnitFiltrationCounts.norm_two_lt_one :
β€–2β€– < 1

β€–(2 : β„šΜ„β‚‚)β€– < 1 β€” the dyadic uniformizer of the base has norm 2⁻¹.

The unit ball O as a subring, and its maximal ideal π”ͺ #

source
noncomputable def GQ2.UnitFiltrationCounts.Osub (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
Subring β†₯k

The valuation ring O = {x ∈ k : β€–xβ€– ≀ 1}, as a subring (multiplicative structure the counts need β€” B13-1's unitBall carries only the additive one).

Equations
  • GQ2.UnitFiltrationCounts.Osub k = { carrier := {x : β†₯k | β€–xβ€– ≀ 1}, mul_mem' := β‹―, one_mem' := β‹―, add_mem' := β‹―, zero_mem' := β‹―, neg_mem' := β‹― }
Instances For
    source
    noncomputable def GQ2.UnitFiltrationCounts.maxIdeal (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
    Ideal β†₯(Osub k)

    The maximal ideal π”ͺ = {x ∈ O : β€–xβ€– < 1} (the non-units of O). Intrinsic β€” no uniformizer is used, so this file does not depend on the B13-2 lane.

    Equations
    Instances For
      source
      instance GQ2.UnitFiltrationCounts.instIsPrimeSubtypeAlgebraicClosurePadicOfNatNatMemIntermediateFieldSubringOsubMaxIdeal (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
      (maxIdeal k).IsPrime

      π”ͺ is prime: β€–xyβ€– = β€–xβ€–β€–yβ€– < 1 forces a factor < 1; 1 βˆ‰ π”ͺ.

      source
      instance GQ2.UnitFiltrationCounts.instCompactSpaceSubtypeAlgebraicClosurePadicOfNatNatMemIntermediateFieldSubringOsub (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] :
      CompactSpace β†₯(Osub k)

      O is compact: the closed unit ball of the proper space β†₯k.

      source
      instance GQ2.UnitFiltrationCounts.instFiniteQuotientSubtypeAlgebraicClosurePadicOfNatNatMemIntermediateFieldSubringOsubIdealMaxIdeal (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] :
      Finite (β†₯(Osub k) β§Έ maxIdeal k)

      O/π”ͺ is finite: π”ͺ is an open subgroup of the compact O.

      source
      @[reducible, inline]
      abbrev GQ2.UnitFiltrationCounts.ResidueField (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
      Type

      The residue field O/π”ͺ.

      Equations
      Instances For
        source
        @[implicit_reducible]
        noncomputable instance GQ2.UnitFiltrationCounts.instFieldResidueField (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] :
        Field (ResidueField k)

        O/π”ͺ is a field: a finite integral domain.

        Equations
        source
        theorem GQ2.UnitFiltrationCounts.two_eq_zero (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
        2 = 0

        2 = 0 in the residue field (β€–2β€– < 1, so 2 ∈ π”ͺ).

        source
        instance GQ2.UnitFiltrationCounts.instCharPResidueFieldOfNatNat (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] :
        CharP (ResidueField k) 2

        The residue field has characteristic 2.

        source
        theorem GQ2.UnitFiltrationCounts.residue_card (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] :
        βˆƒ (f : β„•), 1 ≀ f ∧ Nat.card (ResidueField k) = 2 ^ f ∧ Nat.card (ResidueField k)Λ£ = 2 ^ f - 1

        The residue-field cardinalities: #(O/π”ͺ) = 2^f and #(O/π”ͺ)Λ£ = 2^f βˆ’ 1 with f β‰₯ 1. The f here is the residue degree; B13-4 feeds these into the graded counts.

        B13-4 β€” the graded isomorphisms and the two Nat.card counts #

        Two group homomorphisms cutting the unit filtration into residue-field data: U⁰ = normUnits β†’ (O/π”ͺ)Λ£ (u ↦ Ε«) with kernel UΒΉ and surjective, and for i β‰₯ 1 U^{(i)} β†’ Multiplicative (O/π”ͺ) (u ↦ (uβˆ’1)/πⁱ mod π”ͺ) with kernel U^{(i+1)} and surjective. The isomorphism theorem then gives #(U⁰/UΒΉ) = #(O/π”ͺ)Λ£ = 2^f βˆ’ 1 and #(U^i/U^{i+1}) = #(O/π”ͺ) = 2^f. Everything is parameterized by a uniformizer Ο€ : β†₯k (B13-2's exists_uniformizer).

        source
        theorem GQ2.UnitFiltrationCounts.norm_sub_one_bridge (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) (x : β†₯k) :
        ‖↑x - 1β€– = β€–x - 1β€–

        ‖↑x βˆ’ 1β€– = β€–x βˆ’ 1β€– bridging the β„šΜ„β‚‚-norm of the coercion and the β†₯k-norm.

        source
        theorem GQ2.UnitFiltrationCounts.scaled_exchange (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (hΟ€lt : β€–Ο€β€– < 1) (hΟ€max : βˆ€ (y : β†₯k), β€–yβ€– < 1 β†’ β€–yβ€– ≀ β€–Ο€β€–) (x : β†₯k) (i : β„•) :
        β€–xβ€– < β€–Ο€β€– ^ i ↔ β€–xβ€– ≀ β€–Ο€β€– ^ (i + 1)

        The scaled exchange: β€–xβ€– < ‖π‖ⁱ ↔ β€–xβ€– ≀ β€–Ο€β€–^{i+1} (divide by πⁱ and apply hΟ€_max).

        Grade 0: U⁰/UΒΉ ≃ (O/π”ͺ)Λ£ #

        source
        noncomputable def GQ2.UnitFiltrationCounts.normUnitToOsub (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) (u : β†₯(normUnits k)) :
        β†₯(Osub k)

        A norm-one unit of k as an element of the valuation ring O.

        Equations
        Instances For
          source
          theorem GQ2.UnitFiltrationCounts.normUnitToOsub_one (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
          normUnitToOsub k 1 = 1
          source
          theorem GQ2.UnitFiltrationCounts.normUnitToOsub_mul (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) (a b : β†₯(normUnits k)) :
          normUnitToOsub k (a * b) = normUnitToOsub k a * normUnitToOsub k b
          source
          noncomputable def GQ2.UnitFiltrationCounts.normUnitToOsubUnit (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
          β†₯(normUnits k) β†’* (β†₯(Osub k))Λ£

          A norm-one unit of k as a unit of the valuation ring O.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def GQ2.UnitFiltrationCounts.gradeZeroHom (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) :
            β†₯(normUnits k) β†’* (ResidueField k)Λ£

            The grade-0 map U⁰ β†’ (O/π”ͺ)Λ£: a norm-one unit ↦ its residue.

            Equations
            Instances For
              source
              theorem GQ2.UnitFiltrationCounts.gradeZeroHom_eq_one_iff (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) (u : β†₯(normUnits k)) :
              (gradeZeroHom k) u = 1 ↔ ‖↑↑u - 1β€– < 1

              Grade i β‰₯ 1: U^{(i)}/U^{(i+1)} ≃ (O/π”ͺ, +) #

              source
              noncomputable def GQ2.UnitFiltrationCounts.depthDiv (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (i : β„•) (u : β†₯(depthUnits k (↑π) i)) :
              β†₯k

              (u βˆ’ 1)/πⁱ, the value whose residue is the grade-i datum.

              Equations
              Instances For
                source
                theorem GQ2.UnitFiltrationCounts.depthDiv_mem (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (i : β„•) (u : β†₯(depthUnits k (↑π) i)) :
                depthDiv k i u ∈ Osub k
                source
                noncomputable def GQ2.UnitFiltrationCounts.depthToOsub (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (i : β„•) (u : β†₯(depthUnits k (↑π) i)) :
                β†₯(Osub k)

                (u βˆ’ 1)/πⁱ as an element of O.

                Equations
                Instances For
                  source
                  theorem GQ2.UnitFiltrationCounts.depthRes_eq_zero_iff (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (i : β„•) (u : β†₯(depthUnits k (↑π) i)) :
                  (Ideal.Quotient.mk (maxIdeal k)) (depthToOsub k hΟ€ne i u) = 0 ↔ ‖↑↑u - 1β€– < β€–Ο€β€– ^ i
                  source
                  theorem GQ2.UnitFiltrationCounts.depthRes_add (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (hΟ€lt : β€–Ο€β€– < 1) {i : β„•} (hi : 1 ≀ i) (u v : β†₯(depthUnits k (↑π) i)) :
                  (Ideal.Quotient.mk (maxIdeal k)) (depthToOsub k hΟ€ne i (u * v)) = (Ideal.Quotient.mk (maxIdeal k)) (depthToOsub k hΟ€ne i u) + (Ideal.Quotient.mk (maxIdeal k)) (depthToOsub k hΟ€ne i v)

                  The grade-i additivity (the cross-term (uβˆ’1)(vβˆ’1)/πⁱ has residue 0).

                  source
                  theorem GQ2.UnitFiltrationCounts.gradeI_surj_witness (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (hΟ€lt : β€–Ο€β€– < 1) {i : β„•} (hi : 1 ≀ i) (a : β†₯(Osub k)) :
                  βˆƒ (u : β†₯(depthUnits k (↑π) i)), depthToOsub k hΟ€ne i u = a

                  Surjectivity witness: 1 + a·πⁱ is a norm-one unit in U^{(i)} with datum a.

                  source
                  noncomputable def GQ2.UnitFiltrationCounts.gradeIHom (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (hΟ€lt : β€–Ο€β€– < 1) {i : β„•} (hi : 1 ≀ i) :
                  β†₯(depthUnits k (↑π) i) β†’* Multiplicative (ResidueField k)

                  The grade-i map U^{(i)} β†’ Multiplicative (O/π”ͺ).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem GQ2.UnitFiltrationCounts.exists_gradeCounts (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] {Ο€ : β†₯k} (hΟ€ne : Ο€ β‰  0) (hΟ€lt : β€–Ο€β€– < 1) (hΟ€max : βˆ€ (y : β†₯k), β€–yβ€– < 1 β†’ β€–yβ€– ≀ β€–Ο€β€–) :
                    βˆƒ (f : β„•), 1 ≀ f ∧ Nat.card (β†₯(normUnits k) β§Έ (depthUnits k (↑π) 1).subgroupOf (normUnits k)) = 2 ^ f - 1 ∧ βˆ€ (i : β„•), 1 ≀ i β†’ Nat.card (β†₯(depthUnits k (↑π) i) β§Έ (depthUnits k (↑π) (i + 1)).subgroupOf (depthUnits k (↑π) i)) = 2 ^ f

                    B13-4 result: the graded counts #(U⁰/UΒΉ) = 2^f βˆ’ 1 and #(U^i/U^{i+1}) = 2^f (same f), at a uniformizer Ο€. Fed into the DyadicUnitFiltration structure by B13-5.

                    source
                    noncomputable def GQ2.dyadicUnitFiltration' (k : IntermediateField β„š_[2] (AlgebraicClosure β„š_[2])) [FiniteDimensional β„š_[2] β†₯k] :
                    DyadicUnitFiltration k

                    The B13 capstone (the deep-part proof discharge, B13-5): every finite extension k/β„šβ‚‚ inside β„šΜ„β‚‚ carries a DyadicUnitFiltration. Assembled from the uniformizer + ramification data (exists_uniformizer, exists_ramificationIndex β€” GQ2/UnitFiltrationTop.lean, B13-1/2) and the residue-graded counts (UnitFiltrationCounts.exists_gradeCounts β€” B13-3/4). A single uniformizer Ο€ : β†₯k feeds every field, so the he normalization β€–2β€– = β€–Ο€β€–^e and the graded counts share the same Ο€ (the β†₯k β†’ β„šΜ„β‚‚ coercion is norm-preserving by rfl, so the β†₯k-form hypotheses discharge the β„šΜ„β‚‚-form structure fields defeq). noncomputable β€” the witnesses are pulled from the existence lemmas by Classical.choice. Discharges the axiom GQ2.dyadicUnitFiltration (GQ2/Foundations/Axioms.lean).

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For