tensor of non-commutative ring

Stream: new members

[Chengyan Hu]

Hi! I found out that we don't have tensor product for modules over non-commutative ring in lean, I tried several ways to deal with that but still found no idea. The issue occurs in the last line of the code.
I tried to use tensor product of representation, but that's still only appliable for commutative ring.

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
→ ∃ (δ : Representation ℤ (G_K ℚ_[p]) (Additive ℤˣ)), ∃ (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

[Eric Wieser]

To be clear, you mean A ⊗[R] B where R is non-commutative?

[Chengyan Hu]

yes! In particular , (G p q hq)⊗[ℤ[G] (G_K ℚ_[p])] δ.asModule)

[Eric Wieser]

I think #7152 is one of the blockers here

[Chengyan Hu]

let me have a look

[Chengyan Hu]

yes I finished reading this, and the explain make sense for me. However I still have no idea how to solve my specific problem.

[Chengyan Hu]

I just realized this is a much bigger problem than I thought