Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_PDivisibleGroup_Points.lean

definition module

Points and Tate module of a -divisible group

Throughout, G is a p-divisible group of height h over a commutative ring R in the project's sense — a family of commutative, cocommutative Hopf R-algebras A_v = G.level v, finite and free over R of rank p^{vh}, together with surjective bialgebra maps A_{v+1}\to A_v whose kernels are the ideals generated by the image of the augmentation ideal under multiplication-by-p^v — and L is a commutative R-algebra.

The Hopf-algebraic preliminaries record that on a commutative Hopf algebra the antipode is an algebra map antipodeAlgHom, that composing an algebra map \varphi\colon H\to A with it produces a two-sided inverse of \varphi for the convolution product, hence that every \varphi is a unit in the convolution monoid, and that precomposition with a bialgebra map H\to K is a monoid homomorphism of convolution monoids (convCompMonoidHom).

PDivisibleGroup.Point G L v is the set \operatorname{Hom}_{R\text{-alg}}(A_v,L) with the convolution product (xy)(a)=\mu((x\otimes y)(\Delta a)), unit a\mapsto \mathrm{algebraMap}(\varepsilon(a)) and inverse given by composition with the antipode; it is a commutative group in which every element satisfies x^{p^v}=1. pointIncl is the map x\mapsto x\circ(A_{v+1}\to A_v); it is injective and its image is exactly the p^v-torsion of the level v+1 points, and pointInclLE iterates it for v\le w. Points G L is the direct limit of the additively written groups along these maps: every element comes from some level, each level maps in injectively, and each element of level v is killed by p^v, so for p>0 the limit is torsion. An R-algebra map L\to L' acts by postcomposition, functorially and injectively when the map is, whence a DistribMulAction of \operatorname{Aut}_{R\text{-alg}}(L) on Points G L. Finally, for p prime, tateModule is the Tate module \{(x_n) : p^nx_n=0,\ px_{n+1}=x_n\} of Points G L and tateModuleRep the resulting representation of \operatorname{Aut}_{R\text{-alg}}(L) by \mathbb{Z}_p-linear endomorphisms, acting coordinatewise.

Relation to Mathlib

Mathlib supplies the Hopf-algebra framework (coalgebras, bialgebras, antipodes, the convolution monoid WithConv on algebra maps) and the direct limit AddCommGroup.DirectLimit; the structure PDivisibleGroup and the points and Tate module built from it are the project's own, the Tate module functor TateModule being the one also used for elliptic curves.

Where it is used

These definitions give the p-divisible-group analogue of the Tate module construction used for elliptic curves over \mathbb{Q}, namely a \mathbb{Z}_p-module with an action of the R-algebra automorphisms of L; the module is imported widely in the tree as background for the p-adic Galois representations occurring in the modularity arguments.

References

  1. J. Tate, p-divisible groups, in: Proceedings of a Conference on Local Fields (Driebergen, 1966), Springer, 1967, 158–183
  2. M. Demazure, Lectures on p-divisible groups, Lecture Notes in Mathematics 302, Springer, 1972
  3. J.-P. Serre, Abelian l-adic Representations and Elliptic Curves, Benjamin, 1968

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_PDivisibleGroup_Points.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_PDivisibleGroup_Basic
import Definitions.Def_EllipticCurve_TateModule

set_option autoImplicit false

noncomputable section

open scoped TensorProduct
open Coalgebra Bialgebra WithConv

namespace PDivisibleGroup.Hopf

section AntipodeAlgHom

open HopfAlgebra

variable (R : Type*) [CommSemiring R] (H : Type*) [CommSemiring H] [HopfAlgebra R H]

def antipodeAlgHom : H →ₐ[R] H :=
  AlgHom.ofLinearMap (antipode R) antipode_one fun a b => by
    rw [antipode_mul, mul_comm]

@[simp] theorem antipodeAlgHom_apply (x : H) : antipodeAlgHom R H x = antipode R x := rfl

theorem antipodeAlgHom_toLinearMap : (antipodeAlgHom R H).toLinearMap = antipode R := rfl

