Documentation

TauCeti.NumberTheory.LocalField.UnitFiltration.Graded

Positive graded pieces of the unit filtration #

For a nonarchimedean local field K, multiplication becomes addition on each positive successive quotient of the unit filtration. More precisely, subtracting one gives a canonical isomorphism

U(K,n) / U(K,n+1) ≃ 𝓂[K]^n / 𝓂[K]^(n+1)

for n > 0. Since the maximal ideal of the discrete valuation ring π’ͺ[K] is principal, each ideal quotient is a one-dimensional copy of the residue field. Combining these facts identifies every positive graded piece with the additive group of 𝓀[K], and shows that it has #𝓀[K] elements.

Main results #

The final identification reuses Mathlib's Ideal.quotEquivPowQuotPowSucc, the linear equivalence between a quotient by a nonzero principal ideal and each successive quotient of its powers.

References #

source
@[reducible, inline]
abbrev TauCeti.MaximalIdealGraded (K : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
Type u_2

The nth graded piece of the maximal-ideal filtration of π’ͺ[K], presented as 𝓂[K]^n / 𝓂[K]^(n+1). The denominator is written as 𝓂[K] β€’ ⊀ on the subtype 𝓂[K]^n; Submodule.mem_smul_top_iff identifies it with 𝓂[K]^(n+1).

Equations
Instances For
    source
    noncomputable def TauCeti.unitFiltrationDifference {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (x : β†₯(unitFiltration K (n + 1))) :
    β†₯(IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer ^ (n + 1))

    The difference u - 1 attached to u ∈ U(K,n+1), as an element of 𝓂[K]^(n+1).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.coe_coe_unitFiltrationDifference {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (x : β†₯(unitFiltration K (n + 1))) :
      ↑↑(unitFiltrationDifference n x) = ↑↑x - 1

      In the ambient field, unitFiltrationDifference n u is u - 1.

      source
      noncomputable def TauCeti.unitFiltrationToMaximalIdealGraded {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
      β†₯(unitFiltration K (n + 1)) β†’* Multiplicative (MaximalIdealGraded K (n + 1))

      Subtracting one, modulo the next power of the maximal ideal, is a homomorphism from a positive unit-filtration step to the multiplicative copy of the corresponding ideal quotient.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.unitFiltrationToMaximalIdealGraded_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (x : β†₯(unitFiltration K (n + 1))) :
        (unitFiltrationToMaximalIdealGraded n) x = Multiplicative.ofAdd (Submodule.Quotient.mk (unitFiltrationDifference n x))

        The value of unitFiltrationToMaximalIdealGraded is the class of u - 1.

        source
        theorem TauCeti.ker_unitFiltrationToMaximalIdealGraded {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
        (unitFiltrationToMaximalIdealGraded n).ker = (unitFiltration K (n + 2)).subgroupOf (unitFiltration K (n + 1))

        The kernel of subtracting one modulo 𝓂[K]^(n+2) is precisely U(K,n+2).

        source
        theorem TauCeti.unitFiltrationToMaximalIdealGraded_surjective {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
        Function.Surjective ⇑(unitFiltrationToMaximalIdealGraded n)

        Subtracting one modulo 𝓂[K]^(n+2) maps U(K,n+1) onto the corresponding maximal-ideal graded piece.

        source
        noncomputable def TauCeti.unitFiltrationGradedSuccEquivMaximalIdealGraded {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
        UnitFiltrationGraded K (n + 1) ≃* Multiplicative (MaximalIdealGraded K (n + 1))

        Subtracting one identifies the positive unit-filtration quotient U(K,n+1) / U(K,n+2) with 𝓂[K]^(n+1) / 𝓂[K]^(n+2).

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.unitFiltrationGradedSuccEquivMaximalIdealGraded_mk {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (x : β†₯(unitFiltration K (n + 1))) :
          (unitFiltrationGradedSuccEquivMaximalIdealGraded n) ↑x = Multiplicative.ofAdd (Submodule.Quotient.mk (unitFiltrationDifference n x))

          On a class represented by u ∈ U(K,n+1), the positive-depth graded equivalence is the class of u - 1 modulo 𝓂[K]^(n+2).

          source
          noncomputable def TauCeti.unitFiltrationGradedSuccEquivResidueField {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
          Additive (UnitFiltrationGraded K (n + 1)) ≃+ IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer

          Every positive graded piece U(K,n+1) / U(K,n+2), read additively, is isomorphic to the additive group of the residue field.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.unitFiltrationGradedSuccEquivResidueField_ofMul_mk {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (x : β†₯(unitFiltration K (n + 1))) :
            (unitFiltrationGradedSuccEquivResidueField n) (Additive.ofMul ↑x) = (Ideal.quotEquivPowQuotPowSucc β‹― β‹― (n + 1)).symm (Submodule.Quotient.mk (unitFiltrationDifference n x))

            On a class represented by u ∈ U(K,n+1), the positive-depth residue-field equivalence is the residue class attached to u - 1 by Mathlib's principal-power-quotient equivalence.

            source
            instance TauCeti.finite_unitFiltrationGraded_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
            Finite (UnitFiltrationGraded K (n + 1))

            The positive graded piece U(K,n+1) / U(K,n+2) is finite.

            source
            theorem TauCeti.natCard_unitFiltrationGraded_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
            Nat.card (UnitFiltrationGraded K (n + 1)) = Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)

            Every positive graded piece has the cardinality of the residue field.

            source
            theorem TauCeti.relIndex_unitFiltration_succ_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
            (unitFiltration K (n + 2)).relIndex (unitFiltration K (n + 1)) = Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)

            Every positive step has relative index equal to the cardinality of the residue field: [U(K,n+1) : U(K,n+2)] = #𝓀[K].

            source
            theorem TauCeti.relIndex_unitFiltration_add_succ_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (m n : β„•) :
            (unitFiltration K (m + n + 1)).relIndex (unitFiltration K (m + 1)) = Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer) ^ n

            The index of U(K,m+n+1) in U(K,m+1) is q ^ n, where q = #𝓀[K].

            source
            instance TauCeti.unitFiltration_isFiniteRelIndex_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (m n : β„•) :
            (unitFiltration K m).IsFiniteRelIndex (unitFiltration K (n + 1))

            Every U(K,m) has finite relative index in each positive-depth subgroup U(K,n+1): the index is 1 when m ≀ n + 1, and a power of #𝓀[K] otherwise.

            source
            instance TauCeti.unitFiltration_isFiniteRelIndex_zero {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (m : β„•) :
            (unitFiltration K m).IsFiniteRelIndex (unitFiltration K 0)

            Every U(K,m) has finite index in the unit group U(K,0) = π’ͺ[K]Λ£.

            source
            theorem TauCeti.natCard_unitFiltration_succ_quotient_add_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (m n : β„•) :
            Nat.card (β†₯(unitFiltration K (m + 1)) β§Έ (unitFiltration K (m + n + 1)).subgroupOf (unitFiltration K (m + 1))) = Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer) ^ n

            The positive-depth finite-level quotient U(K,m+1) / U(K,m+n+1) has q ^ n elements, where q = #𝓀[K].