import Mathlib.NumberTheory.Padics.RingHoms
import Mathlib.RingTheory.AdicCompletion.RingHom
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.LinearAlgebra.LinearIndependent.Lemmas
import Mathlib.FieldTheory.Finiteness
import Mathlib.Algebra.Module.ZMod
import Mathlib.Algebra.Field.ZMod
import Mathlib.GroupTheory.Coset.Card
import Mathlib.GroupTheory.QuotientGroup.Basic
import Mathlib.Algebra.Group.Subgroup.Finite
import Definitions.Def_GaloisRep_Adic

open IsLocalRing

def TateModule (p : ℕ) (M : Type) [AddCommGroup M] : AddSubgroup (ℕ → M) where
  carrier := {x | ∀ n, ((p ^ n : ℕ) : ℤ) • x n = 0 ∧ ((p : ℕ) : ℤ) • x (n + 1) = x n}
  add_mem' := fun {x y} hx hy n =>
    ⟨by rw [Pi.add_apply, smul_add, (hx n).1, (hy n).1, add_zero],
     by rw [Pi.add_apply, Pi.add_apply, smul_add, (hx n).2, (hy n).2]⟩
  zero_mem' := fun n => ⟨smul_zero _, by rw [Pi.zero_apply, Pi.zero_apply, smul_zero]⟩
  neg_mem' := fun {x} hx n =>
    ⟨by rw [Pi.neg_apply, smul_neg, (hx n).1, neg_zero],
     by rw [Pi.neg_apply, Pi.neg_apply, smul_neg, (hx n).2]⟩

namespace TateModule

variable {p : ℕ} {M : Type} [AddCommGroup M]

theorem torsion (x : TateModule p M) (n : ℕ) : ((p ^ n : ℕ) : ℤ) • (x : ℕ → M) n = 0 := (x.2 n).1

theorem compat (x : TateModule p M) (n : ℕ) : ((p : ℕ) : ℤ) • (x : ℕ → M) (n + 1) = (x : ℕ → M) n :=
  (x.2 n).2

theorem compat_pow (x : TateModule p M) (n k : ℕ) :
    ((p ^ k : ℕ) : ℤ) • (x : ℕ → M) (n + k) = (x : ℕ → M) n := by
  induction k with
  | zero => rw [pow_zero, Nat.cast_one, one_smul, Nat.add_zero]
  | succ k ih =>
    rw [pow_succ, Nat.cast_mul, mul_smul]
    show ((p ^ k : ℕ) : ℤ) • (((p : ℕ) : ℤ) • (x : ℕ → M) ((n + k) + 1)) = _
    rw [compat, ih]

@[simp] theorem coe_add (x y : TateModule p M) : ((x + y : TateModule p M) : ℕ → M) = x + y := rfl
@[simp] theorem coe_zero : ((0 : TateModule p M) : ℕ → M) = 0 := rfl
@[simp] theorem coe_neg (x : TateModule p M) : ((-x : TateModule p M) : ℕ → M) = -x := rfl
@[simp] theorem coe_sub (x y : TateModule p M) : ((x - y : TateModule p M) : ℕ → M) = x - y := rfl

theorem apply_zero (x : TateModule p M) : (x : ℕ → M) 0 = 0 := by
  have h := torsion x 0
  rwa [pow_zero, Nat.cast_one, one_smul] at h

theorem natCast_smul_eq_mod {n c : ℕ} {m : M} (hm : ((p ^ n : ℕ) : ℤ) • m = 0) :
    (c : ℤ) • m = ((c % p ^ n : ℕ) : ℤ) • m := by
  conv_lhs => rw [← Nat.div_add_mod c (p ^ n)]
  rw [Nat.cast_add, add_smul, Nat.cast_mul, mul_comm, mul_smul, hm, smul_zero, zero_add]

