Transporting infinite and real places along an isomorphism of fields

A ring isomorphism e : K ≃+* L of fields pushes infinite places forward by pulling back along e.symm, giving a bijection NumberField.InfinitePlace.equivOfRingEquiv e between InfinitePlace K and InfinitePlace L. Because e is an isomorphism, this bijection preserves real and complex places, multiplicities, and the canonical real embeddings at real places, and restricts to a bijection NumberField.InfinitePlace.realEquivOfRingEquiv e between the subtypes of real places.

Both constructions are functorial in e and require no number-field hypothesis on K or L. In particular, they identify the infinite and real places of a field with those of any isomorphic copy in another universe, such as Shrink K.

Main definitions

• NumberField.InfinitePlace.equivOfRingEquiv: the bijection InfinitePlace K ≃ InfinitePlace L induced by e : K ≃+* L.
• NumberField.InfinitePlace.realEquivOfRingEquiv: the induced bijection {w : InfinitePlace K // w.IsReal} ≃ {w : InfinitePlace L // w.IsReal} on real places.

Main results

• NumberField.InfinitePlace.equivOfRingEquiv_apply, NumberField.InfinitePlace.equivOfRingEquiv_mk: evaluation of the transported place and compatibility with InfinitePlace.mk.
• NumberField.InfinitePlace.equivOfRingEquiv_refl_apply, NumberField.InfinitePlace.equivOfRingEquiv_refl, NumberField.InfinitePlace.equivOfRingEquiv_symm, NumberField.InfinitePlace.equivOfRingEquiv_trans_apply, NumberField.InfinitePlace.equivOfRingEquiv_trans: functoriality on elements and as bundled bijections.
• NumberField.InfinitePlace.isReal_equivOfRingEquiv_iff, NumberField.InfinitePlace.isComplex_equivOfRingEquiv_iff, NumberField.InfinitePlace.mult_equivOfRingEquiv: preservation of realness, complexity, and multiplicity.
• NumberField.InfinitePlace.embedding_of_isReal_equivOfRingEquiv: the real embedding of the transported place is the real embedding of the original place composed with e.symm.
• NumberField.InfinitePlace.realEquivOfRingEquiv_refl_apply, NumberField.InfinitePlace.realEquivOfRingEquiv_refl, NumberField.InfinitePlace.realEquivOfRingEquiv_symm, NumberField.InfinitePlace.realEquivOfRingEquiv_trans_apply, NumberField.InfinitePlace.realEquivOfRingEquiv_trans: functoriality of realEquivOfRingEquiv.

def NumberField.InfinitePlace.equivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) : InfinitePlace K ≃ InfinitePlace L

The bijection between the infinite places of two fields induced by a ring isomorphism e : K ≃+* L, sending w to w.comap e.symm.

theorem NumberField.InfinitePlace.equivOfRingEquiv_eq_comap {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : InfinitePlace K) : (equivOfRingEquiv e) w = w.comap ↑e.symm

equivOfRingEquiv e sends an infinite place w to w.comap e.symm.

@[simp]

theorem NumberField.InfinitePlace.equivOfRingEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : InfinitePlace K) (x : L) : ((equivOfRingEquiv e) w) x = w (e.symm x)

Evaluating equivOfRingEquiv e w at x : L evaluates w at e.symm x.

@[simp]

theorem NumberField.InfinitePlace.equivOfRingEquiv_mk {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (φ : K →+* ℂ) : (equivOfRingEquiv e) (mk φ) = mk (φ.comp ↑e.symm)

Transporting the infinite place of a complex embedding φ : K →+* ℂ along e : K ≃+* L gives the infinite place of φ ∘ e.symm.

@[simp]

theorem NumberField.InfinitePlace.equivOfRingEquiv_refl_apply {K : Type u_1} [Field K] (w : InfinitePlace K) : (equivOfRingEquiv (RingEquiv.refl K)) w = w

The identity ring isomorphism induces the identity on infinite places.

theorem NumberField.InfinitePlace.equivOfRingEquiv_refl {K : Type u_1} [Field K] : equivOfRingEquiv (RingEquiv.refl K) = Equiv.refl (InfinitePlace K)

The identity ring isomorphism induces Equiv.refl on InfinitePlace K.

@[simp]

theorem NumberField.InfinitePlace.equivOfRingEquiv_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) : (equivOfRingEquiv e).symm = equivOfRingEquiv e.symm

