Complex conjugation and the cyclotomic character #
The conjugation attached to a complex infinite place above a real place acts on roots of unity
by inversion. Its cyclotomic exponent is therefore -1. This identifies the arithmetic
complex-conjugation element when a character on modular units is used to cut out a subfield.
Reference #
- J. S. Milne, Class Field Theory, Chapter VII, Lemma 7.3, https://www.jmilne.org/math/CourseNotes/CFT.pdf.
theorem
IsPrimitiveRoot.autToPow_complexConjugationAt
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[IsGalois K L]
{m : ℕ}
[NeZero m]
{ζ : L}
(hζ : IsPrimitiveRoot ζ m)
(w : NumberField.InfinitePlace L)
(hw : NumberField.InfinitePlace.IsRamified K w)
:
Complex conjugation at a ramified infinite place has cyclotomic exponent -1 on every
primitive root of unity.