theorem natCast_smul_eq_of_zmod_eq {n c d : ℕ} {m : M} (hm : ((p ^ n : ℕ) : ℤ) • m = 0)
    (h : (c : ZMod (p ^ n)) = d) : (c : ℤ) • m = (d : ℤ) • m := by
  rw [natCast_smul_eq_mod hm, natCast_smul_eq_mod (c := d) hm, (ZMod.natCast_eq_natCast_iff' c d _).1 h]

variable [Fact p.Prime]

theorem toZModPow_eq_appr (n : ℕ) (a : ℤ_[p]) : PadicInt.toZModPow n a = (a.appr n : ZMod (p ^ n)) := rfl

theorem appr_succ_smul_eq (a : ℤ_[p]) (x : TateModule p M) (n : ℕ) :
    ((a.appr (n + 1) : ℕ) : ℤ) • (x : ℕ → M) n = ((a.appr n : ℕ) : ℤ) • (x : ℕ → M) n := by
  refine natCast_smul_eq_of_zmod_eq (torsion x n) ?_
  rw [← toZModPow_eq_appr, ← PadicInt.zmod_cast_comp_toZModPow n (n + 1) n.le_succ, RingHom.comp_apply,
    toZModPow_eq_appr, ZMod.castHom_apply, ZMod.cast_natCast (pow_dvd_pow p n.le_succ)]

noncomputable instance instSMul : SMul ℤ_[p] (TateModule p M) :=
  ⟨fun a x => ⟨fun n => ((a.appr n : ℕ) : ℤ) • (x : ℕ → M) n, fun n =>
    ⟨by rw [smul_comm, torsion, smul_zero], by rw [smul_comm, compat, appr_succ_smul_eq]⟩⟩⟩

@[simp] theorem smul_apply (a : ℤ_[p]) (x : TateModule p M) (n : ℕ) :
    ((a • x : TateModule p M) : ℕ → M) n = ((a.appr n : ℕ) : ℤ) • (x : ℕ → M) n := rfl

noncomputable instance instModule : Module ℤ_[p] (TateModule p M) where
  one_smul x := by
    refine Subtype.ext (funext fun n => ?_)
    rw [smul_apply]
    have h : (((1 : ℤ_[p]).appr n : ℕ) : ZMod (p ^ n)) = ((1 : ℕ) : ZMod (p ^ n)) := by
      rw [← toZModPow_eq_appr, map_one, Nat.cast_one]
    rw [natCast_smul_eq_of_zmod_eq (torsion x n) h, Nat.cast_one, one_smul]
  mul_smul a b x := by
    refine Subtype.ext (funext fun n => ?_)
    rw [smul_apply, smul_apply, smul_apply, smul_smul, ← Nat.cast_mul]
    refine natCast_smul_eq_of_zmod_eq (torsion x n) ?_
    rw [← toZModPow_eq_appr, map_mul, toZModPow_eq_appr, toZModPow_eq_appr, Nat.cast_mul]
  smul_zero a := Subtype.ext (funext fun n => by rw [smul_apply, coe_zero, Pi.zero_apply, smul_zero])
  smul_add a x y := Subtype.ext (funext fun n => by
    rw [smul_apply, coe_add, Pi.add_apply, smul_add, coe_add, Pi.add_apply, smul_apply, smul_apply])
  add_smul a b x := by
    refine Subtype.ext (funext fun n => ?_)
    rw [smul_apply, coe_add, Pi.add_apply, smul_apply, smul_apply, ← add_smul, ← Nat.cast_add]
    refine natCast_smul_eq_of_zmod_eq (torsion x n) ?_
    rw [← toZModPow_eq_appr, map_add, toZModPow_eq_appr, toZModPow_eq_appr, Nat.cast_add]
  zero_smul x := by
    refine Subtype.ext (funext fun n => ?_)
    rw [smul_apply, coe_zero, Pi.zero_apply]
    have h : (((0 : ℤ_[p]).appr n : ℕ) : ZMod (p ^ n)) = ((0 : ℕ) : ZMod (p ^ n)) := by
      rw [← toZModPow_eq_appr, map_zero, Nat.cast_zero]
    rw [natCast_smul_eq_of_zmod_eq (torsion x n) h, Nat.cast_zero, zero_smul]

theorem natCast_padicInt_smul_apply (c : ℕ) (x : TateModule p M) (n : ℕ) :
    (((c : ℤ_[p]) • x : TateModule p M) : ℕ → M) n = (c : ℤ) • (x : ℕ → M) n := by
  rw [smul_apply]
  refine natCast_smul_eq_of_zmod_eq (torsion x n) ?_
  rw [← toZModPow_eq_appr, map_natCast]

theorem smul_apply_eq_zero_of_mem_span {n : ℕ} {a : ℤ_[p]}
    (ha : a ∈ Ideal.span {(p : ℤ_[p]) ^ n}) (x : TateModule p M) :
    ((a • x : TateModule p M) : ℕ → M) n = 0 := by
  rw [smul_apply]
  have h : ((a.appr n : ℕ) : ZMod (p ^ n)) = ((0 : ℕ) : ZMod (p ^ n)) := by
    rw [← toZModPow_eq_appr, Nat.cast_zero, ← RingHom.mem_ker, PadicInt.ker_toZModPow]
    exact ha
  rw [natCast_smul_eq_of_zmod_eq (torsion x n) h, Nat.cast_zero, zero_smul]

variable (p M) in

def proj (n : ℕ) : TateModule p M →+ M where
  toFun x := (x : ℕ → M) n
  map_zero' := rfl
  map_add' _ _ := rfl

omit [Fact p.Prime] in
@[simp] theorem proj_apply (n : ℕ) (x : TateModule p M) : proj p M n x = (x : ℕ → M) n := rfl

omit [Fact p.Prime] in
theorem torsionBy_proj (n : ℕ) (x : TateModule p M) : ((p ^ n : ℕ) : ℤ) • proj p M n x = 0 :=
  torsion x n

omit [Fact p.Prime] in
theorem proj_mem_torsionBy (n : ℕ) (x : TateModule p M) :
    proj p M n x ∈ Submodule.torsionBy ℤ M ((p ^ n : ℕ) : ℤ) :=
  (Submodule.mem_torsionBy_iff _ _).2 (torsion x n)

def shiftOfProjEqZero (n : ℕ) (x : TateModule p M) (hx : proj p M n x = 0) : TateModule p M :=
  ⟨fun m => (x : ℕ → M) (m + n), fun m =>
    ⟨by
      show ((p ^ m : ℕ) : ℤ) • (x : ℕ → M) (m + n) = 0
      rw [Nat.add_comm, compat_pow x n m]; exact hx,
     by
      show ((p : ℕ) : ℤ) • (x : ℕ → M) (m + 1 + n) = (x : ℕ → M) (m + n)
      rw [Nat.add_right_comm]; exact compat x (m + n)⟩⟩

theorem pow_smul_shiftOfProjEqZero (n : ℕ) (x : TateModule p M) (hx : proj p M n x = 0) :
    ((p : ℤ_[p]) ^ n) • shiftOfProjEqZero n x hx = x := by
  refine Subtype.ext (funext fun m => ?_)
  rw [← Nat.cast_pow, natCast_padicInt_smul_apply]
  exact compat_pow x m n

theorem proj_eq_zero_iff (n : ℕ) (x : TateModule p M) :
    proj p M n x = 0 ↔ x ∈ (maximalIdeal ℤ_[p] ^ n) • (⊤ : Submodule ℤ_[p] (TateModule p M)) := by
  constructor
  · intro hx
    rw [← pow_smul_shiftOfProjEqZero n x hx]
    refine Submodule.smul_mem_smul ?_ Submodule.mem_top
    rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow]
    exact Ideal.mem_span_singleton_self _
  · intro hx
    rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow] at hx
    refine Submodule.smul_induction_on hx (fun a ha y _ => ?_) (fun y z hy hz => ?_)
    · exact smul_apply_eq_zero_of_mem_span ha y
    · rw [map_add, hy, hz, add_zero]

section action

variable {G : Type} [Monoid G] [DistribMulAction G M]

variable (p M G) in

noncomputable def rep : G →* Module.End ℤ_[p] (TateModule p M) where
  toFun g :=
    { toFun := fun x => ⟨fun n => g • (x : ℕ → M) n, fun n =>
        ⟨by
          show ((p ^ n : ℕ) : ℤ) • DistribSMul.toAddMonoidHom M g ((x : ℕ → M) n) = 0
          rw [← map_zsmul, torsion, map_zero],
         by
          show ((p : ℕ) : ℤ) • DistribSMul.toAddMonoidHom M g ((x : ℕ → M) (n + 1)) = _
          rw [← map_zsmul, compat]; rfl⟩⟩
      map_add' := fun x y => Subtype.ext (funext fun n => by
        show g • ((x + y : TateModule p M) : ℕ → M) n = g • (x : ℕ → M) n + g • (y : ℕ → M) n
        rw [coe_add, Pi.add_apply, smul_add])
      map_smul' := fun a x => Subtype.ext (funext fun n => by
        show g • (((a.appr n : ℕ) : ℤ) • (x : ℕ → M) n) = ((a.appr n : ℕ) : ℤ) • (g • (x : ℕ → M) n)
        exact map_zsmul (DistribSMul.toAddMonoidHom M g) _ _) }
  map_one' := LinearMap.ext fun x => Subtype.ext (funext fun n => one_smul G ((x : ℕ → M) n))
  map_mul' g h := LinearMap.ext fun x => Subtype.ext (funext fun n => mul_smul g h ((x : ℕ → M) n))

@[simp] theorem rep_apply (g : G) (x : TateModule p M) (n : ℕ) :
    ((rep p M G g x : TateModule p M) : ℕ → M) n = g • (x : ℕ → M) n := rfl

theorem rep_sub_mem_of_apply_eq (g : G) (x : TateModule p M) (n : ℕ)
    (h : g • (x : ℕ → M) n = (x : ℕ → M) n) :
    rep p M G g x - x ∈ (maximalIdeal ℤ_[p] ^ n) • (⊤ : Submodule ℤ_[p] (TateModule p M)) := by
  rw [← proj_eq_zero_iff, map_sub, sub_eq_zero]
  exact h

end action

