Theorem: embedding_conj (FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean)

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : K
φ : K →+* ℂ
⊢ (starRingEnd ℂ) (φ x) = φ ((galConj K p) x)
Tactic:
change RingHom.comp conj φ x = (φ.comp <| ↑(galConj K p)) x
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : K
φ : K →+* ℂ
⊢ ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x : K
φ : K →+* ℂ
⊢ ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Tactic:
revert x
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ ∀ (x : K), ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ ∀ (x : K), ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Tactic:
suffices φ (galConj K p ζ) = conj (φ ζ)
  by
  rw [← Function.funext_iff]
  congr
  rw [DFunLike.coe_fn_eq]
  apply (hζ.powerBasis ℚ).rat_hom_ext
  exact this.symm
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
Tactic:
rw [conj_norm_one, galConj_zeta_runity hζ, map_inv₀]
State after:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ Complex.abs (φ ζ) = 1

State before:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ Complex.abs (φ ζ) = 1
Tactic:
refine' Complex.norm_eq_one_of_pow_eq_one _ p.ne_zero
State after:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ζ ^ ↑p = 1

State before:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
⊢ φ ζ ^ ↑p = 1
Tactic:
rw [← map_pow, hζ.pow_eq_one, map_one]
State after:
no goals

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ ∀ (x : K), ((starRingEnd ℂ).comp φ) x = (φ.comp ↑(galConj K p)) x
Tactic:
rw [← Function.funext_iff]
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (fun x => ((starRingEnd ℂ).comp φ) x) = fun x => (φ.comp ↑(galConj K p)) x

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (fun x => ((starRingEnd ℂ).comp φ) x) = fun x => (φ.comp ↑(galConj K p)) x
Tactic:
rw [DFunLike.coe_fn_eq]
State after:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (starRingEnd ℂ).comp φ = φ.comp ↑(galConj K p)

State before:
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ (starRingEnd ℂ).comp φ = φ.comp ↑(galConj K p)
Tactic:
apply (hζ.powerBasis ℚ).rat_hom_ext
State after:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ ((starRingEnd ℂ).comp φ) (IsPrimitiveRoot.powerBasis ℚ hζ).gen =
    (φ.comp ↑(galConj K p)) (IsPrimitiveRoot.powerBasis ℚ hζ).gen

State before:
case h
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
φ : K →+* ℂ
this : φ ((galConj K p) ζ) = (starRingEnd ℂ) (φ ζ)
⊢ ((starRingEnd ℂ).comp φ) (IsPrimitiveRoot.powerBasis ℚ hζ).gen =
    (φ.comp ↑(galConj K p)) (IsPrimitiveRoot.powerBasis ℚ hζ).gen
Tactic:
exact this.symm
State after:
no goals