Ramification under field isomorphisms

The ramification index depends on the extension, not on its presentation as a field carrier: transporting a place of the upstairs field along an isomorphism over the downstairs field does not change its ramification index. This allows an extension to be placed in a finite Galois overfield without changing its ramification behaviour.

More generally, a commutative square of semilinear isomorphisms, σK : K ≃+* K' below and τ : L ≃+* L' above, carrying the constants k onto k' along σ, carries the place of L over P to a place of L' over the transport of P, with the same ramification index and the same relative degree (TauCeti.Place.restrict_equivOfRingEquiv, TauCeti.Place.ramificationIdx_equivOfRingEquiv_of_comm and TauCeti.Place.relativeDegree_equivOfRingEquiv_of_comm). The constants need not be fixed, so this is how a Galois automorphism of the constants acts on the places of a base-changed extension.

Over the identity of the constants these are TauCeti.Place.restrict_map, TauCeti.Place.ramificationIdx_map and TauCeti.Place.relativeDegree_map, for k-algebra isomorphisms. With K = K' and L = L' as fields, this is how a change of the embedding of the base field by an automorphism moves places and their ramification.

theorem TauCeti.Place.ramificationIdx_equivOfRingEquiv_of_comm {k : Type u_1} {k' : Type u_2} {K : Type u_3} {K' : Type u_4} {L : Type u_5} {L' : Type u_6} [Field k] [Field k'] [Field K] [Field K'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] [Algebra K L] [Algebra K' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (σK : K ≃+* K') (hK : ∀ (x : K), τ ((algebraMap K L) x) = (algebraMap K' L') (σK x)) (Q : Place k L) : ramificationIdx K' ((equivOfRingEquiv σ τ h) Q) = ramificationIdx K Q

The ramification index is invariant under a commutative square of semilinear isomorphisms: if τ : L ≃+* L' carries the image of K onto the image of K' along σK : K ≃+* K', then transporting a place of L along τ does not change its ramification index.

theorem TauCeti.Place.restrict_equivOfRingEquiv {k : Type u_1} {k' : Type u_2} {K : Type u_3} {K' : Type u_4} {L : Type u_5} {L' : Type u_6} [Field k] [Field k'] [Field K] [Field K'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] [Algebra K L] [Algebra K' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (σK : K ≃+* K') (hK : ∀ (x : K), τ ((algebraMap K L) x) = (algebraMap K' L') (σK x)) [Algebra k K] [Algebra k' K'] [IsScalarTower k K L] [IsScalarTower k' K' L'] [Algebra.IsIntegral K L] [Algebra.IsIntegral K' L'] (hσK : ∀ (c : k), σK ((algebraMap k K) c) = (algebraMap k' K') (σ c)) (Q : Place k L) : restrict k' K' ((equivOfRingEquiv σ τ h) Q) = (equivOfRingEquiv σ σK hσK) (restrict k K Q)

Restriction commutes with a commutative square of semilinear isomorphisms: if τ : L ≃+* L' carries the image of K onto the image of K' along σK : K ≃+* K', which carries the constants along σ, then the transport of a place Q of L lies over the transport of the place below Q.

theorem TauCeti.Place.relativeDegree_equivOfRingEquiv_of_comm {k : Type u_1} {k' : Type u_2} {K : Type u_3} {K' : Type u_4} {L : Type u_5} {L' : Type u_6} [Field k] [Field k'] [Field K] [Field K'] [Field L] [Field L'] [Algebra k L] [Algebra k' L'] [Algebra K L] [Algebra K' L'] (σ : k ≃+* k') (τ : L ≃+* L') (h : ∀ (c : k), τ ((algebraMap k L) c) = (algebraMap k' L') (σ c)) (σK : K ≃+* K') (hK : ∀ (x : K), τ ((algebraMap K L) x) = (algebraMap K' L') (σK x)) [Algebra k K] [Algebra k' K'] [IsScalarTower k K L] [IsScalarTower k' K' L'] [Algebra.IsIntegral K L] [Algebra.IsIntegral K' L'] (Q : Place k L) : relativeDegree k' K' ((equivOfRingEquiv σ τ h) Q) = relativeDegree k K Q

The relative degree is invariant under a commutative square of semilinear isomorphisms: if τ : L ≃+* L' carries the constants along σ and the image of K onto the image of K' along σK : K ≃+* K', then transporting a place of L along τ does not change its relative degree over the place below. The residue fields above and below are matched by τ and by σK.

@[simp]

theorem TauCeti.Place.ramificationIdx_equivOfRingEquiv {k : Type u_1} {F : Type u_2} {L : Type u_3} {L' : Type u_4} [Field k] [Field F] [Field L] [Field L'] [Algebra k F] [Algebra k L] [Algebra k L'] [Algebra F L] [Algebra F L'] [IsScalarTower k F L] [IsScalarTower k F L'] (e : L ≃ₐ[F] L') (Q : Place k L) : ramificationIdx F ((equivOfRingEquiv (RingEquiv.refl k) e.toRingEquiv ⋯) Q) = ramificationIdx F Q

The ramification index is invariant under an isomorphism of the upstairs field over the base field: transporting a place of L along e : L ≃ₐ[F] L' does not change its ramification index over F.

theorem TauCeti.Place.ramificationIdx_map {k : Type u_1} {L : Type u_3} {L' : Type u_4} [Field k] [Field L] [Field L'] [Algebra k L] [Algebra k L'] {K : Type u_5} {K' : Type u_6} [Field K] [Field K'] [Algebra K L] [Algebra K' L'] (e : L ≃ₐ[k] L') (σ : K ≃+* K') (he : ∀ (x : K), e ((algebraMap K L) x) = (algebraMap K' L') (σ x)) (Q : Place k L) : ramificationIdx K' (map e Q) = ramificationIdx K Q

The ramification index is invariant under a commutative square of isomorphisms: if e : L ≃ₐ[k] L' carries the image of K onto the image of K' along σ : K ≃+* K', then transporting a place of L along e does not change its ramification index.

theorem TauCeti.Place.restrict_map {k : Type u_1} {L : Type u_3} {L' : Type u_4} [Field k] [Field L] [Field L'] [Algebra k L] [Algebra k L'] {K : Type u_5} {K' : Type u_6} [Field K] [Field K'] [Algebra K L] [Algebra K' L'] (e : L ≃ₐ[k] L') [Algebra k K] [Algebra k K'] [IsScalarTower k K L] [IsScalarTower k K' L'] [Algebra.IsIntegral K L] [Algebra.IsIntegral K' L'] (σ : K ≃ₐ[k] K') (he : ∀ (x : K), e ((algebraMap K L) x) = (algebraMap K' L') (σ x)) (Q : Place k L) : restrict k K' (map e Q) = map σ (restrict k K Q)

Restriction commutes with a commutative square of isomorphisms: if e : L ≃ₐ[k] L' carries the image of K onto the image of K' along a k-algebra isomorphism σ, then the transport of a place Q of L lies over the transport of the place below Q.

theorem TauCeti.Place.relativeDegree_map {k : Type u_1} {L : Type u_3} {L' : Type u_4} [Field k] [Field L] [Field L'] [Algebra k L] [Algebra k L'] {K : Type u_5} {K' : Type u_6} [Field K] [Field K'] [Algebra K L] [Algebra K' L'] (e : L ≃ₐ[k] L') [Algebra k K] [Algebra k K'] [IsScalarTower k K L] [IsScalarTower k K' L'] [Algebra.IsIntegral K L] [Algebra.IsIntegral K' L'] (σ : K ≃+* K') (he : ∀ (x : K), e ((algebraMap K L) x) = (algebraMap K' L') (σ x)) (Q : Place k L) : relativeDegree k K' (map e Q) = relativeDegree k K Q

The relative degree is invariant under a commutative square of isomorphisms: if e : L ≃ₐ[k] L' carries the image of K onto the image of K' along σ : K ≃+* K', then transporting a place of L along e does not change its relative degree.