theorem smul_apply_eq_smul [Module ℤ_[p] M] (a : ℤ_[p]) (x : TateModule p M) (n : ℕ) :
    ((a • x : TateModule p M) : ℕ → M) n = a • (x : ℕ → M) n := by
  obtain ⟨c, hc⟩ := Ideal.mem_span_singleton'.1 (PadicInt.appr_spec n a)
  have ha : a = ((a.appr n : ℕ) : ℤ_[p]) + c * (p ^ n : ℕ) := by
    rw [Nat.cast_pow, hc, add_sub_cancel]
  have hkill : ((p ^ n : ℕ) : ℤ_[p]) • (x : ℕ → M) n = 0 := by
    rw [Nat.cast_smul_eq_nsmul, ← natCast_zsmul]
    exact torsion x n
  conv_rhs => rw [ha]
  rw [add_smul, mul_smul, hkill, smul_zero, add_zero, Nat.cast_smul_eq_nsmul, smul_apply,
    natCast_zsmul]

section InstanceRegression

noncomputable example [Module ℤ_[p] M] : SMul ℤ_[p] (TateModule p M) := inferInstance

example [Module ℤ_[p] M] : (inferInstance : SMul ℤ_[p] (TateModule p M)) = instSMul := by
  with_reducible_and_instances rfl

example [Module ℤ_[p] M] : (inferInstance : Module ℤ_[p] (TateModule p M)) = instModule := by
  with_reducible_and_instances rfl

example [Module ℤ_[p] M] :
    (inferInstance : DistribMulAction ℤ_[p] (TateModule p M)).toMulAction.toSMul = instSMul := by
  with_reducible_and_instances rfl

example {G : Type} [Monoid G] [DistribMulAction G M] : True := by
  fail_if_success (have _i : SMul G (TateModule p M) := inferInstance)
  trivial

example [Module ℤ_[p] M] : True := by
  fail_if_success (fail_if_success (have _i : SMul ℤ_[p] (TateModule p M) := inferInstance))
  trivial

end InstanceRegression

end TateModule

namespace GaloisRep

variable (𝒪 : Type) [CommRing 𝒪] [IsLocalRing 𝒪] (p : ℕ) [Fact p.Prime]

omit [Fact p.Prime] in
theorem ringChar_quotient_dvd (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) (n : ℕ) :
    ringChar (𝒪 ⧸ maximalIdeal 𝒪 ^ n) ∣ p ^ n := by
  rw [← ringChar.spec, Nat.cast_pow, ← map_natCast (Ideal.Quotient.mk (maximalIdeal 𝒪 ^ n)), ← map_pow,
    Ideal.Quotient.eq_zero_iff_mem]
  exact Ideal.pow_mem_pow hp n

noncomputable def padicIntToRingLevel (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) (n : ℕ) :
    ℤ_[p] →+* 𝒪 ⧸ maximalIdeal 𝒪 ^ n :=
  (ZMod.castHom (ringChar_quotient_dvd 𝒪 p hp n) (𝒪 ⧸ maximalIdeal 𝒪 ^ n)).comp (PadicInt.toZModPow n)

theorem padicIntToRingLevel_compat (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) {m n : ℕ} (hle : m ≤ n) :
    (Ideal.Quotient.factorPow (maximalIdeal 𝒪) hle).comp (padicIntToRingLevel 𝒪 p hp n) =
      padicIntToRingLevel 𝒪 p hp m := by
  rw [padicIntToRingLevel, padicIntToRingLevel, ← PadicInt.zmod_cast_comp_toZModPow m n hle,
    ← RingHom.comp_assoc, ← RingHom.comp_assoc]
  congr 1
  exact Subsingleton.elim _ _

variable [IsAdicComplete (maximalIdeal 𝒪) 𝒪]

noncomputable def padicIntToRing (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) : ℤ_[p] →+* 𝒪 :=
  IsAdicComplete.liftRingHom (maximalIdeal 𝒪) (padicIntToRingLevel 𝒪 p hp)
    (fun hle => padicIntToRingLevel_compat 𝒪 p hp hle)

theorem isLocalHom_padicIntToRing (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) :
    IsLocalHom (padicIntToRing 𝒪 p hp) := by
  refine ⟨fun a ha => ?_⟩
  by_contra hna
  have hmem : a ∈ maximalIdeal ℤ_[p] := hna
  rw [PadicInt.maximalIdeal_eq_span_p, Ideal.mem_span_singleton] at hmem
  obtain ⟨b, rfl⟩ := hmem
  rw [map_mul, map_natCast] at ha
  exact (IsLocalRing.mem_maximalIdeal _).1 (Ideal.mul_mem_right _ _ hp) ha

end GaloisRep

namespace TateModule

open Submodule

variable {p : ℕ} {M : Type} [AddCommGroup M]

theorem mem_torsionBy_add {n : ℕ} {m : M} (hm : m ∈ torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) (k : ℕ) :
    m ∈ torsionBy ℤ M ((p ^ (n + k) : ℕ) : ℤ) := by
  rw [mem_torsionBy_iff] at hm ⊢
  rw [pow_add, Nat.cast_mul, mul_comm, mul_smul, hm, smul_zero]

theorem smul_mem_torsionBy_of_mem_succ {n : ℕ} {m : M} (hm : m ∈ torsionBy ℤ M ((p ^ (n + 1) : ℕ) : ℤ)) :
    ((p : ℕ) : ℤ) • m ∈ torsionBy ℤ M ((p ^ n : ℕ) : ℤ) := by
  rw [mem_torsionBy_iff] at hm ⊢
  rw [smul_smul, ← Nat.cast_mul, ← pow_succ, hm]

theorem pow_smul_mem_torsionBy {n k : ℕ} {m : M} (hk : k ≤ n) (hm : m ∈ torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) :
    ((p ^ (n - k) : ℕ) : ℤ) • m ∈ torsionBy ℤ M ((p ^ k : ℕ) : ℤ) := by
  rw [mem_torsionBy_iff] at hm ⊢
  rw [smul_smul, ← Nat.cast_mul, ← pow_add, Nat.add_sub_cancel' hk, hm]

theorem mem_torsionBy_one_of_smul_eq_zero {m : M} (hm : ((p : ℕ) : ℤ) • m = 0) :
    m ∈ torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ) := by
  rw [mem_torsionBy_iff, pow_one]; exact hm

theorem smul_eq_zero_of_mem_torsionBy_one {m : M} (hm : m ∈ torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ)) :
    ((p : ℕ) : ℤ) • m = 0 := by
  rw [mem_torsionBy_iff, pow_one] at hm; exact hm

section Counting

variable [Fact p.Prime]

theorem finite_torsionBy (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) (n : ℕ) :
    Finite (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) :=
  Nat.finite_of_card_ne_zero (by
    rw [hcard n]; exact pow_ne_zero _ (pow_ne_zero _ (Fact.out : p.Prime).ne_zero))

variable (p M) in

def mulP (n : ℕ) : torsionBy ℤ M ((p ^ (n + 1) : ℕ) : ℤ) →+ torsionBy ℤ M ((p ^ n : ℕ) : ℤ) where
  toFun m := ⟨((p : ℕ) : ℤ) • (m : M), smul_mem_torsionBy_of_mem_succ m.2⟩
  map_zero' := Subtype.ext (smul_zero _)
  map_add' _ _ := Subtype.ext (smul_add _ _ _)

omit [Fact p.Prime] in
@[simp] theorem coe_mulP (n : ℕ) (m : torsionBy ℤ M ((p ^ (n + 1) : ℕ) : ℤ)) :
    (mulP p M n m : M) = ((p : ℕ) : ℤ) • (m : M) := rfl