Inverting the ring isomorphism inverts the induced bijection of infinite places.

@[simp]

theorem NumberField.InfinitePlace.equivOfRingEquiv_trans_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] (e : K ≃+* L) (e' : L ≃+* M) (w : InfinitePlace K) : (equivOfRingEquiv e') ((equivOfRingEquiv e) w) = (equivOfRingEquiv (e.trans e')) w

Transporting an infinite place along e and then e' is transporting along e.trans e'.

theorem NumberField.InfinitePlace.equivOfRingEquiv_trans {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] (e : K ≃+* L) (e' : L ≃+* M) : equivOfRingEquiv (e.trans e') = (equivOfRingEquiv e).trans (equivOfRingEquiv e')

Transporting infinite places commutes with composing ring isomorphisms.

@[simp]

theorem NumberField.InfinitePlace.isReal_equivOfRingEquiv_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : InfinitePlace K) : ((equivOfRingEquiv e) w).IsReal ↔ w.IsReal

Transport along a ring isomorphism preserves realness of infinite places.

@[simp]

theorem NumberField.InfinitePlace.isComplex_equivOfRingEquiv_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : InfinitePlace K) : ((equivOfRingEquiv e) w).IsComplex ↔ w.IsComplex

Transport along a ring isomorphism preserves complexity of infinite places.

@[simp]

theorem NumberField.InfinitePlace.mult_equivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : InfinitePlace K) : ((equivOfRingEquiv e) w).mult = w.mult

Transport along a ring isomorphism preserves the multiplicity of an infinite place.

@[simp]

theorem NumberField.InfinitePlace.embedding_of_isReal_equivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) {w : InfinitePlace K} (hw : ((equivOfRingEquiv e) w).IsReal) : embedding_of_isReal hw = (embedding_of_isReal ⋯).comp ↑e.symm

The real embedding of a real place transported along e : K ≃+* L is the real embedding of the original place composed with e.symm.

def NumberField.InfinitePlace.realEquivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) : { w : InfinitePlace K // w.IsReal } ≃ { w : InfinitePlace L // w.IsReal }

The bijection between the real places of two fields induced by a ring isomorphism e : K ≃+* L.

@[simp]

theorem NumberField.InfinitePlace.coe_realEquivOfRingEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (w : { w : InfinitePlace K // w.IsReal }) : ↑((realEquivOfRingEquiv e) w) = (equivOfRingEquiv e) ↑w

The underlying infinite place of realEquivOfRingEquiv e w is equivOfRingEquiv e w.

@[simp]

theorem NumberField.InfinitePlace.realEquivOfRingEquiv_refl_apply {K : Type u_1} [Field K] (w : { w : InfinitePlace K // w.IsReal }) : (realEquivOfRingEquiv (RingEquiv.refl K)) w = w

The identity ring isomorphism induces the identity on real places.

theorem NumberField.InfinitePlace.realEquivOfRingEquiv_refl {K : Type u_1} [Field K] : realEquivOfRingEquiv (RingEquiv.refl K) = Equiv.refl { w : InfinitePlace K // w.IsReal }

The identity ring isomorphism induces Equiv.refl on the real places of K.

@[simp]

theorem NumberField.InfinitePlace.realEquivOfRingEquiv_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) : (realEquivOfRingEquiv e).symm = realEquivOfRingEquiv e.symm

Inverting the ring isomorphism inverts the induced bijection of real places.

@[simp]

theorem NumberField.InfinitePlace.realEquivOfRingEquiv_trans_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] (e : K ≃+* L) (e' : L ≃+* M) (w : { w : InfinitePlace K // w.IsReal }) : (realEquivOfRingEquiv e') ((realEquivOfRingEquiv e) w) = (realEquivOfRingEquiv (e.trans e')) w

Transporting a real place along e and then e' is transporting along e.trans e'.

theorem NumberField.InfinitePlace.realEquivOfRingEquiv_trans {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] (e : K ≃+* L) (e' : L ≃+* M) : realEquivOfRingEquiv (e.trans e') = (realEquivOfRingEquiv e).trans (realEquivOfRingEquiv e')

Transporting real places commutes with composing ring isomorphisms.