Taylor Kim note chapter 01 #741
Conversation
| {p : ℕ} (pp : p.Prime) (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) : Nonempty FLT.FreyPackage := | ||
| FLT.FreyPackage.of_not_FermatLastTheorem_p_ge_5 ha hb hc pp hp5 H | ||
|
|
||
| def IsBadReduction (C : WeierstrassCurve ℚ) (p : ℕ) [Fact (Nat.Prime p)] :Prop:= sorry |
There was a problem hiding this comment.
It would be an interesting project to write down this definition.
| variable (p : ℕ) [Fact (Nat.Prime p)] | ||
|
|
||
| lemma badreduction (P : FreyPackage) : | ||
| IsBadReduction (FreyCurve P) p ↔ ((p : Int) ∣ (P.a * P.b * P.c)):= sorry |
There was a problem hiding this comment.
It would also be an interesting project to prove this theorem! Both ways are probably possible -- you could first prove that if the valuation of the j-invariant is negative then the curve has bad reduction, and then for p coprime to abc you could explicitly check that it has good reduction. This would teach you something about eliptic curves and probably about p-adic fields as well.
| lemma badreduction (P : FreyPackage) : | ||
| IsBadReduction (FreyCurve P) p ↔ ((p : Int) ∣ (P.a * P.b * P.c)):= sorry | ||
|
|
||
| local notation "G_K" => absoluteGaloisGroup |
There was a problem hiding this comment.
I think \Gamma is better notation, I don't think notation should have random letters like K in it.
|
|
||
| noncomputable instance AddCommMonoid | ||
| (q : IsLocalRing.maximalIdeal ℤ_[p]) (hq : (q : ℚ_[p]) ≠ 0) : AddCommMonoid (G p q hq) | ||
| := by infer_instance |
There was a problem hiding this comment.
If the proof is by infer_instance then you don't need it in the first place.
| def twist (ρ : Representation ℤ G M) (δ : G →* ℤˣ) : Representation ℤ G M where | ||
| toFun g := { | ||
| toFun m := δ g • ρ g m | ||
| map_add' := by aesop |
There was a problem hiding this comment.
This is probably quite slow. Does grind do it? Can you just prove it easily by hand?
There was a problem hiding this comment.
It seems that grind doesn’t work here, I changed to a simpler version by hand
|
|
||
| section | ||
| include q hq P hPp δ hqδ | ||
| lemma q_equation : ∃(C : ℕ → ℚ_[p]), (FreyCurve P).j= |
There was a problem hiding this comment.
C takes values in Z! And you might just want to remove the 744 and sum over all of Nat, and then just put in a lemma saying C 0 = 744.
| (q : ℚ_[p])⁻¹ + 744 + ∑' n : ℕ+, (C n) * q^(n:ℕ) := sorry | ||
|
|
||
| lemma p_valuation : Padic.valuation ((FreyCurve P).j : ℚ_[p]) | ||
| = Padic.valuation (q : ℚ_[p])⁻¹ := sorry |
There was a problem hiding this comment.
This says "for all q, v(j)=v(q)^{-1} as far as I can see.
| lemma p_valuation_mod (hp : Odd p) : | ||
| ((Padic.valuation (p := p ) (q:ℤ_[p])) : ZMod (2*P.p)) = 0 := sorry | ||
|
|
||
| lemma p_valuation_mod2 : ((Padic.valuation (p := p ) (q:ℤ_[p])) : ZMod 2) = -8 := sorry |
There was a problem hiding this comment.
Similarly this says "for all q, the p-adic valuation of q, when reduced mod 2, is -8", which is surely far from what you want to say.
| {M₁ M₂ : Type*} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] | ||
| (ρ₁ : Representation R G M₁) (ρ₂ : Representation R G M₂) | ||
| extends M₁ ≃ₗ[R] M₂ where | ||
| exchange : ∀(g : G), ∀(m : M₁), toFun (ρ₁ g m) = (ρ₂ g (toFun m)) |
There was a problem hiding this comment.
You might want to PR this to mathlib
| extends M₁ ≃ₗ[R] M₂ where | ||
| exchange : ∀(g : G), ∀(m : M₁), toFun (ρ₁ g m) = (ρ₂ g (toFun m)) | ||
|
|
||
| def twist (ρ : Representation ℤ G M) (δ : G →* ℤˣ) : Representation ℤ G M where |
There was a problem hiding this comment.
This too! In the right generality (general base commring R)
3 participants
This is part of the formalization of Taylor Kim notes chapter 01.