variable (p M) in

def kerMulPEquiv (n : ℕ) : (mulP p M n).ker ≃ torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ) where
  toFun m := ⟨(m.1 : M), mem_torsionBy_one_of_smul_eq_zero (by
    have h := m.2; rw [AddMonoidHom.mem_ker] at h; exact congrArg Subtype.val h)⟩
  invFun m := ⟨⟨(m : M), by
      rw [mem_torsionBy_iff, pow_succ, Nat.cast_mul, mul_smul, smul_eq_zero_of_mem_torsionBy_one m.2,
        smul_zero]⟩,
    by rw [AddMonoidHom.mem_ker]; exact Subtype.ext (smul_eq_zero_of_mem_torsionBy_one m.2)⟩
  left_inv m := rfl
  right_inv m := rfl

theorem mulP_surjective (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) (n : ℕ) :
    Function.Surjective (mulP p M n) := by
  haveI := finite_torsionBy hcard (n + 1)
  haveI := finite_torsionBy hcard n
  have hker : Nat.card (mulP p M n).ker = p ^ 2 := by
    rw [Nat.card_congr (kerMulPEquiv p M n), hcard 1, pow_one]
  have h := AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup (mulP p M n).ker
  rw [hcard (n + 1), Nat.card_congr (QuotientAddGroup.quotientKerEquivRange (mulP p M n)).toEquiv, hker] at h
  have hrange : Nat.card (mulP p M n).range = Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) := by
    rw [hcard n]
    refine Nat.eq_of_mul_eq_mul_right (pow_pos (Fact.out : p.Prime).pos 2) ?_
    rw [← h]; ring
  rw [← AddMonoidHom.range_eq_top]
  exact AddSubgroup.eq_top_of_card_eq _ hrange

theorem exists_smul_eq_of_mem_torsionBy
    (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) {n : ℕ} {m : M}
    (hm : m ∈ torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) :
    ∃ m' ∈ torsionBy ℤ M ((p ^ (n + 1) : ℕ) : ℤ), ((p : ℕ) : ℤ) • m' = m := by
  obtain ⟨m', hm'⟩ := mulP_surjective hcard n ⟨m, hm⟩
  exact ⟨m', m'.2, congrArg Subtype.val hm'⟩

noncomputable def liftAux
    (next : (k : ℕ) → torsionBy ℤ M ((p ^ k : ℕ) : ℤ) → torsionBy ℤ M ((p ^ (k + 1) : ℕ) : ℤ))
    (n : ℕ) (m : torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) : (j : ℕ) → torsionBy ℤ M ((p ^ (n + j) : ℕ) : ℤ)
  | 0 => m
  | j + 1 => next (n + j) (liftAux next n m j)

noncomputable def liftFun
    (next : (k : ℕ) → torsionBy ℤ M ((p ^ k : ℕ) : ℤ) → torsionBy ℤ M ((p ^ (k + 1) : ℕ) : ℤ))
    (n : ℕ) (m : torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) (k : ℕ) : M :=
  if n ≤ k then (liftAux next n m (k - n) : M) else ((p ^ (n - k) : ℕ) : ℤ) • (m : M)

omit [Fact p.Prime] in
theorem liftFun_of_le {next} {n : ℕ} {m : torsionBy ℤ M ((p ^ n : ℕ) : ℤ)} {k : ℕ} (hk : n ≤ k) :
    liftFun next n m k = (liftAux next n m (k - n) : M) := if_pos hk

omit [Fact p.Prime] in
theorem liftFun_of_lt {next} {n : ℕ} {m : torsionBy ℤ M ((p ^ n : ℕ) : ℤ)} {k : ℕ} (hk : k < n) :
    liftFun next n m k = ((p ^ (n - k) : ℕ) : ℤ) • (m : M) := if_neg (not_le.mpr hk)

omit [Fact p.Prime] in
theorem coe_liftAux_congr {next} {n : ℕ} {m : torsionBy ℤ M ((p ^ n : ℕ) : ℤ)} {j j' : ℕ} (h : j = j') :
    (liftAux next n m j : M) = (liftAux next n m j' : M) := by subst h; rfl

omit [Fact p.Prime] in
theorem pow_smul_coe_liftAux {next} {n : ℕ} {m : torsionBy ℤ M ((p ^ n : ℕ) : ℤ)} (j : ℕ) {e : ℕ}
    (he : e = n + j) : ((p ^ e : ℕ) : ℤ) • (liftAux next n m j : M) = 0 := by
  subst he; exact (mem_torsionBy_iff _ _).mp (liftAux next n m j).2

omit [Fact p.Prime] in

theorem liftFun_mem
    {next : (k : ℕ) → torsionBy ℤ M ((p ^ k : ℕ) : ℤ) → torsionBy ℤ M ((p ^ (k + 1) : ℕ) : ℤ)}
    (hnext : ∀ k (m : torsionBy ℤ M ((p ^ k : ℕ) : ℤ)), ((p : ℕ) : ℤ) • (next k m : M) = m)
    (n : ℕ) (m : torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) : liftFun next n m ∈ TateModule p M := by
  intro k
  constructor
  ·
    by_cases hk : n ≤ k
    · rw [liftFun_of_le hk]
      exact pow_smul_coe_liftAux (k - n) (by omega)
    · rw [liftFun_of_lt (not_le.mp hk)]
      exact (mem_torsionBy_iff _ _).mp (pow_smul_mem_torsionBy (not_le.mp hk).le m.2)
  ·
    by_cases hk : n ≤ k
    · rw [liftFun_of_le hk, liftFun_of_le (by omega : n ≤ k + 1),
        coe_liftAux_congr (by omega : k + 1 - n = (k - n) + 1)]
      exact hnext _ _
    · by_cases hk' : n ≤ k + 1
      · have hn : n = k + 1 := by omega
        subst hn
        rw [liftFun_of_le le_rfl, liftFun_of_lt (by omega : k < k + 1), coe_liftAux_congr (Nat.sub_self _),
          Nat.add_sub_cancel_left, pow_one]
        rfl
      · rw [liftFun_of_lt (not_le.mp hk'), liftFun_of_lt (not_le.mp hk), smul_smul, ← Nat.cast_mul,
          ← pow_succ', show n - (k + 1) + 1 = n - k by omega]

theorem proj_surjective (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) (n : ℕ) :
    ∀ m ∈ torsionBy ℤ M ((p ^ n : ℕ) : ℤ), ∃ x : TateModule p M, proj p M n x = m := by
  intro m hm
  choose next hnext using fun k (m : torsionBy ℤ M ((p ^ k : ℕ) : ℤ)) => mulP_surjective hcard k m
  refine ⟨⟨liftFun next n ⟨m, hm⟩, liftFun_mem (fun k m => congrArg Subtype.val (hnext k m)) n ⟨m, hm⟩⟩, ?_⟩
  rw [proj_apply]
  change liftFun next n ⟨m, hm⟩ n = m
  rw [liftFun_of_le le_rfl, coe_liftAux_congr (Nat.sub_self n)]
  rfl

theorem range_proj (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) (n : ℕ) :
    Set.range (proj p M n) = torsionBy ℤ M ((p ^ n : ℕ) : ℤ) := by
  ext m
  exact ⟨fun ⟨x, hx⟩ => hx ▸ proj_mem_torsionBy n x, fun hm => proj_surjective hcard n m hm⟩

end Counting

section Free

variable [Fact p.Prime]

theorem exists_pair_of_card_eq_sq {V : Type} [AddCommGroup V] [Module (ZMod p) V] [Finite V]
    (hV : Nat.card V = p ^ 2) :
    ∃ v w : V, ∀ a b : ℤ, a • v + b • w = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b := by
  have hp : p.Prime := Fact.out
  have hrank : Module.finrank (ZMod p) V = 2 := by
    have h := Module.natCard_eq_pow_finrank (K := ZMod p) (V := V)
    rw [hV, Nat.card_zmod] at h
    exact (Nat.pow_right_injective hp.two_le h).symm
  let b := Module.finBasisOfFinrankEq (ZMod p) V hrank
  refine ⟨b 0, b 1, fun a c h => ?_⟩
  rw [← Int.cast_smul_eq_zsmul (ZMod p) a, ← Int.cast_smul_eq_zsmul (ZMod p) c] at h
  have hli := (Fintype.linearIndependent_iff.mp b.linearIndependent) ![(a : ZMod p), (c : ZMod p)]
    (by rw [Fin.sum_univ_two]; exact h)
  exact ⟨(ZMod.intCast_zmod_eq_zero_iff_dvd a p).mp (hli 0), (ZMod.intCast_zmod_eq_zero_iff_dvd c p).mp (hli 1)⟩

theorem exists_indep_pair_torsionBy_one
    (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    ∃ e₁ ∈ torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ), ∃ e₂ ∈ torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ),
      ∀ a b : ℤ, a • e₁ + b • e₂ = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b := by
  haveI := finite_torsionBy hcard 1
  have hmod : ∀ m : torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ), p • m = 0 := fun m =>
    Subtype.ext (by
      rw [coe_smul_of_tower, ← Nat.cast_smul_eq_nsmul ℤ, Submodule.coe_zero]
      exact smul_eq_zero_of_mem_torsionBy_one m.2)
  letI : Module (ZMod p) (torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ)) := AddCommGroup.zmodModule hmod
  have h1 : Nat.card (torsionBy ℤ M ((p ^ 1 : ℕ) : ℤ)) = p ^ 2 := by rw [hcard 1, pow_one]
  obtain ⟨v, w, h⟩ := exists_pair_of_card_eq_sq (p := p) h1
  refine ⟨v, v.2, w, w.2, fun a b hab => h a b (Subtype.ext ?_)⟩
  rw [Submodule.coe_add, coe_smul_of_tower, coe_smul_of_tower, Submodule.coe_zero]
  exact hab

