Transporting localized units and Hilbert symbols along an isomorphism of fields

A ring isomorphism e : K ≃+* L of number fields identifies the finite places of K with those of L by HeightOneSpectrum.equivOfRingEquiv (RingOfIntegers.mapRingEquiv e) and the real places of K with those of L by NumberField.InfinitePlace.realEquivOfRingEquiv e. At each pair of corresponding finite places v and w, adicCompletionCongr extends e to a ring isomorphism K_v ≃+* L_w that intertwines unitAtFinitePlace, preserves local squares, and preserves the norm-equation Hilbert symbol. At each real place w, realEquivOfRingEquiv e intertwines unitAtRealPlace on the nose in ℝˣ.

Reindexing along the two place bijections shows that the product of the finite-place Hilbert symbols (a_v, b_v)_v and the product of the real-place Hilbert symbols (a_w, b_w)_w are both invariant under e. In particular, global statements expressed through local squareness and localized Hilbert symbols transfer along Shrink.ringEquiv K : Shrink.{0} K ≃+* K from Type to number fields in any universe.

Main results

• TauCeti.units_map_adicCompletionCongr_unitAtFinitePlace: adicCompletionCongr intertwines unitAtFinitePlace with Units.map e.
• TauCeti.isSquare_unitAtFinitePlace_iff_of_ringEquiv, TauCeti.isSquare_unitAtFinitePlace_equivOfRingEquiv: local squareness at a finite place is preserved along e.
• TauCeti.hilbertSymbol_unitAtFinitePlace_of_ringEquiv, TauCeti.hilbertSymbol_unitAtFinitePlace_equivOfRingEquiv: the localized Hilbert symbol at a finite place is preserved along e.
• TauCeti.finprod_hilbertSymbol_unitAtFinitePlace_ringEquiv: the product of the finite-place Hilbert symbols is preserved along e.
• TauCeti.unitAtRealPlace_realEquivOfRingEquiv, TauCeti.unitAtRealPlace_realEquivOfRingEquiv_units_map: unitAtRealPlace at a transported real place pulls back along e.symm, and is unchanged when both place and unit are transported along e.
• TauCeti.prod_hilbertSymbol_unitAtRealPlace_ringEquiv: the product of the real-place Hilbert symbols is preserved along e.

@[simp]

theorem TauCeti.units_map_adicCompletionCongr_unitAtFinitePlace {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)} {e : K ≃+* L} (he : ∀ (x : K), (IsDedekindDomain.HeightOneSpectrum.valuation L w) (e x) = (IsDedekindDomain.HeightOneSpectrum.valuation K v) x) (a : Kˣ) : (Units.map ↑(v.adicCompletionCongr w e he)) (v.unitAtFinitePlace a) = w.unitAtFinitePlace ((Units.map ↑e) a)

Extending a valuation-preserving isomorphism e : K ≃+* L to the adic completions intertwines unitAtFinitePlace with Units.map e.

theorem TauCeti.isSquare_unitAtFinitePlace_iff_of_ringEquiv {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] (e : K ≃+* L) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)} (hvw : w.asIdeal = Ideal.map (NumberField.RingOfIntegers.mapRingEquiv e) v.asIdeal) (a : Kˣ) : IsSquare (w.unitAtFinitePlace ((Units.map ↑e) a)) ↔ IsSquare (v.unitAtFinitePlace a)

Local squareness at a finite place is preserved under a ring isomorphism e : K ≃+* L of number fields carrying v to w.

@[simp]

theorem TauCeti.isSquare_unitAtFinitePlace_equivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] (e : K ≃+* L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : Kˣ) : IsSquare (((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (NumberField.RingOfIntegers.mapRingEquiv e)) v).unitAtFinitePlace ((Units.map ↑e) a)) ↔ IsSquare (v.unitAtFinitePlace a)

Local squareness at a finite place is preserved when both the place and the unit are transported along e : K ≃+* L.

theorem TauCeti.hilbertSymbol_unitAtFinitePlace_of_ringEquiv {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] (e : K ≃+* L) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)} (hvw : w.asIdeal = Ideal.map (NumberField.RingOfIntegers.mapRingEquiv e) v.asIdeal) (a b : Kˣ) : hilbertSymbol (w.unitAtFinitePlace ((Units.map ↑e) a)) (w.unitAtFinitePlace ((Units.map ↑e) b)) = hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)

The localized Hilbert symbol at a finite place is preserved under a ring isomorphism e : K ≃+* L of number fields carrying v to w.

@[simp]

theorem TauCeti.hilbertSymbol_unitAtFinitePlace_equivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] (e : K ≃+* L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (a b : Kˣ) : hilbertSymbol (((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (NumberField.RingOfIntegers.mapRingEquiv e)) v).unitAtFinitePlace ((Units.map ↑e) a)) (((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (NumberField.RingOfIntegers.mapRingEquiv e)) v).unitAtFinitePlace ((Units.map ↑e) b)) = hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)

The localized Hilbert symbol at a finite place is preserved when both the place and the units are transported along e : K ≃+* L.

theorem TauCeti.finprod_hilbertSymbol_unitAtFinitePlace_ringEquiv {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] (e : K ≃+* L) (a b : Kˣ) : ∏ᶠ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), hilbertSymbol (w.unitAtFinitePlace ((Units.map ↑e) a)) (w.unitAtFinitePlace ((Units.map ↑e) b)) = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)

The product of the localized Hilbert symbols over all finite places is preserved under a ring isomorphism e : K ≃+* L of number fields.

@[simp]

theorem TauCeti.unitAtRealPlace_realEquivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : { w : NumberField.InfinitePlace K // w.IsReal }) (b : Lˣ) : (unitAtRealPlace ((NumberField.InfinitePlace.realEquivOfRingEquiv e) w)) b = (unitAtRealPlace w) ((Units.map ↑e.symm) b)

Evaluating unitAtRealPlace at a real place transported along e : K ≃+* L pulls the unit back along e.symm.

theorem TauCeti.unitAtRealPlace_realEquivOfRingEquiv_units_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : Kˣ) : (unitAtRealPlace ((NumberField.InfinitePlace.realEquivOfRingEquiv e) w)) ((Units.map ↑e) a) = (unitAtRealPlace w) a

Transporting both a real place and a global unit along e : K ≃+* L leaves unitAtRealPlace unchanged.

theorem TauCeti.prod_hilbertSymbol_unitAtRealPlace_ringEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Fintype { w : NumberField.InfinitePlace K // w.IsReal }] [Fintype { w : NumberField.InfinitePlace L // w.IsReal }] (e : K ≃+* L) (a b : Kˣ) : ∏ w : { w : NumberField.InfinitePlace L // w.IsReal }, hilbertSymbol ((unitAtRealPlace w) ((Units.map ↑e) a)) ((unitAtRealPlace w) ((Units.map ↑e) b)) = ∏ w : { w : NumberField.InfinitePlace K // w.IsReal }, hilbertSymbol ((unitAtRealPlace w) a) ((unitAtRealPlace w) b)

The product of the localized Hilbert symbols over all real places is preserved under a ring isomorphism e : K ≃+* L.