[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ↑(ghostComponent n) (teichmullerFun p r) = r ^ p ^ n
[PROOFSTEP]
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul, tsub_zero]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ coeff (teichmullerFun p r) 0 ^ p ^ n = r ^ p ^ n
[PROOFSTEP]
rfl
[GOAL]
case h₀
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ∀ (b : ℕ), b ∈ Finset.range (n + 1) → b ≠ 0 → ↑p ^ b * coeff (teichmullerFun p r) b ^ p ^ (n - b) = 0
[PROOFSTEP]
intro i hi h0
[GOAL]
case h₀
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ ↑p ^ i * coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
[PROOFSTEP]
convert mul_zero (M₀ := R) _
[GOAL]
case h.e'_2.h.e'_6
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i ^ p ^ (n - i) = 0
[PROOFSTEP]
convert zero_pow (M := R) _
[GOAL]
case h.e'_2.h.e'_5
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ coeff (teichmullerFun p r) i = 0
[PROOFSTEP]
cases i
[GOAL]
case h.e'_2.h.e'_5.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
hi : Nat.zero ∈ Finset.range (n + 1)
h0 : Nat.zero ≠ 0
⊢ coeff (teichmullerFun p r) Nat.zero = 0
[PROOFSTEP]
contradiction
[GOAL]
case h.e'_2.h.e'_5.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n n✝ : ℕ
hi : Nat.succ n✝ ∈ Finset.range (n + 1)
h0 : Nat.succ n✝ ≠ 0
⊢ coeff (teichmullerFun p r) (Nat.succ n✝) = 0
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.h.e'_6.convert_2
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n i : ℕ
hi : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ 0 < p ^ (n - i)
[PROOFSTEP]
exact pow_pos hp.1.pos _
[GOAL]
case h₁
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 ∈ Finset.range (n + 1) → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
[PROOFSTEP]
rw [Finset.mem_range]
[GOAL]
case h₁
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
[PROOFSTEP]
intro h
[GOAL]
case h₁
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
n : ℕ
h : ¬0 < n + 1
⊢ ↑p ^ 0 * coeff (teichmullerFun p r) 0 ^ p ^ (n - 0) = 0
[PROOFSTEP]
exact (h (Nat.succ_pos n)).elim
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ ↑(map f) (teichmullerFun p r) = teichmullerFun p (↑f r)
[PROOFSTEP]
ext n
[GOAL]
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) n = coeff (teichmullerFun p (↑f r)) n
[PROOFSTEP]
cases n
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ coeff (↑(map f) (teichmullerFun p r)) Nat.zero = coeff (teichmullerFun p (↑f r)) Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) (Nat.succ n✝) = coeff (teichmullerFun p (↑f r)) (Nat.succ n✝)
[PROOFSTEP]
exact f.map_zero
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
[PROOFSTEP]
apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x * teichmullerFun p y)
[PROOFSTEP]
rw [RingHom.map_mul]
[GOAL]
case a
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)
[PROOFSTEP]
ext1 n
[GOAL]
case a.h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
n : ℕ
⊢ ↑ghostMap (teichmullerFun p (x * y)) n = (↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)) n
[PROOFSTEP]
simp only [Pi.mul_apply, ghostMap_apply, ghostComponent_teichmullerFun, mul_pow]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
[PROOFSTEP]
refine' map_injective (MvPolynomial.map (Int.castRingHom ℚ)) (MvPolynomial.map_injective _ Int.cast_injective) _
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p (x * y)) =
    ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p x * teichmullerFun p y)
[PROOFSTEP]
simp only [teichmuller_mul_aux₁, map_teichmullerFun, RingHom.map_mul]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ teichmullerFun p 1 = 1
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (teichmullerFun p 1) Nat.zero = coeff 1 Nat.zero
[PROOFSTEP]
rw [one_coeff_zero]
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (teichmullerFun p 1) Nat.zero = 1
[PROOFSTEP]
rfl
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (teichmullerFun p 1) (Nat.succ n✝) = coeff 1 (Nat.succ n✝)
[PROOFSTEP]
rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (teichmullerFun p 1) (Nat.succ n✝) = 0
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (x y : R),
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (x * y) =
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } x *
        OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } y
[PROOFSTEP]
intro x y
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : R
⊢ OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (x * y) =
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } x *
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } y
[PROOFSTEP]
rcases counit_surjective R x with ⟨x, rfl⟩
[GOAL]
case intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
y : R
x : MvPolynomial R ℤ
⊢ OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x * y) =
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x) *
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } y
[PROOFSTEP]
rcases counit_surjective R y with ⟨y, rfl⟩
[GOAL]
case intro.intro
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x * ↑(counit R) y) =
    OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) x) *
      OneHom.toFun { toFun := teichmullerFun p, map_one' := (_ : teichmullerFun p 1 = 1) } (↑(counit R) y)
[PROOFSTEP]
simp only [← map_teichmullerFun, ← RingHom.map_mul, teichmuller_mul_aux₂]
[GOAL]
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑(teichmuller p) 0 = 0
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (↑(teichmuller p) 0) Nat.zero = coeff 0 Nat.zero
[PROOFSTEP]
rw [zero_coeff]
[GOAL]
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ coeff (↑(teichmuller p) 0) Nat.zero = 0
[PROOFSTEP]
rfl
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (↑(teichmuller p) 0) (Nat.succ n✝) = coeff 0 (Nat.succ n✝)
[PROOFSTEP]
rw [zero_coeff]
[GOAL]
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
n✝ : ℕ
⊢ coeff (↑(teichmuller p) 0) (Nat.succ n✝) = 0
[PROOFSTEP]
rfl