variable {R H}
variable {A : Type*} [CommSemiring A] [Algebra R A]

theorem lift_comp_antipodeAlgHom_apply (φ : H →ₐ[R] A) (z : H ⊗[R] H) :
    Algebra.TensorProduct.lift φ (φ.comp (antipodeAlgHom R H)) (fun _ _ => .all _ _) z =
      φ (LinearMap.mul' R H ((antipode R).lTensor H z)) := by
  induction z with
  | zero => simp
  | tmul x y => simp [LinearMap.lTensor_tmul]
  | add x y hx hy => simp [map_add, hx, hy]

theorem lift_antipodeAlgHom_comp_apply (φ : H →ₐ[R] A) (z : H ⊗[R] H) :
    Algebra.TensorProduct.lift (φ.comp (antipodeAlgHom R H)) φ (fun _ _ => .all _ _) z =
      φ (LinearMap.mul' R H ((antipode R).rTensor H z)) := by
  induction z with
  | zero => simp
  | tmul x y => simp [LinearMap.rTensor_tmul]
  | add x y hx hy => simp [map_add, hx, hy]

theorem convMul_comp_antipodeAlgHom (φ : H →ₐ[R] A) :
    toConv φ * toConv (φ.comp (antipodeAlgHom R H)) = 1 := by
  refine WithConv.ext (AlgHom.ext fun x => ?_)
  change (toConv φ * toConv (φ.comp (antipodeAlgHom R H))) x = (1 : WithConv (H →ₐ[R] A)) x
  rw [AlgHom.convMul_apply, AlgHom.convOne_apply, ofConv_toConv, ofConv_toConv,
    lift_comp_antipodeAlgHom_apply, mul_antipode_lTensor_comul_apply, AlgHom.commutes]

theorem comp_antipodeAlgHom_convMul (φ : H →ₐ[R] A) :
    toConv (φ.comp (antipodeAlgHom R H)) * toConv φ = 1 := by
  refine WithConv.ext (AlgHom.ext fun x => ?_)
  change (toConv (φ.comp (antipodeAlgHom R H)) * toConv φ) x = (1 : WithConv (H →ₐ[R] A)) x
  rw [AlgHom.convMul_apply, AlgHom.convOne_apply, ofConv_toConv, ofConv_toConv,
    lift_antipodeAlgHom_comp_apply, mul_antipode_rTensor_comul_apply, AlgHom.commutes]

theorem isUnit_toConv_algHom (φ : H →ₐ[R] A) : IsUnit (toConv φ) :=
  isUnit_iff_exists.2 ⟨_, convMul_comp_antipodeAlgHom φ, comp_antipodeAlgHom_convMul φ⟩

end AntipodeAlgHom

section ConvComp

variable {R : Type*} [CommSemiring R] {H K : Type*} [CommSemiring H] [CommSemiring K]
  [Bialgebra R H] [Bialgebra R K]
variable (A : Type*) [CommSemiring A] [Algebra R A]

def convCompMonoidHom (π : H →ₐc[R] K) : WithConv (K →ₐ[R] A) →* WithConv (H →ₐ[R] A) where
  toFun f := toConv (f.ofConv.comp (π : H →ₐ[R] K))
  map_one' := by
    refine WithConv.ext ?_
    simp only [ofConv_toConv, AlgHom.convOne_def, AlgHom.comp_assoc, BialgHom.counitAlgHom_comp]
  map_mul' f g := by
    rw [AlgHom.convMul_comp_bialgHom_distrib]

@[simp] theorem convCompMonoidHom_apply (π : H →ₐc[R] K) (f : WithConv (K →ₐ[R] A)) :
    convCompMonoidHom A π f = toConv (f.ofConv.comp (π : H →ₐ[R] K)) := rfl

end ConvComp

end PDivisibleGroup.Hopf

namespace PDivisibleGroup

variable {R : Type} [CommRing R] {p h : ℕ} (G : PDivisibleGroup R p h)
variable (L : Type) [CommRing L] [Algebra R L]

def Point (v : ℕ) : Type := WithConv (G.level v →ₐ[R] L)

namespace Point

variable {G L} {v : ℕ}

instance instCommMonoid : CommMonoid (G.Point L v) :=
  inferInstanceAs (CommMonoid (WithConv (G.level v →ₐ[R] L)))

def toConv (x : G.Point L v) : WithConv (G.level v →ₐ[R] L) := x

def ofConv (f : WithConv (G.level v →ₐ[R] L)) : G.Point L v := f

def toAlgHom (x : G.Point L v) : G.level v →ₐ[R] L := WithConv.ofConv x

def ofAlgHom (f : G.level v →ₐ[R] L) : G.Point L v := WithConv.toConv f

@[simp] theorem toAlgHom_ofAlgHom (f : G.level v →ₐ[R] L) : toAlgHom (ofAlgHom f : G.Point L v) = f := rfl
@[simp] theorem ofAlgHom_toAlgHom (x : G.Point L v) : ofAlgHom (toAlgHom x) = x := rfl
@[simp] theorem toConv_ofConv (f : WithConv (G.level v →ₐ[R] L)) : toConv (ofConv f : G.Point L v) = f := rfl
@[simp] theorem ofConv_toConv (x : G.Point L v) : ofConv (toConv x) = x := rfl
theorem toConv_eq (x : G.Point L v) : toConv x = WithConv.toConv (toAlgHom x) := rfl

@[ext] theorem ext {x y : G.Point L v} (hxy : ∀ a, toAlgHom x a = toAlgHom y a) : x = y :=
  WithConv.ext (AlgHom.ext hxy)

theorem toConv_mul (x y : G.Point L v) : toConv (x * y) = toConv x * toConv y := rfl
theorem toConv_one : toConv (1 : G.Point L v) = 1 := rfl
theorem toConv_pow (x : G.Point L v) (n : ℕ) : toConv (x ^ n) = toConv x ^ n := rfl
theorem ofConv_mul (f g : WithConv (G.level v →ₐ[R] L)) : (ofConv (f * g) : G.Point L v) = ofConv f * ofConv g := rfl
theorem ofConv_pow (f : WithConv (G.level v →ₐ[R] L)) (n : ℕ) : (ofConv (f ^ n) : G.Point L v) = ofConv f ^ n := rfl

theorem one_apply (a : G.level v) : toAlgHom (1 : G.Point L v) a = algebraMap R L (counit (R := R) a) := rfl

theorem mul_apply (x y : G.Point L v) (a : G.level v) :
    toAlgHom (x * y) a =
      Algebra.TensorProduct.lift (toAlgHom x) (toAlgHom y) (fun _ _ => .all _ _) (comul (R := R) a) :=
  AlgHom.convMul_apply _ _ a

theorem isUnit (x : G.Point L v) : IsUnit x :=
  Hopf.isUnit_toConv_algHom (toAlgHom x)

noncomputable instance instCommGroup : CommGroup (G.Point L v) := commGroupOfIsUnit isUnit

theorem inv_eq (x : G.Point L v) :
    x⁻¹ = ofAlgHom ((toAlgHom x).comp (Hopf.antipodeAlgHom R (G.level v))) := by
  apply mul_left_cancel (a := x)
  rw [mul_inv_cancel]
  exact (Hopf.convMul_comp_antipodeAlgHom (toAlgHom x)).symm

theorem pow_card_eq_one (x : G.Point L v) : x ^ (p ^ v) = 1 :=
  G.point_pow_eq_one v (toConv x)

theorem toAlgHom_pow (x : G.Point L v) (n : ℕ) :
    toAlgHom (x ^ n) = (toAlgHom x).comp (Hopf.nsmulAlgHom R (G.level v) n) :=
  congrArg WithConv.ofConv (Hopf.toConv_pow_eq_toConv_comp_nsmulAlgHom (toAlgHom x) n)

end Point

noncomputable def pointIncl (v : ℕ) : G.Point L v →* G.Point L (v + 1) :=
  Hopf.convCompMonoidHom L (G.transition v)

variable {L}

theorem toAlgHom_pointIncl (v : ℕ) (x : G.Point L v) :
    Point.toAlgHom (G.pointIncl L v x) = (Point.toAlgHom x).comp (G.transitionAlgHom v) := rfl

@[simp] theorem pointIncl_apply (v : ℕ) (x : G.Point L v) (a : G.level (v + 1)) :
    Point.toAlgHom (G.pointIncl L v x) a = Point.toAlgHom x (G.transition v a) := rfl

theorem pointIncl_injective (v : ℕ) : Function.Injective (G.pointIncl L v) := by
  intro x y hxy
  have h := G.comp_transition_injective v (L := L)
    (show (Point.toAlgHom x).comp (G.transitionAlgHom v) = (Point.toAlgHom y).comp (G.transitionAlgHom v)
      from congrArg Point.toAlgHom hxy)
  exact Point.ext fun a => DFunLike.congr_fun h a

theorem mem_range_pointIncl_iff (v : ℕ) (y : G.Point L (v + 1)) :
    y ∈ Set.range (G.pointIncl L v) ↔ y ^ (p ^ v) = 1 := by
  change _ ↔ Point.toConv y ^ (p ^ v) = 1
  rw [← (G.exists_comp_transition_eq_iff v (Point.toConv y))]
  constructor
  · rintro ⟨x, rfl⟩
    exact ⟨Point.toAlgHom x, rfl⟩
  · rintro ⟨g, hg⟩
    exact ⟨Point.ofAlgHom g, Point.ext fun a => DFunLike.congr_fun hg a⟩

theorem exists_pointIncl_eq_of_pow_eq_one (v : ℕ) (y : G.Point L (v + 1)) (hy : y ^ (p ^ v) = 1) :
    ∃ x : G.Point L v, G.pointIncl L v x = y :=
  (G.mem_range_pointIncl_iff v y).2 hy

variable (L)

noncomputable def pointInclLE {v w : ℕ} (hvw : v ≤ w) : G.Point L v →* G.Point L w :=
  Nat.leRec (motive := fun w _ => G.Point L v →* G.Point L w) (MonoidHom.id _)
    (fun w _ ih => (G.pointIncl L w).comp ih) hvw

variable {L}

@[simp] theorem pointInclLE_self (v : ℕ) (x : G.Point L v) : G.pointInclLE L (le_refl v) x = x := by
  rw [pointInclLE, Nat.leRec_self]
  rfl

theorem pointInclLE_succ {v w : ℕ} (hvw : v ≤ w) (x : G.Point L v) :
    G.pointInclLE L (Nat.le_succ_of_le hvw) x = G.pointIncl L w (G.pointInclLE L hvw x) := by
  rw [pointInclLE, Nat.leRec_succ (h1 := hvw)]
  rfl

theorem pointInclLE_succ_self (v : ℕ) (x : G.Point L v) :
    G.pointInclLE L (Nat.le_succ v) x = G.pointIncl L v x := by
  rw [G.pointInclLE_succ (le_refl v), G.pointInclLE_self]

theorem pointInclLE_trans {u v w : ℕ} (huv : u ≤ v) (hvw : v ≤ w) (x : G.Point L u) :
    G.pointInclLE L (huv.trans hvw) x = G.pointInclLE L hvw (G.pointInclLE L huv x) := by
  induction hvw with
  | refl => rw [G.pointInclLE_self]
  | step hvw ih =>
    rw [G.pointInclLE_succ hvw, ← ih]
    exact G.pointInclLE_succ (huv.trans hvw) x

theorem pointInclLE_injective {v w : ℕ} (hvw : v ≤ w) : Function.Injective (G.pointInclLE L hvw) := by
  induction hvw with
  | refl => intro x y hxy; rwa [G.pointInclLE_self, G.pointInclLE_self] at hxy
  | step hvw ih =>
    intro x y hxy
    rw [G.pointInclLE_succ hvw, G.pointInclLE_succ hvw] at hxy
    exact ih (G.pointIncl_injective _ hxy)

theorem exists_pointInclLE_eq_of_pow_eq_one {v w : ℕ} (hvw : v ≤ w) (y : G.Point L w)
    (hy : y ^ (p ^ v) = 1) : ∃ x : G.Point L v, G.pointInclLE L hvw x = y := by
  induction hvw with
  | refl => exact ⟨y, G.pointInclLE_self v y⟩
  | @step w hvw ih =>

    have hyw : y ^ (p ^ w) = 1 := by
      obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le hvw
      have hpw : p ^ w = p ^ v * p ^ k := by rw [hk, pow_add]
      rw [hpw, pow_mul, hy, one_pow]
    obtain ⟨z, rfl⟩ := G.exists_pointIncl_eq_of_pow_eq_one w y hyw
    have hz : z ^ (p ^ v) = 1 := G.pointIncl_injective w (by rw [map_pow, hy, map_one])
    obtain ⟨x, rfl⟩ := ih z hz
    exact ⟨x, G.pointInclLE_succ hvw x⟩

noncomputable abbrev pointsDirectedSystemMap (v w : ℕ) (hvw : v ≤ w) :
    Additive (G.Point L v) →+ Additive (G.Point L w) :=
  MonoidHom.toAdditive (G.pointInclLE L hvw)

instance pointsDirectedSystem :
    DirectedSystem (fun v => Additive (G.Point L v)) fun v w hvw => G.pointsDirectedSystemMap (L := L) v w hvw where
  map_self _ x := G.pointInclLE_self _ x
  map_map _ _ _ huv hvw x := (G.pointInclLE_trans huv hvw x).symm

variable (L)

def Points : Type :=
  AddCommGroup.DirectLimit (fun v => Additive (G.Point L v)) fun v w hvw => G.pointsDirectedSystemMap v w hvw

noncomputable instance Points.instAddCommGroup : AddCommGroup (G.Points L) :=
  inferInstanceAs (AddCommGroup
    (AddCommGroup.DirectLimit (fun v => Additive (G.Point L v)) fun v w hvw => G.pointsDirectedSystemMap v w hvw))

noncomputable instance Points.instInhabited : Inhabited (G.Points L) := ⟨0⟩

noncomputable def pointsMkAdd (v : ℕ) : Additive (G.Point L v) →+ G.Points L :=
  AddCommGroup.DirectLimit.of (fun v => Additive (G.Point L v))
    (fun v w hvw => G.pointsDirectedSystemMap v w hvw) v

noncomputable def pointsMk (v : ℕ) : G.Point L v →* Multiplicative (G.Points L) :=
  AddMonoidHom.toMultiplicativeRight (G.pointsMkAdd L v)

variable {L}

theorem pointsMk_apply (v : ℕ) (x : G.Point L v) :
    G.pointsMk L v x = Multiplicative.ofAdd (G.pointsMkAdd L v (Additive.ofMul x)) := rfl

theorem toAdd_pointsMk (v : ℕ) (x : G.Point L v) :
    (G.pointsMk L v x).toAdd = G.pointsMkAdd L v (Additive.ofMul x) := rfl

@[simp] theorem pointsMkAdd_pointInclLE {v w : ℕ} (hvw : v ≤ w) (x : G.Point L v) :
    G.pointsMkAdd L w (Additive.ofMul (G.pointInclLE L hvw x)) = G.pointsMkAdd L v (Additive.ofMul x) :=
  AddCommGroup.DirectLimit.of_f (G := fun v => Additive (G.Point L v)) hvw (Additive.ofMul x)

@[simp] theorem pointsMkAdd_pointIncl (v : ℕ) (x : G.Point L v) :
    G.pointsMkAdd L (v + 1) (Additive.ofMul (G.pointIncl L v x)) = G.pointsMkAdd L v (Additive.ofMul x) := by
  rw [← G.pointInclLE_succ_self, pointsMkAdd_pointInclLE]

@[simp] theorem pointsMk_pointInclLE {v w : ℕ} (hvw : v ≤ w) (x : G.Point L v) :
    G.pointsMk L w (G.pointInclLE L hvw x) = G.pointsMk L v x :=
  congrArg Multiplicative.ofAdd (G.pointsMkAdd_pointInclLE hvw x)

@[simp] theorem pointsMk_pointIncl (v : ℕ) (x : G.Point L v) :
    G.pointsMk L (v + 1) (G.pointIncl L v x) = G.pointsMk L v x :=
  congrArg Multiplicative.ofAdd (G.pointsMkAdd_pointIncl v x)

theorem Points.exists_mkAdd (z : G.Points L) : ∃ (v : ℕ) (x : G.Point L v), G.pointsMkAdd L v (Additive.ofMul x) = z := by
  refine AddCommGroup.DirectLimit.induction_on (G := fun v => Additive (G.Point L v))
    (f := fun v w hvw => G.pointsDirectedSystemMap v w hvw)
    (C := fun z : G.Points L => ∃ (v : ℕ) (x : G.Point L v), G.pointsMkAdd L v (Additive.ofMul x) = z) z ?_
  intro v x
  exact ⟨v, Additive.toMul x, rfl⟩

theorem Points.induction_on {C : G.Points L → Prop} (z : G.Points L)
    (ih : ∀ (v : ℕ) (x : G.Point L v), C (G.pointsMkAdd L v (Additive.ofMul x))) : C z := by
  obtain ⟨v, x, rfl⟩ := Points.exists_mkAdd G z
  exact ih v x

theorem pointsMkAdd_injective (v : ℕ) : Function.Injective (G.pointsMkAdd L v) := by
  intro x y hxy
  have h0 : G.pointsMkAdd L v (x - y) = 0 := by rw [map_sub, hxy, sub_self]
  obtain ⟨w, hvw, hw⟩ := AddCommGroup.DirectLimit.of.zero_exact (G := fun v => Additive (G.Point L v))
    (f := fun v w hvw => G.pointsDirectedSystemMap v w hvw) v (x - y) h0
  have hinj := G.pointInclLE_injective (L := L) hvw
  have hw' : G.pointInclLE L hvw (Additive.toMul (x - y)) = 1 := hw
  have : Additive.toMul (x - y) = 1 := hinj (by rw [hw', map_one])
  exact sub_eq_zero.1 this

theorem pointsMk_injective (v : ℕ) : Function.Injective (G.pointsMk L v) := fun _ _ hxy =>
  G.pointsMkAdd_injective v (congrArg Multiplicative.toAdd hxy)

theorem pointsMkAdd_eq_pointsMkAdd_iff {v : ℕ} (x y : G.Point L v) :
    G.pointsMkAdd L v (Additive.ofMul x) = G.pointsMkAdd L v (Additive.ofMul y) ↔ x = y :=
  ⟨fun hxy => G.pointsMkAdd_injective v hxy, fun hxy => by rw [hxy]⟩

theorem nsmul_pointsMkAdd_eq_zero (v : ℕ) (x : G.Point L v) :
    (p ^ v) • G.pointsMkAdd L v (Additive.ofMul x) = 0 := by
  rw [← map_nsmul, ← ofMul_pow, Point.pow_card_eq_one, ofMul_one, map_zero]

theorem isTorsion_points_of_pos (hp : 0 < p) (z : G.Points L) : ∃ n : ℕ, 0 < n ∧ n • z = 0 := by
  obtain ⟨v, x, rfl⟩ := Points.exists_mkAdd G z
  exact ⟨p ^ v, pow_pos hp v, G.nsmul_pointsMkAdd_eq_zero v x⟩

section Map

variable {L' : Type} [CommRing L'] [Algebra R L'] {L'' : Type} [CommRing L''] [Algebra R L'']

def pointMap (φ : L →ₐ[R] L') (v : ℕ) : G.Point L v →* G.Point L' v where
  toFun x := Point.ofAlgHom (φ.comp (Point.toAlgHom x))
  map_one' := by
    apply congrArg Point.ofAlgHom
    change φ.comp ((Algebra.ofId R L).comp (counitAlgHom R (G.level v))) =
      (Algebra.ofId R L').comp (counitAlgHom R (G.level v))
    rw [← AlgHom.comp_assoc, Algebra.comp_ofId]
  map_mul' x y := by
    apply congrArg Point.ofConv
    apply WithConv.ofConv_injective
    exact AlgHom.comp_convMul_distrib φ (Point.toConv x) (Point.toConv y)

@[simp] theorem toAlgHom_pointMap (φ : L →ₐ[R] L') (v : ℕ) (x : G.Point L v) :
    Point.toAlgHom (G.pointMap φ v x) = φ.comp (Point.toAlgHom x) := rfl

theorem pointMap_id (v : ℕ) : G.pointMap (AlgHom.id R L) v = MonoidHom.id _ :=
  MonoidHom.ext fun _ => Point.ext fun _ => rfl

theorem pointMap_comp (φ : L →ₐ[R] L') (ψ : L' →ₐ[R] L'') (v : ℕ) :
    G.pointMap (ψ.comp φ) v = (G.pointMap ψ v).comp (G.pointMap φ v) :=
  MonoidHom.ext fun _ => Point.ext fun _ => rfl

theorem pointMap_pointIncl (φ : L →ₐ[R] L') (v : ℕ) (x : G.Point L v) :
    G.pointMap φ (v + 1) (G.pointIncl L v x) = G.pointIncl L' v (G.pointMap φ v x) :=
  Point.ext fun _ => rfl

theorem pointMap_pointInclLE (φ : L →ₐ[R] L') {v w : ℕ} (hvw : v ≤ w) (x : G.Point L v) :
    G.pointMap φ w (G.pointInclLE L hvw x) = G.pointInclLE L' hvw (G.pointMap φ v x) := by
  induction hvw with
  | refl => rw [G.pointInclLE_self, G.pointInclLE_self]
  | step hvw ih => rw [G.pointInclLE_succ hvw, G.pointInclLE_succ hvw, pointMap_pointIncl, ih]

noncomputable def pointsMap (φ : L →ₐ[R] L') : G.Points L →+ G.Points L' :=
  AddCommGroup.DirectLimit.map (G := fun v => Additive (G.Point L v)) (G' := fun v => Additive (G.Point L' v))
    (f := fun v w hvw => G.pointsDirectedSystemMap v w hvw)
    (f' := fun v w hvw => G.pointsDirectedSystemMap v w hvw)
    (fun v => MonoidHom.toAdditive (G.pointMap φ v))
    (fun _ _ hvw => AddMonoidHom.ext fun x =>
      congrArg Additive.ofMul (G.pointMap_pointInclLE φ hvw (Additive.toMul x)))

@[simp] theorem pointsMap_pointsMkAdd (φ : L →ₐ[R] L') (v : ℕ) (x : G.Point L v) :
    G.pointsMap φ (G.pointsMkAdd L v (Additive.ofMul x)) = G.pointsMkAdd L' v (Additive.ofMul (G.pointMap φ v x)) :=
  AddCommGroup.DirectLimit.map_apply_of (G := fun v => Additive (G.Point L v)) (G' := fun v => Additive (G.Point L' v))
    (f := fun v w hvw => G.pointsDirectedSystemMap v w hvw)
    (f' := fun v w hvw => G.pointsDirectedSystemMap v w hvw)
    (fun v => MonoidHom.toAdditive (G.pointMap φ v)) _ (Additive.ofMul x)

theorem pointsMap_id : G.pointsMap (AlgHom.id R L) = AddMonoidHom.id _ := by
  refine AddCommGroup.DirectLimit.hom_ext (G := fun v => Additive (G.Point L v))
    (f := fun v w hvw => G.pointsDirectedSystemMap v w hvw) (P := G.Points L) fun v => ?_
  refine AddMonoidHom.ext fun x => ?_
  change G.pointsMap (AlgHom.id R L) (G.pointsMkAdd L v x) = G.pointsMkAdd L v x
  exact G.pointsMap_pointsMkAdd (AlgHom.id R L) v (Additive.toMul x)

theorem pointsMap_comp (φ : L →ₐ[R] L') (ψ : L' →ₐ[R] L'') :
    G.pointsMap (ψ.comp φ) = (G.pointsMap ψ).comp (G.pointsMap φ) := by
  refine AddCommGroup.DirectLimit.hom_ext (G := fun v => Additive (G.Point L v))
    (f := fun v w hvw => G.pointsDirectedSystemMap v w hvw) (P := G.Points L'') fun v => ?_
  refine AddMonoidHom.ext fun x => ?_
  change G.pointsMap (ψ.comp φ) (G.pointsMkAdd L v x) = G.pointsMap ψ (G.pointsMap φ (G.pointsMkAdd L v x))
  rw [show x = Additive.ofMul (Additive.toMul x) from rfl, pointsMap_pointsMkAdd, pointsMap_pointsMkAdd,
    pointsMap_pointsMkAdd, pointMap_comp]
  rfl

theorem pointsMap_injective_of_injective (φ : L →ₐ[R] L') (hφ : Function.Injective φ) :
    Function.Injective (G.pointsMap φ) := by
  intro z w hzw
  induction z using Points.induction_on with
  | ih v x =>
    induction w using Points.induction_on with
    | ih w y =>

      rw [← G.pointsMkAdd_pointInclLE (le_max_left v w) x, ← G.pointsMkAdd_pointInclLE (le_max_right v w) y]
        at hzw ⊢
      rw [pointsMap_pointsMkAdd, pointsMap_pointsMkAdd, pointsMkAdd_eq_pointsMkAdd_iff] at hzw
      rw [pointsMkAdd_eq_pointsMkAdd_iff]
      refine Point.ext fun a => hφ ?_
      exact DFunLike.congr_fun (congrArg Point.toAlgHom hzw) a

end Map

noncomputable instance Points.instDistribMulAction : DistribMulAction (L ≃ₐ[R] L) (G.Points L) where
  smul σ z := G.pointsMap (σ : L →ₐ[R] L) z
  one_smul z := by
    change G.pointsMap ((1 : L ≃ₐ[R] L) : L →ₐ[R] L) z = z
    rw [show ((1 : L ≃ₐ[R] L) : L →ₐ[R] L) = AlgHom.id R L from rfl, pointsMap_id]
    rfl
  mul_smul σ τ z := by
    change G.pointsMap ((σ * τ : L ≃ₐ[R] L) : L →ₐ[R] L) z =
      G.pointsMap (σ : L →ₐ[R] L) (G.pointsMap (τ : L →ₐ[R] L) z)
    rw [show ((σ * τ : L ≃ₐ[R] L) : L →ₐ[R] L) = (σ : L →ₐ[R] L).comp (τ : L →ₐ[R] L) from rfl,
      pointsMap_comp]
    rfl
  smul_zero σ := map_zero (G.pointsMap (σ : L →ₐ[R] L))
  smul_add σ z w := map_add (G.pointsMap (σ : L →ₐ[R] L)) z w

theorem Points.smul_def (σ : L ≃ₐ[R] L) (z : G.Points L) : σ • z = G.pointsMap (σ : L →ₐ[R] L) z := rfl

@[simp] theorem Points.smul_pointsMkAdd (σ : L ≃ₐ[R] L) (v : ℕ) (x : G.Point L v) :
    σ • G.pointsMkAdd L v (Additive.ofMul x) =
      G.pointsMkAdd L v (Additive.ofMul (G.pointMap (σ : L →ₐ[R] L) v x)) :=
  G.pointsMap_pointsMkAdd _ v x

section Tate

variable [Fact p.Prime]
variable (L)

abbrev tateModule : AddSubgroup (ℕ → G.Points L) := TateModule p (G.Points L)

noncomputable abbrev tateModuleRep : (L ≃ₐ[R] L) →* Module.End ℤ_[p] (TateModule p (G.Points L)) :=
  TateModule.rep p (G.Points L) (L ≃ₐ[R] L)

theorem tateModuleRep_apply (σ : L ≃ₐ[R] L) (x : TateModule p (G.Points L)) (n : ℕ) :
    ((G.tateModuleRep L σ x : TateModule p (G.Points L)) : ℕ → G.Points L) n = σ • (x : ℕ → G.Points L) n :=
  rfl

end Tate

end PDivisibleGroup

end

Statements phrased using this module (170)

… and 20 more statements (search for the module name to find them).