Transport of places along isomorphisms

A k-algebra isomorphism e : F ≃ₐ[k] F' carries a place P of F / k to the place P.map e of F' / k whose valuation is v_P ∘ e⁻¹. Normalization is preserved because e is bijective, and triviality on the constants because e commutes with the structure maps from k. The construction is the one behind the action of Aut(F' / F) on the places of F' / k (TauCeti.Place.instMulActionAlgEquiv), which it extends to isomorphisms between different fields; the two agree on automorphisms (TauCeti.Place.smul_eq_map).

Main definitions

• TauCeti.Place.map: the place P.map e of F' obtained from a place P of F and an isomorphism e : F ≃ₐ[k] F'.
• TauCeti.Place.mapEquiv: the resulting bijection between the places of F and those of F'.

Main results

• TauCeti.Place.valuation_map_apply and TauCeti.Place.ord_map_apply: e carries the valuation and the order function of P to those of P.map e.
• TauCeti.Place.integersEquivMap and TauCeti.Place.residueFieldEquivMap: e carries the valuation ring and the residue field of P isomorphically onto those of P.map e.
• TauCeti.Place.degree_map: transport preserves the degree of a place.

def TauCeti.Place.map {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) : Place k F'

Transport of a place along an isomorphism: the place P.map e of F' / k whose valuation is v_P ∘ e⁻¹, for a k-algebra isomorphism e : F ≃ₐ[k] F' and a place P of F / k.

Equations

• TauCeti.Place.map e P = { valuation := Valuation.comap (↑e.symm) P.valuation, valuation_surjective := ⋯, isTrivialOn := ⋯ }

@[simp]

theorem TauCeti.Place.valuation_map {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (x : F') : (map e P).valuation x = P.valuation (e.symm x)

The defining property of transport: the valuation of P.map e is the valuation of P composed with e⁻¹.

theorem TauCeti.Place.valuation_map_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (x : F) : (map e P).valuation (e x) = P.valuation x

Transport moves the valuation along e.

@[simp]

theorem TauCeti.Place.ord_map {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (x : F') : (map e P).ord x = P.ord (e.symm x)

The order function of P.map e is the order function of P composed with e⁻¹.

theorem TauCeti.Place.ord_map_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (x : F) : (map e P).ord (e x) = P.ord x

Transport moves the order function along e.

theorem TauCeti.Place.mem_integers_map_iff {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) {x : F'} : x ∈ (map e P).integers ↔ e.symm x ∈ P.integers

Membership in the valuation ring of P.map e, read off at P.

@[simp]

theorem TauCeti.Place.map_refl {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (P : Place k F) : map AlgEquiv.refl P = P

Transport along the identity is the identity.

@[simp]

theorem TauCeti.Place.map_map {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) {F'' : Type u_1} [Field F''] [Algebra k F''] (e' : F' ≃ₐ[k] F'') : map e' (map e P) = map (e.trans e') P

Transport respects composition: transporting along e and then along e' is transport along e.trans e'.

theorem TauCeti.Place.map_symm_map {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) : map e.symm (map e P) = P

Transport along e.symm undoes transport along e.

theorem TauCeti.Place.map_map_symm {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (Q : Place k F') : map e (map e.symm Q) = Q

Transport along e undoes transport along e.symm.

def TauCeti.Place.mapEquiv {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') : Place k F ≃ Place k F'

Transport is a bijection between the places of F / k and those of F' / k, with inverse the transport along e⁻¹.

Equations

• TauCeti.Place.mapEquiv e = { toFun := TauCeti.Place.map e, invFun := TauCeti.Place.map e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.Place.mapEquiv_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) : (mapEquiv e) P = map e P

@[simp]

theorem TauCeti.Place.mapEquiv_symm_apply {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (Q : Place k F') : (mapEquiv e).symm Q = map e.symm Q

def TauCeti.Place.integersEquivMap {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) : ↥P.integers ≃+* ↥(map e P).integers

Transport of the valuation ring: e carries the valuation ring of P isomorphically onto the valuation ring of P.map e.

Equations

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

@[simp]

theorem TauCeti.Place.coe_integersEquivMap {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (x : ↥P.integers) : ↑((integersEquivMap e P) x) = e ↑x

@[simp]

theorem TauCeti.Place.coe_integersEquivMap_symm {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (y : ↥(map e P).integers) : ↑((integersEquivMap e P).symm y) = e.symm ↑y

@[simp]

theorem TauCeti.Place.integersEquivMap_algebraMap {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (c : k) : (integersEquivMap e P) ((algebraMap k ↥P.integers) c) = (algebraMap k ↥(map e P).integers) c

e carries the constants of 𝒪_P to the constants of 𝒪_{P.map e}.

noncomputable def TauCeti.Place.residueFieldEquivMap {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) : P.ResidueField ≃ₐ[k] (map e P).ResidueField

Transport of the residue field: the k-algebra isomorphism F_P ≃ F_{P.map e} of residue fields induced by e.

Equations

• TauCeti.Place.residueFieldEquivMap e P = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem TauCeti.Place.residueFieldEquivMap_residue {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) (x : ↥P.integers) : (residueFieldEquivMap e P) ((IsLocalRing.residue ↥P.integers) x) = (IsLocalRing.residue ↥(map e P).integers) ((integersEquivMap e P) x)

The residue-field isomorphism of transport sends the residue of x at P to the residue of e x at P.map e.

@[simp]

theorem TauCeti.Place.degree_map {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (e : F ≃ₐ[k] F') (P : Place k F) : (map e P).degree = P.degree

Transport preserves the degree of a place: e identifies the residue fields of P and P.map e as k-algebras.