omit [Fact p.Prime] in

theorem dvd_of_rel_apply {x y : TateModule p M}
    (h1 : ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b) :
    ∀ (n : ℕ) (a b : ℤ), a • (x : ℕ → M) n + b • (y : ℕ → M) n = 0 →
      ((p ^ n : ℕ) : ℤ) ∣ a ∧ ((p ^ n : ℕ) : ℤ) ∣ b := by
  intro n
  induction n with
  | zero => intro a b _; simp
  | succ n ih =>
    intro a b hab

    have hab1 : a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 := by
      have := congrArg (((p ^ n : ℕ) : ℤ) • ·) hab
      simpa only [smul_add, smul_zero, smul_comm _ a, smul_comm _ b, Nat.add_comm n 1 ▸ compat_pow x 1 n,
        Nat.add_comm n 1 ▸ compat_pow y 1 n] using this
    obtain ⟨⟨a', rfl⟩, ⟨b', rfl⟩⟩ := h1 a b hab1

    have hab' : a' • (x : ℕ → M) n + b' • (y : ℕ → M) n = 0 := by
      rw [mul_comm, mul_smul, mul_comm, mul_smul, compat, compat] at hab
      exact hab
    obtain ⟨ha, hb⟩ := ih a' b' hab'
    rw [pow_succ', Nat.cast_mul]
    exact ⟨mul_dvd_mul_left _ ha, mul_dvd_mul_left _ hb⟩

noncomputable def levelMap (x y : TateModule p M) (n : ℕ) (c : ZMod (p ^ n) × ZMod (p ^ n)) :
    torsionBy ℤ M ((p ^ n : ℕ) : ℤ) :=
  ⟨(c.1.val : ℤ) • (x : ℕ → M) n + (c.2.val : ℤ) • (y : ℕ → M) n, by
    rw [mem_torsionBy_iff, smul_add, smul_comm _ (c.1.val : ℤ), torsion, smul_comm _ (c.2.val : ℤ), torsion,
      smul_zero, smul_zero, add_zero]⟩

theorem levelMap_injective {x y : TateModule p M}
    (h1 : ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b) (n : ℕ) :
    Function.Injective (levelMap x y n) := by
  haveI : NeZero (p ^ n) := ⟨pow_ne_zero _ (Fact.out : p.Prime).ne_zero⟩
  rintro ⟨a, b⟩ ⟨a', b'⟩ h
  have h' : ((a.val : ℤ) - a'.val) • (x : ℕ → M) n + ((b.val : ℤ) - b'.val) • (y : ℕ → M) n = 0 := by
    have := sub_eq_zero.mpr (congrArg Subtype.val h)
    simp only [levelMap] at this
    rw [← this, sub_smul, sub_smul]
    abel
  obtain ⟨ha, hb⟩ := dvd_of_rel_apply h1 n _ _ h'
  have key : ∀ {u v : ZMod (p ^ n)}, ((p ^ n : ℕ) : ℤ) ∣ (u.val : ℤ) - v.val → u = v := fun {u v} huv => by
    have := (ZMod.intCast_eq_intCast_iff_dvd_sub (v.val : ℤ) (u.val : ℤ) (p ^ n)).mpr huv
    rwa [Int.cast_natCast, Int.cast_natCast, ZMod.natCast_zmod_val, ZMod.natCast_zmod_val, eq_comm] at this
  exact Prod.ext (key ha) (key hb)

theorem levelMap_bijective (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2)
    {x y : TateModule p M}
    (h1 : ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b) (n : ℕ) :
    Function.Bijective (levelMap x y n) := by
  haveI := finite_torsionBy hcard n
  refine (levelMap_injective h1 n).bijective_of_nat_card_le ?_
  rw [hcard n, Nat.card_prod, Nat.card_zmod, sq]

theorem exists_eq_levelMap (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2)
    {x y : TateModule p M}
    (h1 : ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b) (n : ℕ)
    {m : M} (hm : m ∈ torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) :
    ∃ a b : ℕ, (a : ℤ) • (x : ℕ → M) n + (b : ℤ) • (y : ℕ → M) n = m := by
  obtain ⟨⟨a, b⟩, h⟩ := (levelMap_bijective hcard h1 n).2 ⟨m, hm⟩
  exact ⟨a.val, b.val, congrArg Subtype.val h⟩

theorem linearIndependent_pair {x y : TateModule p M}
    (h1 : ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b) :
    LinearIndependent ℤ_[p] ![x, y] := by
  rw [LinearIndependent.pair_iff]
  intro s t hst
  have hlev : ∀ n, ((p ^ n : ℕ) : ℤ) ∣ (s.appr n : ℤ) ∧ ((p ^ n : ℕ) : ℤ) ∣ (t.appr n : ℤ) := fun n =>
    dvd_of_rel_apply h1 n _ _ (by
      have := congrArg (fun z : TateModule p M => (z : ℕ → M) n) hst
      simpa only [coe_add, Pi.add_apply, smul_apply, coe_zero, Pi.zero_apply] using this)
  have key : ∀ {u : ℤ_[p]}, (∀ n, ((p ^ n : ℕ) : ℤ) ∣ (u.appr n : ℤ)) → u = 0 := fun {u} hu =>
    PadicInt.ext_of_toZModPow.mp fun n => by
      rw [map_zero, toZModPow_eq_appr, ZMod.natCast_eq_zero_iff]
      exact Int.natCast_dvd_natCast.mp (hu n)
  exact ⟨key fun n => (hlev n).1, key fun n => (hlev n).2⟩

theorem mem_span_pair (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2)
    {x y : TateModule p M}
    (h1 : ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b)
    (z : TateModule p M) : ∃ s t : ℤ_[p], s • x + t • y = z := by
  choose a b hab using fun n => exists_eq_levelMap hcard h1 n (proj_mem_torsionBy n z)

  have hcompat : ∀ n, ((p ^ n : ℕ) : ℤ) ∣ (a (n + 1) : ℤ) - a n ∧ ((p ^ n : ℕ) : ℤ) ∣ (b (n + 1) : ℤ) - b n :=
    fun n => dvd_of_rel_apply h1 n _ _ (by
      rw [sub_smul, sub_smul, sub_add_sub_comm, hab n, sub_eq_zero, proj_apply, ← compat z n,
        ← proj_apply (n + 1) z, ← hab (n + 1), smul_add, smul_comm _ (a (n + 1) : ℤ),
        smul_comm _ (b (n + 1) : ℤ), compat, compat])
  have hca : ∀ i, (p : ℤ) ^ i ∣ (fun i => (a i : ℤ)) (i + 1) - (fun i => (a i : ℤ)) i := fun i => by
    rw [← Nat.cast_pow]; exact (hcompat i).1
  have hcb : ∀ i, (p : ℤ) ^ i ∣ (fun i => (b i : ℤ)) (i + 1) - (fun i => (b i : ℤ)) i := fun i => by
    rw [← Nat.cast_pow]; exact (hcompat i).2
  refine ⟨PadicInt.ofIntSeq (fun i => (a i : ℤ)) (PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub _ p hca),
    PadicInt.ofIntSeq (fun i => (b i : ℤ)) (PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub _ p hcb),
    Subtype.ext (funext fun n => ?_)⟩
  rw [coe_add, Pi.add_apply, smul_apply, smul_apply, ← proj_apply n z, ← hab n]
  congr 1
  · refine natCast_smul_eq_of_zmod_eq (torsion x n) ?_
    rw [← toZModPow_eq_appr, PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub (fun i => (a i : ℤ)) p hca n,
      Int.cast_natCast]
  · refine natCast_smul_eq_of_zmod_eq (torsion y n) ?_
    rw [← toZModPow_eq_appr, PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub (fun i => (b i : ℤ)) p hcb n,
      Int.cast_natCast]

theorem exists_pair (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    ∃ x y : TateModule p M,
      ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b := by
  obtain ⟨e₁, he₁, e₂, he₂, h1⟩ := exists_indep_pair_torsionBy_one hcard
  obtain ⟨x, hx⟩ := proj_surjective hcard 1 e₁ he₁
  obtain ⟨y, hy⟩ := proj_surjective hcard 1 e₂ he₂
  rw [proj_apply] at hx hy
  exact ⟨x, y, by rw [hx, hy]; exact h1⟩

theorem top_le_span_pair (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2)
    {x y : TateModule p M}
    (h1 : ∀ a b : ℤ, a • (x : ℕ → M) 1 + b • (y : ℕ → M) 1 = 0 → (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b) :
    ⊤ ≤ span ℤ_[p] (Set.range ![x, y]) := by
  intro z _
  obtain ⟨s, t, hst⟩ := mem_span_pair hcard h1 z
  rw [Matrix.range_cons_cons_empty, Submodule.mem_span_pair]
  exact ⟨s, t, hst⟩

noncomputable def basisOfCard (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    Module.Basis (Fin 2) ℤ_[p] (TateModule p M) :=
  Module.Basis.mk (v := ![(exists_pair hcard).choose, (exists_pair hcard).choose_spec.choose])
    (linearIndependent_pair (exists_pair hcard).choose_spec.choose_spec)
    (top_le_span_pair hcard (exists_pair hcard).choose_spec.choose_spec)

theorem basisOfCard_rel_one (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2)
    (a b : ℤ) (h : a • ((basisOfCard hcard 0 : TateModule p M) : ℕ → M) 1 +
      b • ((basisOfCard hcard 1 : TateModule p M) : ℕ → M) 1 = 0) : (p : ℤ) ∣ a ∧ (p : ℤ) ∣ b := by
  rw [basisOfCard, Module.Basis.coe_mk] at h
  exact (exists_pair hcard).choose_spec.choose_spec a b h

theorem dvd_of_rel_basisOfCard_apply
    (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) (n : ℕ) (a b : ℤ)
    (h : a • ((basisOfCard hcard 0 : TateModule p M) : ℕ → M) n +
      b • ((basisOfCard hcard 1 : TateModule p M) : ℕ → M) n = 0) :
    ((p ^ n : ℕ) : ℤ) ∣ a ∧ ((p ^ n : ℕ) : ℤ) ∣ b :=
  dvd_of_rel_apply (basisOfCard_rel_one hcard) n a b h

theorem exists_eq_smul_basisOfCard_apply
    (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) (n : ℕ) {m : M}
    (hm : m ∈ torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) :
    ∃ a b : ℕ, (a : ℤ) • ((basisOfCard hcard 0 : TateModule p M) : ℕ → M) n +
      (b : ℤ) • ((basisOfCard hcard 1 : TateModule p M) : ℕ → M) n = m :=
  exists_eq_levelMap hcard (basisOfCard_rel_one hcard) n hm

theorem free (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    Module.Free ℤ_[p] (TateModule p M) :=
  Module.Free.of_basis (basisOfCard hcard)

theorem finite (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    Module.Finite ℤ_[p] (TateModule p M) :=
  Module.Finite.of_basis (basisOfCard hcard)

theorem finrank_eq_two (hcard : ∀ n : ℕ, Nat.card (torsionBy ℤ M ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    Module.finrank ℤ_[p] (TateModule p M) = 2 := by
  rw [Module.finrank_eq_card_basis (basisOfCard hcard), Fintype.card_fin]

end Free

end TateModule

namespace TateModule

variable {p : ℕ} {M : Type} [AddCommGroup M] [Fact p.Prime]

section action

variable {G : Type} [Monoid G] [DistribMulAction G M]

theorem rep_sub_mem_of_forall_torsionBy (g : G) (n : ℕ)
    (h : ∀ m ∈ Submodule.torsionBy ℤ M ((p ^ n : ℕ) : ℤ), g • m = m) (x : TateModule p M) :
    rep p M G g x - x ∈ (maximalIdeal ℤ_[p] ^ n) • (⊤ : Submodule ℤ_[p] (TateModule p M)) :=
  rep_sub_mem_of_apply_eq g x n (h _ (proj_mem_torsionBy n x))

theorem rep_eq_one_of_forall_torsionBy (g : G)
    (h : ∀ n : ℕ, ∀ m ∈ Submodule.torsionBy ℤ M ((p ^ n : ℕ) : ℤ), g • m = m) :
    rep p M G g = 1 := by
  refine LinearMap.ext fun x => Subtype.ext (funext fun n => ?_)
  rw [rep_apply, Module.End.one_apply]
  exact h n _ (proj_mem_torsionBy n x)

end action

end TateModule

namespace WeierstrassCurve

open WeierstrassCurve.Affine WeierstrassCurve.Affine.Point

def Affine.Point.coords {F : Type} [Field F] {W : WeierstrassCurve F} : W.toAffine.Point → Set F
  | 0 => ∅
  | @Affine.Point.some _ _ _ x y _ => {x, y}

theorem Affine.Point.coords_finite {F : Type} [Field F] {W : WeierstrassCurve F}
    (P : W.toAffine.Point) : P.coords.Finite := by
  rcases P with _ | ⟨x, y, h⟩
  · exact Set.finite_empty
  · exact (Set.finite_singleton y).insert x

theorem Affine.Point.algEquiv_smul_eq_self_of_forall_coords {F S : Type} [Field F] [CommRing S]
    [Algebra S F] [DecidableEq F] {W : WeierstrassCurve S} (σ : F ≃ₐ[S] F)
    (P : (W.toAffine⁄F).Point) (h : ∀ z ∈ Affine.Point.coords (W := W.baseChange F) P, σ z = z) :
    σ • P = P := by
  rcases P with _ | ⟨x, y, hP⟩
  · rfl
  · have hx : σ x = x := h x (Set.mem_insert x {y})
    have hy : σ y = y := h y (Set.mem_insert_of_mem x (Set.mem_singleton y))
    rw [algEquiv_smul_def, map_some, Affine.Point.some.injEq]
    exact ⟨hx, hy⟩

variable (W : WeierstrassCurve ℚ) (p : ℕ) [Fact p.Prime]

noncomputable def torsionField (n : ℕ) : IntermediateField ℚ (AlgebraicClosure ℚ) :=
  IntermediateField.adjoin ℚ
    (⋃ P ∈ (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ) :
        Set (W⁄(AlgebraicClosure ℚ)).Point),
      Affine.Point.coords (W := W.baseChange (AlgebraicClosure ℚ)) P)

omit [Fact p.Prime] in
theorem coords_subset_torsionField (n : ℕ) {P : (W⁄(AlgebraicClosure ℚ)).Point}
    (hP : P ∈ Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) :
    Affine.Point.coords (W := W.baseChange (AlgebraicClosure ℚ)) P ⊆ (W.torsionField p n : Set _) :=
  fun _ hz => IntermediateField.subset_adjoin ℚ _ (Set.mem_biUnion hP hz)

omit [Fact p.Prime] in

theorem finiteDimensional_torsionField (n : ℕ)
    (hfin : Finite (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ))) :
    FiniteDimensional ℚ (W.torsionField p n) := by
  have hS : (⋃ P ∈ (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ) :
        Set (W⁄(AlgebraicClosure ℚ)).Point),
      Affine.Point.coords (W := W.baseChange (AlgebraicClosure ℚ)) P).Finite :=
    Set.Finite.biUnion (Set.finite_coe_iff.mp hfin) fun P _ => Affine.Point.coords_finite P
  haveI := hS.to_subtype

  exact IntermediateField.finiteDimensional_adjoin fun z _ => by
    convert ((AlgebraicClosure.isAlgebraic ℚ).isAlgebraic z).isIntegral
    exact Subsingleton.elim _ _

omit [Fact p.Prime] in

theorem algEquiv_smul_eq_self_of_mem_torsionBy (n : ℕ) (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
    (hσ : ∀ z ∈ W.torsionField p n, σ z = z) {P : (W⁄(AlgebraicClosure ℚ)).Point}
    (hP : P ∈ Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) :
    σ • P = P :=
  Affine.Point.algEquiv_smul_eq_self_of_forall_coords σ P
    fun z hz => hσ z (W.coords_subset_torsionField p n hP hz)

theorem tateModule_isAdicContinuous
    (hfin : ∀ n : ℕ, Finite (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ))) :
    GaloisActionIsAdicContinuous ℤ_[p]
      (TateModule.rep p (W⁄(AlgebraicClosure ℚ)).Point (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)) :=
  fun n => ⟨W.torsionField p n, W.finiteDimensional_torsionField p n (hfin n), fun σ hσ x =>
    TateModule.rep_sub_mem_of_forall_torsionBy σ n
      (fun _ hP => W.algEquiv_smul_eq_self_of_mem_torsionBy p n σ hσ hP) x⟩

omit [Fact p.Prime] in
theorem finite_torsionBy_of_card (n : ℕ)
    (hcard : Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ))
      = (p ^ n) ^ 2) (hp : p ≠ 0) :
    Finite (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) :=
  Nat.finite_of_card_ne_zero (by rw [hcard]; exact pow_ne_zero 2 (pow_ne_zero n hp))

noncomputable def tateModuleRepOfBasis
    (hcard : ∀ n : ℕ, Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ))
      = (p ^ n) ^ 2)
    (b : Module.Basis (Fin 2) ℤ_[p] (TateModule p (W⁄(AlgebraicClosure ℚ)).Point)) :
    GaloisRepAdic ℤ_[p] where
  V := TateModule p (W⁄(AlgebraicClosure ℚ)).Point
  instFree := Module.Free.of_basis b
  instFinite := Module.Finite.of_basis b
  finrank_eq := by rw [Module.finrank_eq_card_basis b, Fintype.card_fin]
  ρ := TateModule.rep p (W⁄(AlgebraicClosure ℚ)).Point (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)
  isAdicContinuous := W.tateModule_isAdicContinuous p
    fun n => W.finite_torsionBy_of_card p n (hcard n) (Nat.Prime.ne_zero Fact.out)

@[simp] theorem tateModuleRepOfBasis_V
    (hcard : ∀ n : ℕ, Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ))
      = (p ^ n) ^ 2)
    (b : Module.Basis (Fin 2) ℤ_[p] (TateModule p (W⁄(AlgebraicClosure ℚ)).Point)) :
    (W.tateModuleRepOfBasis p hcard b).V = TateModule p (W⁄(AlgebraicClosure ℚ)).Point := rfl

