Fail in write a representation as module

Stream: new members

[Chengyan Hu]

Hi! I'm trying to write the representation δ : (G_K ℚ_[p]) →* ℤˣ as a G_K ℚ_[p] module. (where G_K ℚ_[p] means the absolute Galois group of Q_[p]) . It seems that Representation.asModule can't work here as it's not a typical representation.

[Aaron Liu]

Can you elaborate?

[Aaron Liu]

a #mwe would be nice

[Chengyan Hu]

(deleted)

[Aaron Liu]

Can you post a version that works in the web editor (without having to import FLT)?

[Aaron Liu]

I still don't know what you mean when you say you want to write δ as a G_K ℚ_[p]-module

[Chengyan Hu]

Aaron Liu said:

Can you post a version that works in the web editor (without having to import FLT)?

I’ll try, but I’m afraid it gonna be hard

[Chengyan Hu]

It’s in the last line of the last theorem I want to claim

[Aaron Liu]

Can you explain how you want to interpret δ as a G_K ℚ_[p]-module?

[Chengyan Hu]

Here I hope to give ℤˣ a G_K Q_[p]-module structruce, where the scalar product is defined by \delta

[Aaron Liu]

What's the AddCommGroup structure that you want to put on ℤˣ?

[Aaron Liu]

based on the code you gave I'm assuming you actually want a ℤ[G_K ℚ_[p]]-module structure on ℤˣ

[Chengyan Hu]

It’s the normal multiplicative group structure inherit from Z, just use Additive as you mentioned to me in another post to change into AddCommGroup

[Chengyan Hu]

import Mathlib
open Field
open scoped TensorProduct

local notation "ℤ[G]" => MonoidAlgebra ℤ
local notation "G_K" => absoluteGaloisGroup
variable (ℓ : ℕ) [Fact (Nat.Prime ℓ)]

structure FreyPackage where
  a : ℤ
  b : ℤ
  c : ℤ
  ha0 : a ≠ 0
  hb0 : b ≠ 0
  hc0 : c ≠ 0
  p : ℕ
  pp : Nat.Prime p
  hp5 : 5 ≤ p
  hFLT : a ^ p + b ^ p = c ^ p
  hgcdab : gcd a b = 1 -- same as saying a,b,c pairwise coprime
  ha4 : (a : ZMod 4) = 3
  hb2 : (b : ZMod 2) = 0

namespace FreyPackage

def IsBadReduction (C : WeierstrassCurve ℚ) (p : ℕ) [Fact (Nat.Prime p)] :Prop:= sorry
def FreyCurveSimple (P : FreyPackage) : WeierstrassCurve ℚ := sorry

abbrev E_pclosure (C : WeierstrassCurve ℚ) (p : ℕ) [Fact (Nat.Prime p)] : Type :=
  (C.map (algebraMap ℚ (AlgebraicClosure ℚ_[p])) ).toAffine.Point

noncomputable instance CommGroupstructure (C : WeierstrassCurve ℚ) :
 AddCommGroup (E_pclosure C ℓ):= by classical infer_instance

noncomputable instance Modulestructue (C : WeierstrassCurve ℚ) :
Module (ℤ[G] (G_K ℚ_[ℓ])) (E_pclosure C ℓ) := sorry

abbrev G (q : IsLocalRing.maximalIdeal ℤ_[ℓ]) (hq : (q : ℚ_[ℓ]) ≠ 0) :
 Type := Additive (ℚ_[ℓ]ˣ⧸(Subgroup.closure ({Units.mk0 (q: ℚ_[ℓ]) hq})))

noncomputable instance AddCommMonoid
(q : IsLocalRing.maximalIdeal ℤ_[ℓ]) (hq : (q : ℚ_[ℓ]) ≠ 0) : AddCommMonoid (G ℓ q hq)
:= by infer_instance

noncomputable instance Modulestructue1
(q : IsLocalRing.maximalIdeal ℤ_[ℓ]) (hq : (q : ℚ_[ℓ]) ≠ 0) :
Module (ℤ[G] (G_K ℚ_[ℓ])) (G ℓ q hq) := sorry

theorem Tate (P : FreyPackage) (p : ℕ) [Fact (Nat.Prime p)] : IsBadReduction (FreyCurveSimple P) p
→ ∃ (δ : (G_K ℚ_[p]) →* ℤˣ), ∃ (q : IsLocalRing.maximalIdeal ℤ_[p]) (hq : (q : ℚ_[p]) ≠ 0),
Nonempty ((E_pclosure (FreyCurveSimple P) p) ≃ₗ[ℤ[G] (G_K ℚ_[p])] ((G p q hq)⊗[ℤ[G] (G_K ℚ_[p])] δ.asModule)) := sorry

[Chengyan Hu]

here is a version without FLT

[Chengyan Hu]

I edited again to a better version

[Aaron Liu]

Maybe you can write (δ : Representation ℤ (G_K ℚ_[p]) (Additive ℤˣ)) instead?

[Chengyan Hu]

I believe some significant issue is occuring here. After changed the error is failed to synthesize CommSemiring (ℤ[G] (G_K ℚ_[p])), but this group ring is clearly not commutative

[Chengyan Hu]

Seems the usual tensor in lean doesn't work with non-commutative ring?

[Aaron Liu]

yes that is correct