The canonical element at a ramified real place

Let L / K be a Galois extension and w a complex place of L lying above a real place of K, that is a place with w.IsRamified K. Exactly one nonidentity automorphism of L / K conjugates the embedding attached to w, and this file names it complexConjugationAt K w hw.

The place is part of the input. In a general Galois extension there is no place-independent conjugation element: Mathlib's IsCMField.complexConj picks one by choosing an embedding once and for all, which is available only for a CM field. Indexing by the place is what makes the element canonical in general, and the indexing is exactly what the API below records.

Everything here rests on Mathlib's embedding-level theory of ComplexEmbedding.IsConj, which already supplies existence at a ramified place (exists_isConj_of_isRamified), uniqueness (ComplexEmbedding.IsConj.ext), order two, and the description of the stabilizer. This file transports that theory to the place w itself and gives the resulting element a name; it does not restate any of it.

⚠ This element is not a Frobenius. At an infinite place the local Galois group is Gal(ℂ/ℝ): there is no residue field, and no congruence σ x ≡ x ^ q.

Main definitions

• TauCeti.NumberField.complexConjugationAt: the conjugation attached to a ramified place.

Main results

• TauCeti.NumberField.isConj_complexConjugationAt: it conjugates w.embedding.
• TauCeti.NumberField.eq_complexConjugationAt: it is the only automorphism that does, so the name is justified.
• TauCeti.NumberField.complexConjugationAt_ne_one and TauCeti.NumberField.orderOf_complexConjugationAt: it is nontrivial, of order two.
• TauCeti.NumberField.coe_stabilizer_eq_pair: the stabilizer of w is exactly the pair {1, c}, with TauCeti.NumberField.complexConjugationAt_mem_stabilizer recording the membership, TauCeti.NumberField.complexConjugationAt_smul_self the same fact as the equation c • w = w, and TauCeti.NumberField.eq_complexConjugationAt_of_mem_stabilizer_of_ne_one the resulting uniqueness among nonidentity elements.
• TauCeti.NumberField.complexConjugationAt_smul: the conjugation transforms by conjugacy, c (σ • w) = σ * c w * σ⁻¹.
• TauCeti.NumberField.complexConjugationAt_restrictNormal_of_isComplex and TauCeti.NumberField.complexConjugationAt_restrictNormal_eq_one_of_isReal: restriction to an intermediate field, in both branches. The restriction is the conjugation at the induced place when that place stays complex, and is trivial when the induced place is real.
• TauCeti.NumberField.isTotallyComplex_fixedField_of_complexConjugationAt_notMem: the fixed field of a subgroup of the Galois group of a totally complex field, containing no complex conjugation, is totally complex.

The general tower facts these rest on — equivariance of the action along the tower, and the ramification of a complex induced place — are in TauCeti/NumberTheory/NumberField/InfinitePlace/Tower.lean.

References

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

noncomputable def TauCeti.NumberField.complexConjugationAt (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) : Gal(L/K)

The canonical conjugation at a ramified place. For w a place of L ramified over K, this is the unique nonidentity element of Gal(L/K) conjugating the embedding of w.

The hypothesis hw is data of the statement, not decoration: at an unramified place any automorphism conjugating the embedding would have to be the identity, and there is nothing to name.

@[simp]

theorem TauCeti.NumberField.isConj_complexConjugationAt (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) : NumberField.ComplexEmbedding.IsConj w.embedding (complexConjugationAt K w hw)

complexConjugationAt K w hw conjugates the embedding attached to w.

theorem TauCeti.NumberField.eq_complexConjugationAt (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] {w : NumberField.InfinitePlace L} (hw : NumberField.InfinitePlace.IsRamified K w) {σ : Gal(L/K)} (hσ : NumberField.ComplexEmbedding.IsConj w.embedding σ) : σ = complexConjugationAt K w hw

Uniqueness. Any automorphism conjugating the embedding of w is complexConjugationAt, so the definition does not depend on the choice made to produce it.

@[simp]

theorem TauCeti.NumberField.complexConjugationAt_ne_one (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) : complexConjugationAt K w hw ≠ 1

The conjugation at a ramified place is not the identity: were it, the place would be unramified.

@[simp]

theorem TauCeti.NumberField.orderOf_complexConjugationAt (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) : orderOf (complexConjugationAt K w hw) = 2

The conjugation at a ramified place has order two, matching Gal(ℂ/ℝ).

theorem TauCeti.NumberField.coe_stabilizer_eq_pair (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) : ↑(MulAction.stabilizer Gal(L/K) w) = {1, complexConjugationAt K w hw}

The stabilizer of a ramified place is the pair {1, c}, for c the conjugation at that place.

theorem TauCeti.NumberField.complexConjugationAt_mem_stabilizer (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) : complexConjugationAt K w hw ∈ MulAction.stabilizer Gal(L/K) w

The conjugation at w fixes w.

@[simp]

theorem TauCeti.NumberField.complexConjugationAt_smul_self (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) : complexConjugationAt K w hw • w = w

The conjugation at w fixes w, as an equation. This is the simp normal form of complexConjugationAt_mem_stabilizer: MulAction.mem_stabilizer_iff rewrites that membership to this equation, so this is the shape simp can discharge.

theorem TauCeti.NumberField.eq_complexConjugationAt_of_mem_stabilizer_of_ne_one (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) {σ : Gal(L/K)} (hmem : σ ∈ MulAction.stabilizer Gal(L/K) w) (hne : σ ≠ 1) : σ = complexConjugationAt K w hw

Uniqueness among nonidentity stabilizer elements. An automorphism fixing a ramified place is either the identity or the conjugation at that place.

theorem TauCeti.NumberField.complexConjugationAt_smul (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w) (σ : Gal(L/K)) : complexConjugationAt K (σ • w) ⋯ = σ * complexConjugationAt K w hw * σ⁻¹

Conjugacy covariance. Moving the place by σ conjugates the element by σ.

Restriction in a normal tower

@[simp]

theorem TauCeti.NumberField.complexConjugationAt_restrictNormal_eq_one_of_isReal (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois 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) (hw : NumberField.InfinitePlace.IsRamified K w) (hv : (w.comap (algebraMap F L)).IsReal) : (complexConjugationAt K w hw).restrictNormal F = 1

The conjugation at w restricts trivially when the induced place on F is real.

@[simp]

theorem TauCeti.NumberField.complexConjugationAt_restrictNormal_of_isComplex (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois 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) (hw : NumberField.InfinitePlace.IsRamified K w) (hv : (w.comap (algebraMap F L)).IsComplex) : (complexConjugationAt K w hw).restrictNormal F = complexConjugationAt K (w.comap (algebraMap F L)) ⋯

The conjugation at w restricts to the conjugation at the induced complex place on F.

theorem TauCeti.NumberField.isTotallyComplex_fixedField_of_complexConjugationAt_notMem (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsGalois K L] [NumberField L] [NumberField.IsTotallyComplex L] (H : Subgroup Gal(L/K)) (hH : ∀ (w : NumberField.InfinitePlace L) (hw : NumberField.InfinitePlace.IsRamified K w), complexConjugationAt K w hw ∉ H) : NumberField.IsTotallyComplex ↥(IntermediateField.fixedField H)

The fixed field of a subgroup of the Galois group of a totally complex number field L over K is totally complex as soon as the subgroup contains no complex conjugation of a place of L ramified over K.