theorem tateModuleRepOfBasis_ρ
    (hcard : ∀ n : ℕ, Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ))
      = (p ^ n) ^ 2)
    (b : Module.Basis (Fin 2) ℤ_[p] (TateModule p (W⁄(AlgebraicClosure ℚ)).Point)) :
    (W.tateModuleRepOfBasis p hcard b).ρ
      = TateModule.rep p (W⁄(AlgebraicClosure ℚ)).Point (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) :=
  rfl

@[simp] theorem tateModuleRepOfBasis_ρ_apply
    (hcard : ∀ n : ℕ, Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ))
      = (p ^ n) ^ 2)
    (b : Module.Basis (Fin 2) ℤ_[p] (TateModule p (W⁄(AlgebraicClosure ℚ)).Point))
    (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : TateModule p (W⁄(AlgebraicClosure ℚ)).Point)
    (n : ℕ) :
    ((show TateModule p (W⁄(AlgebraicClosure ℚ)).Point from (W.tateModuleRepOfBasis p hcard b).ρ σ x) :
        ℕ → (W⁄(AlgebraicClosure ℚ)).Point) n
      = σ • (x : ℕ → (W⁄(AlgebraicClosure ℚ)).Point) n := rfl

end WeierstrassCurve

namespace GaloisRep

variable (𝒪 : Type) [CommRing 𝒪] [IsLocalRing 𝒪] (p : ℕ) [Fact p.Prime]

