Restriction of places along a stable intermediate field

Let E be an intermediate field of L / k carried onto itself by every k-automorphism of L, so that automorphisms restrict to E through IntermediateField.restrictAlgEquivHom. The restriction of places from L / k to E / k is then equivariant: the place σ • Q lies over σ|_E • (Q|_E), and the ramification index of σ • Q over E is that of Q. These are the compatibilities needed to let Aut(L / k) act on the places of E that ramify in L.

These results generalize TauCeti.Place.restrict_smul and TauCeti.Place.ramificationIdx_smul of TauCeti/FieldTheory/FunctionField/Place/Extension/Galois.lean, which treat automorphisms fixing E pointwise, so that σ|_E is the identity there; the proofs follow the same order computation.

Main results

• TauCeti.Place.restrict_smul_of_map_eq: restriction to E is equivariant.
• TauCeti.Place.ramificationIdx_smul_of_map_eq: the ramification index over E is invariant.

theorem TauCeti.Place.ord_smul_algebraMap_of_map_eq {k : Type u_1} {L : Type u_2} [Field k] [Field L] [Algebra k L] (E : IntermediateField k L) [Algebra.IsIntegral (↥E) L] (hE : ∀ (σ : Gal(L/k)), IntermediateField.map (↑σ) E = E) (σ : Gal(L/k)) (Q : Place k L) (f : ↥E) : (σ • Q).ord ((algebraMap (↥E) L) f) = ↑(ramificationIdx (↥E) Q) * ((E.restrictAlgEquivHom hE) σ • restrict k (↥E) Q).ord f

The order at σ • Q of an element of E is e(Q ∣ E) times its order at σ|_E • (Q|_E).

@[simp]

theorem TauCeti.Place.restrict_smul_of_map_eq {k : Type u_1} {L : Type u_2} [Field k] [Field L] [Algebra k L] (E : IntermediateField k L) [Algebra.IsIntegral (↥E) L] (hE : ∀ (σ : Gal(L/k)), IntermediateField.map (↑σ) E = E) (σ : Gal(L/k)) (Q : Place k L) : restrict k (↥E) (σ • Q) = (E.restrictAlgEquivHom hE) σ • restrict k (↥E) Q

Restriction of places is equivariant: σ • Q lies over σ|_E • (Q|_E).

@[simp]

theorem TauCeti.Place.ramificationIdx_smul_of_map_eq {k : Type u_1} {L : Type u_2} [Field k] [Field L] [Algebra k L] (E : IntermediateField k L) [Algebra.IsIntegral (↥E) L] (hE : ∀ (σ : Gal(L/k)), IntermediateField.map (↑σ) E = E) (σ : Gal(L/k)) (Q : Place k L) : ramificationIdx (↥E) (σ • Q) = ramificationIdx (↥E) Q

The ramification index over a stable intermediate field is invariant under the automorphisms of L / k.