The quadratic norm quotient is detected on units

Let a have odd quadratic defect exponent. There is then a norm from K(√a) of every normalized valuation. Consequently, every class in the quotient of Kˣ by the quadratic norm subgroup has a representative in the depth-zero unit filtration U(K, 0).

This identifies the full norm quotient with the quotient of U(K, 0) by the unit norms. In particular, their indices agree. This is the reduction from the valuation part to the unit part in the ramified cases of the quadratic norm-index theorem, especially for a unit radicand of odd defect.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A.

noncomputable def TauCeti.unitNormQuotientMap {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : ↥(unitFiltration K 0) →* Kˣ ⧸ quadraticNormSubgroup ↑a

The map from depth-zero units to the quotient by the quadratic norm subgroup.

@[simp]

theorem TauCeti.unitNormQuotientMap_apply {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) (u : ↥(unitFiltration K 0)) : (unitNormQuotientMap a) u = ↑↑u

theorem TauCeti.ker_unitNormQuotientMap {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : (unitNormQuotientMap a).ker = (quadraticNormSubgroup ↑a).subgroupOf (unitFiltration K 0)

The kernel of the unit-to-norm-quotient map consists exactly of the unit norms.

theorem TauCeti.unitNormQuotientMap_surjective_of_odd_defectExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {d : ℤ} (hd : defectExponent a = ↑d) (hodd : Odd d) : Function.Surjective ⇑(unitNormQuotientMap a)

If the quadratic defect exponent of a is odd, every norm coset has a representative in U(K, 0).

noncomputable def TauCeti.unitNormQuotientEquivOfOddDefectExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {d : ℤ} (hd : defectExponent a = ↑d) (hodd : Odd d) : ↥(unitFiltration K 0) ⧸ (quadraticNormSubgroup ↑a).subgroupOf (unitFiltration K 0) ≃* Kˣ ⧸ quadraticNormSubgroup ↑a

For odd quadratic defect, quotienting the unit group by its unit norms gives the full quadratic norm quotient.

@[simp]

theorem TauCeti.unitNormQuotientEquivOfOddDefectExponent_mk {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {d : ℤ} (hd : defectExponent a = ↑d) (hodd : Odd d) (u : ↥(unitFiltration K 0)) : (unitNormQuotientEquivOfOddDefectExponent hd hodd) ↑u = ↑↑u

The quotient equivalence sends the class of a depth-zero unit to the class of the same element in the full quadratic norm quotient.

theorem TauCeti.index_subgroupOf_unitFiltration_eq_quadraticNormSubgroup_index_of_odd_defectExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {d : ℤ} (hd : defectExponent a = ↑d) (hodd : Odd d) : ((quadraticNormSubgroup ↑a).subgroupOf (unitFiltration K 0)).index = (quadraticNormSubgroup ↑a).index

For odd quadratic defect, the index of the quadratic norm subgroup is already the index of the unit norms inside U(K, 0).