@[simp] theorem padicIntToRingLevel_apply (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) (n : ℕ) (a : ℤ_[p]) :
    padicIntToRingLevel 𝒪 p hp n a = ZMod.cast (PadicInt.toZModPow n a) := rfl

theorem padicIntToRingLevel_natCast (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) (n c : ℕ) :
    padicIntToRingLevel 𝒪 p hp n c = c :=
  map_natCast _ c

variable [IsAdicComplete (maximalIdeal 𝒪) 𝒪]

theorem mk_comp_padicIntToRing (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) (n : ℕ) :
    (Ideal.Quotient.mk (maximalIdeal 𝒪 ^ n)).comp (padicIntToRing 𝒪 p hp) =
      padicIntToRingLevel 𝒪 p hp n :=
  IsAdicComplete.mk_comp_liftRingHom (maximalIdeal 𝒪) _ _ n

theorem mk_padicIntToRing (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) (n : ℕ) (a : ℤ_[p]) :
    Ideal.Quotient.mk (maximalIdeal 𝒪 ^ n) (padicIntToRing 𝒪 p hp a) =
      padicIntToRingLevel 𝒪 p hp n a :=
  IsAdicComplete.mk_liftRingHom (maximalIdeal 𝒪) _ _ n a

theorem eq_padicIntToRing (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) {φ : ℤ_[p] →+* 𝒪}
    (hφ : ∀ n, (Ideal.Quotient.mk (maximalIdeal 𝒪 ^ n)).comp φ = padicIntToRingLevel 𝒪 p hp n) :
    φ = padicIntToRing 𝒪 p hp :=
  IsAdicComplete.eq_liftRingHom (maximalIdeal 𝒪) _ _ φ hφ

