theorem PowerBasis.rat_hom_ext {S : Type u_1} {S' : Type u_2} [CommRing S] [hS : Algebra ℚ S] [Ring S'] [hS' : Algebra ℚ S'] (pb : PowerBasis ℚ S) ⦃f : S →+* S'⦄ ⦃g : S →+* S'⦄ (h : ↑f pb.gen = ↑g pb.gen) : f = g

def galConj (K : Type u_1) (p : ℕ+) [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] : K ≃ₐ[ℚ] K

complex conjugation as a Galois automorphism

Equations

• galConj K p = ↑(MulEquiv.symm (IsCyclotomicExtension.autEquivPow K (_ : Irreducible (Polynomial.cyclotomic ↑p ℚ)))) (-1)

theorem ZMod.val_neg_one' {n : ℕ} : 0 < n → ZMod.val (-1) = n - 1

theorem galConj_zeta {K : Type u_1} {p : ℕ+} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] : ↑(galConj K p) (IsCyclotomicExtension.zeta p ℚ K) = (IsCyclotomicExtension.zeta p ℚ K)⁻¹

@[simp]

theorem galConj_zeta_runity {K : Type u_1} {p : ℕ+} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) : ↑(galConj K p) ζ = ζ⁻¹

theorem galConj_zeta_runity_pow {K : Type u_1} {p : ℕ+} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (n : ℕ) : ↑(galConj K p) (ζ ^ n) = ζ⁻¹ ^ n

theorem conj_norm_one (x : ℂ) (h : ↑Complex.abs x = 1) : ↑(starRingEnd ℂ) x = x⁻¹

@[simp]

theorem embedding_conj {K : Type u_1} {p : ℕ+} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (x : K) (φ : K →+* ℂ) : ↑(starRingEnd ((fun x => ℂ) x)) (↑φ x) = ↑φ (↑(galConj K p) x)

theorem galConj_idempotent {K : Type u_1} {p : ℕ+} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] : AlgEquiv.trans (galConj K p) (galConj K p) = AlgEquiv.refl

theorem gal_map_mem {K : Type u_1} [Field K] [CharZero K] {x : K} (hx : x ∈ NumberField.ringOfIntegers K) (σ : K →ₐ[ℚ] K) : ↑σ x ∈ NumberField.ringOfIntegers K

theorem gal_map_mem_subtype {K : Type u_1} [Field K] [CharZero K] (σ : K →ₐ[ℚ] K) (x : { x // x ∈ NumberField.ringOfIntegers K }) : ↑σ ↑x ∈ NumberField.ringOfIntegers K

def intGal {K : Type u_1} [Field K] [CharZero K] (σ : K →ₐ[ℚ] K) : { x // x ∈ NumberField.ringOfIntegers K } →ₐ[ℤ] { x // x ∈ NumberField.ringOfIntegers K }

Restriction of σ : K →ₐ[ℚ] K to the ring of integers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem intGal_apply_coe {K : Type u_1} [Field K] [CharZero K] (σ : K →ₐ[ℚ] K) (x : { x // x ∈ NumberField.ringOfIntegers K }) : ↑(↑(intGal σ) x) = ↑σ ↑x

def unitsGal {K : Type u_1} [Field K] [CharZero K] (σ : K →ₐ[ℚ] K) : { x // x ∈ NumberField.ringOfIntegers K }ˣ →* { x // x ∈ NumberField.ringOfIntegers K }ˣ

Restriction of σ : K →ₐ[ℚ] K to the units of the ring of integers.

Equations

• unitsGal σ = Units.map ↑(intGal σ)

def unitGalConj (K : Type u_1) (p : ℕ+) [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] : { x // x ∈ NumberField.ringOfIntegers K }ˣ →* { x // x ∈ NumberField.ringOfIntegers K }ˣ

unit_gal_conj as a bundled hom.

Equations

• unitGalConj K p = unitsGal ↑(galConj K p)

theorem unitGalConj_spec (K : Type u_1) (p : ℕ+) [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) : ↑(galConj K p) ↑↑u = ↑↑(↑(unitGalConj K p) u)

theorem unit_lemma_val_one {K : Type u_1} (p : ℕ+) [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (φ : K →+* ℂ) : ↑Complex.abs (↑φ (↑↑u * ↑↑(↑(unitGalConj K p) u)⁻¹)) = 1