Infinite places in a normal tower

For a tower K ⊆ F ⊆ L with F / K normal, restriction of automorphisms along AlgEquiv.restrictNormal is compatible with the Galois action on infinite places: moving a place of L by σ and then inducing a place of F gives the same place as inducing first and then moving by the restricted automorphism.

The general tower API also identifies places over a fixed base place with pairs of successive places through the intermediate field. Two consequences of the Galois-action compatibility are recorded here too. A place of F induced by a place of L ramified over K is itself ramified over K as soon as it stays complex, because both places lie over the same place of K. And an automorphism restricting trivially to F is itself trivial whenever it fixes a place that is unramified over F, because such a place has trivial stabilizer in Gal(L/F).

Nothing here mentions complex conjugation: these are general facts about the action on places, used by TauCeti/NumberTheory/NumberField/ComplexConjugation/Basic.lean.

Main results

• AlgEquiv.restrictNormal_smul_comap: the action is equivariant along the tower.
• NumberField.InfinitePlace.liesOverTowerEquiv: places over a fixed place correspond to pairs of successive places through an intermediate field.
• TauCeti.NumberField.isRamified_comap_of_isComplex: a complex induced place is itself ramified.
• TauCeti.NumberField.eq_one_of_restrictNormal_eq_one: an automorphism restricting trivially to F and fixing a place unramified over F is the identity.

References

• J. Neukirch, Algebraic Number Theory, Chapter III, §3.

def NumberField.InfinitePlace.liesOverTowerEquiv {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] (v : InfinitePlace K) : (w : { w : InfinitePlace L // w.LiesOver v }) × { u : InfinitePlace M // u.LiesOver ↑w } ≃ { u : InfinitePlace M // u.LiesOver v }

Infinite places over v correspond to pairs of successive infinite places through an intermediate field.

@[simp]

theorem NumberField.InfinitePlace.liesOverTowerEquiv_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] (v : InfinitePlace K) (p : (w : { w : InfinitePlace L // w.LiesOver v }) × { u : InfinitePlace M // u.LiesOver ↑w }) : ↑(v.liesOverTowerEquiv p) = ↑p.snd

@[simp]

theorem NumberField.InfinitePlace.liesOverTowerEquiv_symm_apply_fst {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] (v : InfinitePlace K) (u : { u : InfinitePlace M // u.LiesOver v }) : ↑(v.liesOverTowerEquiv.symm u).fst = (↑u).comap (algebraMap L M)

The inverse of liesOverTowerEquiv passes through the place u induces on L.

@[simp]

theorem NumberField.InfinitePlace.liesOverTowerEquiv_symm_apply_snd {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra L M] [Algebra K M] [IsScalarTower K L M] (v : InfinitePlace K) (u : { u : InfinitePlace M // u.LiesOver v }) : ↑(v.liesOverTowerEquiv.symm u).snd = ↑u

The inverse of liesOverTowerEquiv keeps u as the top place.

@[simp]

theorem AlgEquiv.restrictNormal_smul_comap (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] {F : Type u_3} [Field F] [Algebra K F] [Algebra F L] [IsScalarTower K F L] [Normal K F] (σ : Gal(L/K)) (w : NumberField.InfinitePlace L) : σ.restrictNormal F • w.comap (algebraMap F L) = (σ • w).comap (algebraMap F L)

The Galois action on infinite places is equivariant along a normal tower. Restricting σ to F and then moving the place w induces on F gives the same place as moving w by σ and inducing afterwards.

theorem TauCeti.NumberField.isRamified_comap_of_isComplex (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] {F : Type u_3} [Field F] [Algebra K F] [Algebra F L] [IsScalarTower K F L] {w : NumberField.InfinitePlace L} (hreal : (w.comap (algebraMap K L)).IsReal) (hv : (w.comap (algebraMap F L)).IsComplex) : NumberField.InfinitePlace.IsRamified K (w.comap (algebraMap F L))

A complex induced place above a real place is ramified. The place w induces on F lies over the same place of K that w does, so if that place is real and the induced place is complex, then the induced place is ramified over K.

theorem TauCeti.NumberField.eq_one_of_restrictNormal_eq_one (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] {F : Type u_3} [Field F] [Algebra K F] [Algebra F L] [IsScalarTower K F L] [Normal K F] {w : NumberField.InfinitePlace L} (hu : NumberField.InfinitePlace.IsUnramified F w) {σ : Gal(L/K)} (hσ : σ • w = w) (h1 : σ.restrictNormal F = 1) : σ = 1

An automorphism restricting trivially to F and fixing a place unramified over F is the identity.