omit [IsAdicComplete (maximalIdeal 𝒪) 𝒪] in

theorem mk_comp_eq_padicIntToRingLevel_iff (hp : (p : 𝒪) ∈ maximalIdeal 𝒪) (φ : ℤ_[p] →+* 𝒪) (n : ℕ) :
    (Ideal.Quotient.mk (maximalIdeal 𝒪 ^ n)).comp φ = padicIntToRingLevel 𝒪 p hp n ↔
      ∀ a : ℤ_[p], φ a - (a.appr n : 𝒪) ∈ maximalIdeal 𝒪 ^ n := by
  constructor
  · intro h a
    have ha := RingHom.congr_fun h a
    rw [RingHom.comp_apply, padicIntToRingLevel_apply, TateModule.toZModPow_eq_appr,
      ZMod.cast_natCast (ringChar_quotient_dvd 𝒪 p hp n), ← map_natCast (Ideal.Quotient.mk _),
      Ideal.Quotient.eq] at ha
    exact ha
  · intro h
    refine RingHom.ext fun a => ?_
    rw [RingHom.comp_apply, padicIntToRingLevel_apply, TateModule.toZModPow_eq_appr,
      ZMod.cast_natCast (ringChar_quotient_dvd 𝒪 p hp n), ← map_natCast (Ideal.Quotient.mk _),
      Ideal.Quotient.eq]
    exact h a

end GaloisRep

namespace PadicInt

variable (p : ℕ) [Fact p.Prime]

theorem natCast_mem_maximalIdeal : (p : ℤ_[p]) ∈ maximalIdeal ℤ_[p] := by
  rw [maximalIdeal_eq_span_p]
  exact Ideal.mem_span_singleton_self _

theorem padicIntToRing_self :
    GaloisRep.padicIntToRing ℤ_[p] p (natCast_mem_maximalIdeal p) = RingHom.id ℤ_[p] := by
  symm
  refine GaloisRep.eq_padicIntToRing ℤ_[p] p (natCast_mem_maximalIdeal p) fun n => ?_
  rw [GaloisRep.mk_comp_eq_padicIntToRingLevel_iff]
  intro a
  rw [RingHom.id_apply, maximalIdeal_eq_span_p, Ideal.span_singleton_pow]
  exact appr_spec n a

end PadicInt

namespace WeierstrassCurve

open WeierstrassCurve.Affine WeierstrassCurve.Affine.Point

noncomputable def tateModuleRep (W : WeierstrassCurve ℚ) (p : ℕ) [Fact p.Prime]
    (hcard : ∀ n : ℕ,
      Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    GaloisRepAdic ℤ_[p] :=
  W.tateModuleRepOfBasis p hcard (TateModule.basisOfCard hcard)

@[simp] theorem tateModuleRep_V (W : WeierstrassCurve ℚ) (p : ℕ) [Fact p.Prime]
    (hcard : ∀ n : ℕ,
      Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    (W.tateModuleRep p hcard).V = TateModule p (W⁄(AlgebraicClosure ℚ)).Point := rfl

theorem tateModuleRep_ρ (W : WeierstrassCurve ℚ) (p : ℕ) [Fact p.Prime]
    (hcard : ∀ n : ℕ,
      Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2) :
    (W.tateModuleRep p hcard).ρ
      = TateModule.rep p (W⁄(AlgebraicClosure ℚ)).Point (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) :=
  rfl

@[simp] theorem tateModuleRep_ρ_apply (W : WeierstrassCurve ℚ) (p : ℕ) [Fact p.Prime]
    (hcard : ∀ n : ℕ,
      Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2)
    (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : TateModule p (W⁄(AlgebraicClosure ℚ)).Point)
    (n : ℕ) :
    ((show TateModule p (W⁄(AlgebraicClosure ℚ)).Point from (W.tateModuleRep p hcard).ρ σ x) : ℕ → _) n
      = σ • (x : ℕ → (W⁄(AlgebraicClosure ℚ)).Point) n := rfl

theorem tateModuleRepOfBasis_eq_tateModuleRep (W : WeierstrassCurve ℚ) (p : ℕ) [Fact p.Prime]
    (hcard : ∀ n : ℕ,
      Nat.card (Submodule.torsionBy ℤ (W⁄(AlgebraicClosure ℚ)).Point ((p ^ n : ℕ) : ℤ)) = (p ^ n) ^ 2)
    (b : Module.Basis (Fin 2) ℤ_[p] (TateModule p (W⁄(AlgebraicClosure ℚ)).Point)) :
    W.tateModuleRepOfBasis p hcard b = W.tateModuleRep p hcard := rfl

end WeierstrassCurve