Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CerednikDrinfeld_CriticalIndexChart.lean

definition module

Critical indices and truncated invariants of formal -module Cartier modules

Throughout, p is a prime, B a commutative ring and X a formal \mathcal O_D-module over B in the sense of the project's structure FormalODModule, with associated formal group X.F and Cartier module M= CartierModule p X.F, carrying the operator \Pi given by endAct X.varpiEnd, the action endAct (X.actEnd a) of a\in Zp2 p, Verschiebung V, Frobenius, homotheties and the Witt-vector scalar action. The first part defines cartierBaseChange: for ring maps f\colon B\to B', f'\colon B\to B'' and g\colon B'\to B'' with g\circ f=f', an additive map M(X_{f})\to M(X_{f'}), realised on power series by applying g coefficientwise, together with its compatibilities: it commutes with \Pi, with the Zp2 p-action, with V and its iterates and with Frobenius (the Verschiebung statements under characteristic p on B', B''), sends homothety b to homothety (g b) and the action of a Witt vector w to that of WittVector.map g w, transforms tangent vectors by g, preserves the graded pieces gradedPiece (the eigenspace conditions \mathrm{endAct}(X.\mathrm{actEnd}(\tau(c)))m=\mathrm{homothety}(j(\tau(c))^{p^i})m for all c\in\mathbb F_{p^2}), is the identity for g=\mathrm{id}, is compatible with composition, and is injective when g is.

In the CritChart namespace, with B of characteristic p and j\colon Zp2 p \to B: IsCritical X j i asserts that every m in the i-th graded piece M_i satisfies \Pi m\in VM; invariants X j i is the additive subgroup \{m\in M_i:\Pi m=Vm\}; vPowRange X j i k is the image V^k M_i; preInvariants X j i n is \{m\in M_i:\Pi m-Vm\in V^{2n+1}M_i\}; and truncInvariants X j i n is the quotient of preInvariants by the subgroup of its elements lying in V^{2n}M_i, with quotient map truncMk, membership criteria, the reduction invariantsRed from invariants, and the vanishing of the n=0 level. A functorial part fixes a base B_0, sets cartierObj X B' =M(X_{B'}) for a B_0-algebra B' and cartierMap X φ for a B_0-algebra map φ, shows that cartierMap preserves invariants, vPowRange and preInvariants, and so induces invariantsMap, preInvariantsMap and truncMap satisfying the identity and composition laws. Finally, under the hypothesis that V^2 maps M_i into M_i, the inclusions preInvariants X j i (n+1) ≤ preInvariants X j i n and V^{2(n+1)}M_i\subseteq V^{2n}M_i give the transition map truncTransition from level n+1 to level n.

Relation to Mathlib

Mathlib has no formal \mathcal O_D-modules or Cartier modules; these notions, and the operators \Pi, Verschiebung, Frobenius and homothety used here, are the project's own, built on Mathlib's multivariate power series, Witt vectors and GaloisField.

Where it is used

These subgroups and quotients are the data from which Drinfeld's étale sheaf attached to a special formal \mathcal O_D-module is built, the p-adic uniformisation of Shimura curves being the input to the level-lowering arguments (Mazur's principle and Ribet's theorem) in the passage from the Frey curve to Fermat's Last Theorem.

References

  1. J.-F. Boutot and H. Carayol, Uniformisation p-adique des courbes de Shimura: les théorèmes de Čerednik et de Drinfeld, Astérisque 196–197 (1991), 45–158, chap. II, §§4, 6
  2. V. G. Drinfeld, Coverings of p-adic symmetric domains, Functional Analysis and its Applications 10 (1976), 107–115
  3. T. Zink, Cartiertheorie kommutativer formaler Gruppen, Teubner-Texte zur Mathematik 68, Teubner, 1984

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_CerednikDrinfeld_CriticalIndexChart.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_MvFormalGroup_NegV2
import Definitions.Def_MvFormalGroup_CartierModule
import Definitions.Def_MvFormalGroup_CartierModuleHomothety
import Definitions.Def_MvFormalGroup_CartierModuleWittAction
import Definitions.Def_MvFormalGroup_CartierModuleBaseChange
import Definitions.Def_CerednikDrinfeld_SpecialFormalModule
import Definitions.Def_CerednikDrinfeld_CartierGradedPiece
import Definitions.Def_CerednikDrinfeld_CartierStructureConstants

set_option autoImplicit false

noncomputable section

universe u v w

namespace CerednikDrinfeld

namespace FormalODModule

open MvFormalGroup MvFormalGroup.CartierModule

section BaseChange

variable {p : ℕ} [hp : Fact p.Prime] {B : Type u} [CommRing B] {B' : Type v} [CommRing B']
  {B'' : Type w} [CommRing B'']

theorem map_F_map (f : B →+* B') (g : B' →+* B'') (X : FormalODModule p B) :
    (X.map f).F.map g = (X.map (g.comp f)).F :=
  MvFormalGroup.map_map_ringHom X.F f g

def cartierBaseChange (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''} (g : B' →+* B'')
    (hg : g.comp f = f') : CartierModule p (X.map f).F →+ CartierModule p (X.map f').F :=
  CartierModule.baseChangeEq g (by rw [map_F, map_F, MvFormalGroup.map_map_ringHom, hg])

theorem toPowerSeries_cartierBaseChange (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (m : CartierModule p (X.map f).F) (l : Fin 2) :
    (X.cartierBaseChange g hg m).toPowerSeries l = MvPowerSeries.map g (m.toPowerSeries l) := rfl

theorem cartierBaseChange_pi (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g hg (endAct (X.map f).varpiEnd m) =
      endAct (X.map f').varpiEnd (X.cartierBaseChange g hg m) := by
  refine CartierModule.baseChangeEq_endAct g _ (fun i => ?_) m
  subst hg
  rfl

theorem cartierBaseChange_act (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (a : Zp2 p) (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g hg (endAct ((X.map f).actEnd a) m) =
      endAct ((X.map f').actEnd a) (X.cartierBaseChange g hg m) := by
  refine CartierModule.baseChangeEq_endAct g _ (fun i => ?_) m
  subst hg
  rfl

theorem cartierBaseChange_verschiebung [CharP B' p] [CharP B'' p] (X : FormalODModule p B)
    {f : B →+* B'} {f' : B →+* B''} (g : B' →+* B'') (hg : g.comp f = f')
    (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g hg (verschiebung m) = verschiebung (X.cartierBaseChange g hg m) :=
  CartierModule.baseChangeEq_verschiebung g _ m

theorem cartierBaseChange_verschiebung_iterate [CharP B' p] [CharP B'' p] (X : FormalODModule p B)
    {f : B →+* B'} {f' : B →+* B''} (g : B' →+* B'') (hg : g.comp f = f') (k : ℕ)
    (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g hg ((⇑(verschiebung (p := p) (Φ := (X.map f).F)))^[k] m) =
      (⇑(verschiebung (p := p) (Φ := (X.map f').F)))^[k] (X.cartierBaseChange g hg m) :=
  CartierModule.baseChangeEq_verschiebung_iterate g _ k m

theorem cartierBaseChange_frobenius (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g hg (frobenius m) = frobenius (X.cartierBaseChange g hg m) :=
  CartierModule.baseChangeEq_frobenius g _ m

theorem cartierBaseChange_homothety (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (b : B') (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g hg (homothety b m) = homothety (g b) (X.cartierBaseChange g hg m) :=
  CartierModule.baseChangeEq_homothety g _ b m

theorem cartierBaseChange_smul_witt (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (w : WittVector p B') (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g hg (w • m) = (WittVector.map g w) • (X.cartierBaseChange g hg m) :=
  CartierModule.baseChangeEq_smul_witt g _ w m

theorem tangent_cartierBaseChange (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (m : CartierModule p (X.map f).F) :
    tangent (X.cartierBaseChange g hg m) = fun l => g (tangent m l) :=
  CartierModule.tangent_baseChangeEq g _ m

theorem cartierBaseChange_mem_gradedPiece (X : FormalODModule p B) (j : Zp2 p →+* B) {f : B →+* B'}
    {f' : B →+* B''} (g : B' →+* B'') (hg : g.comp f = f') (i : ℕ)
    {m : CartierModule p (X.map f).F} (hm : m ∈ (X.map f).gradedPiece (f.comp j) i) :
    X.cartierBaseChange g hg m ∈ (X.map f').gradedPiece (f'.comp j) i := by
  intro c
  rw [← cartierBaseChange_act, hm c, cartierBaseChange_homothety]
  congr 1
  rw [map_pow, ← hg]
  rfl

theorem cartierBaseChange_id (X : FormalODModule p B) {f : B →+* B'}
    (h : (RingHom.id B').comp f = f) (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange (RingHom.id B') h m = m :=
  CartierModule.baseChangeEq_id _ m

theorem cartierBaseChange_comp {B₃ : Type*} [CommRing B₃] (X : FormalODModule p B) {f : B →+* B'}
    {f' : B →+* B''} {f'' : B →+* B₃} (g : B' →+* B'') (hg : g.comp f = f') (g' : B'' →+* B₃)
    (hg' : g'.comp f' = f'') (hgg' : (g'.comp g).comp f = f'') (m : CartierModule p (X.map f).F) :
    X.cartierBaseChange g' hg' (X.cartierBaseChange g hg m) = X.cartierBaseChange (g'.comp g) hgg' m :=
  CartierModule.baseChangeEq_baseChangeEq g g' _ _ _ m

theorem cartierBaseChange_injective (X : FormalODModule p B) {f : B →+* B'} {f' : B →+* B''}
    (g : B' →+* B'') (hg : g.comp f = f') (hinj : Function.Injective g) :
    Function.Injective (X.cartierBaseChange g hg) :=
  CartierModule.baseChangeEq_injective g _ hinj

end BaseChange

namespace CritChart

variable {p : ℕ} [hp : Fact p.Prime] {B : Type u} [CommRing B]

section OneBase

variable [CharP B p]

def IsCritical (X : FormalODModule p B) (j : Zp2 p →+* B) (i : ℕ) : Prop :=
  ∀ m ∈ X.gradedPiece j i, ∃ g : CartierModule p X.F, verschiebung g = endAct X.varpiEnd m

def invariants (X : FormalODModule p B) (j : Zp2 p →+* B) (i : ℕ) : AddSubgroup (CartierModule p X.F) where
  carrier := {m | m ∈ X.gradedPiece j i ∧ endAct X.varpiEnd m = verschiebung m}
  zero_mem' := ⟨zero_mem _, by rw [map_zero, map_zero]⟩
  add_mem' := fun {a b} ha hb => ⟨add_mem ha.1 hb.1, by rw [map_add, map_add, ha.2, hb.2]⟩
  neg_mem' := fun {a} ha => ⟨neg_mem ha.1, by rw [map_neg, map_neg, ha.2]⟩

theorem mem_invariants_iff (X : FormalODModule p B) (j : Zp2 p →+* B) (i : ℕ) (m : CartierModule p X.F) :
    m ∈ invariants X j i ↔ m ∈ X.gradedPiece j i ∧ endAct X.varpiEnd m = verschiebung m :=
  Iff.rfl

theorem invariants_le_gradedPiece (X : FormalODModule p B) (j : Zp2 p →+* B) (i : ℕ) :
    invariants X j i ≤ X.gradedPiece j i := fun _ hm => hm.1

def vPowRange (X : FormalODModule p B) (j : Zp2 p →+* B) (i k : ℕ) : AddSubgroup (CartierModule p X.F) where
  carrier := {m | ∃ g ∈ X.gradedPiece j i, (⇑(verschiebung (p := p) (Φ := X.F)))^[k] g = m}
  zero_mem' := ⟨0, zero_mem _, iterate_map_zero _ k⟩
  add_mem' := by
    rintro a b ⟨g, hg, rfl⟩ ⟨g', hg', rfl⟩
    exact ⟨g + g', add_mem hg hg', iterate_map_add _ k g g'⟩
  neg_mem' := by
    rintro a ⟨g, hg, rfl⟩
    exact ⟨-g, neg_mem hg, iterate_map_neg _ k g⟩

theorem mem_vPowRange_iff (X : FormalODModule p B) (j : Zp2 p →+* B) (i k : ℕ) (m : CartierModule p X.F) :
    m ∈ vPowRange X j i k ↔
      ∃ g ∈ X.gradedPiece j i, (⇑(verschiebung (p := p) (Φ := X.F)))^[k] g = m :=
  Iff.rfl

theorem vPowRange_zero (X : FormalODModule p B) (j : Zp2 p →+* B) (i : ℕ) :
    vPowRange X j i 0 = X.gradedPiece j i := by
  ext m
  rw [mem_vPowRange_iff]
  constructor
  · rintro ⟨g, hg, rfl⟩
    exact hg
  · intro hm
    exact ⟨m, hm, rfl⟩

theorem iterate_verschiebung_mem_vPowRange (X : FormalODModule p B) (j : Zp2 p →+* B) (i k : ℕ)
    {g : CartierModule p X.F} (hg : g ∈ X.gradedPiece j i) :
    (⇑(verschiebung (p := p) (Φ := X.F)))^[k] g ∈ vPowRange X j i k :=
  ⟨g, hg, rfl⟩

def preInvariants (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) :
    AddSubgroup (CartierModule p X.F) where
  carrier := {m | m ∈ X.gradedPiece j i ∧ endAct X.varpiEnd m - verschiebung m ∈ vPowRange X j i (2 * n + 1)}
  zero_mem' := ⟨zero_mem _, by rw [map_zero, map_zero, sub_zero]; exact zero_mem _⟩
  add_mem' := fun {a b} ha hb => ⟨add_mem ha.1 hb.1, by
    rw [map_add, map_add, add_sub_add_comm]
    exact add_mem ha.2 hb.2⟩
  neg_mem' := fun {a} ha => ⟨neg_mem ha.1, by
    rw [map_neg, map_neg, ← neg_sub', sub_eq_add_neg]
    exact neg_mem ha.2⟩

theorem mem_preInvariants_iff (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ)
    (m : CartierModule p X.F) :
    m ∈ preInvariants X j i n ↔
      m ∈ X.gradedPiece j i ∧ endAct X.varpiEnd m - verschiebung m ∈ vPowRange X j i (2 * n + 1) :=
  Iff.rfl

theorem invariants_le_preInvariants (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) :
    invariants X j i ≤ preInvariants X j i n := fun m hm =>
  ⟨hm.1, by rw [hm.2, sub_self]; exact zero_mem _⟩

theorem preInvariants_le_gradedPiece (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) :
    preInvariants X j i n ≤ X.gradedPiece j i := fun _ hm => hm.1

abbrev truncRel (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) : AddSubgroup ↥(preInvariants X j i n) :=
  (vPowRange X j i (2 * n)).addSubgroupOf (preInvariants X j i n)

abbrev truncInvariants (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) : Type u :=
  ↥(preInvariants X j i n) ⧸ truncRel X j i n

abbrev truncMk (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) :
    ↥(preInvariants X j i n) →+ truncInvariants X j i n :=
  QuotientAddGroup.mk' (truncRel X j i n)

theorem truncMk_surjective (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) :
    Function.Surjective (truncMk X j i n) :=
  QuotientAddGroup.mk'_surjective _

theorem truncMk_eq_zero_iff (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ)
    (m : ↥(preInvariants X j i n)) :
    truncMk X j i n m = 0 ↔ (m : CartierModule p X.F) ∈ vPowRange X j i (2 * n) := by
  rw [QuotientAddGroup.mk'_apply, QuotientAddGroup.eq_zero_iff]
  rfl

theorem truncMk_eq_truncMk_iff (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ)
    (m m' : ↥(preInvariants X j i n)) :
    truncMk X j i n m = truncMk X j i n m' ↔ (m : CartierModule p X.F) - m' ∈ vPowRange X j i (2 * n) := by
  rw [← sub_eq_zero, ← map_sub, truncMk_eq_zero_iff]
  rfl

theorem truncInvariants_zero_subsingleton (X : FormalODModule p B) (j : Zp2 p →+* B) (i : ℕ) :
    Subsingleton (truncInvariants X j i 0) := by
  refine ⟨fun a b => ?_⟩
  obtain ⟨a, rfl⟩ := truncMk_surjective X j i 0 a
  obtain ⟨b, rfl⟩ := truncMk_surjective X j i 0 b
  rw [truncMk_eq_truncMk_iff, Nat.mul_zero, vPowRange_zero]
  exact sub_mem a.2.1 b.2.1

def invariantsRed (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) :
    ↥(invariants X j i) →+ truncInvariants X j i n :=
  (truncMk X j i n).comp (AddSubgroup.inclusion (invariants_le_preInvariants X j i n))

theorem invariantsRed_apply (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ) (m : ↥(invariants X j i)) :
    invariantsRed X j i n m = truncMk X j i n (AddSubgroup.inclusion (invariants_le_preInvariants X j i n) m) :=
  rfl

end OneBase

section Functor

variable {B₀ : Type u} [CommRing B₀]

abbrev cartierObj (X : FormalODModule p B₀) (B' : Type v) [CommRing B'] [Algebra B₀ B'] : Type v :=
  CartierModule p (X.map (algebraMap B₀ B')).F

abbrev cartierMap (X : FormalODModule p B₀) {B' : Type v} [CommRing B'] [Algebra B₀ B'] {B'' : Type w}
    [CommRing B''] [Algebra B₀ B''] (φ : B' →ₐ[B₀] B'') : cartierObj X B' →+ cartierObj X B'' :=
  X.cartierBaseChange φ.toRingHom φ.comp_algebraMap

variable {B' : Type v} [CommRing B'] [Algebra B₀ B'] {B'' : Type w} [CommRing B''] [Algebra B₀ B'']

theorem cartierMap_id (X : FormalODModule p B₀) (m : cartierObj X B') : cartierMap X (AlgHom.id B₀ B') m = m :=
  X.cartierBaseChange_id _ m

theorem cartierMap_comp (X : FormalODModule p B₀) {B₃ : Type*} [CommRing B₃] [Algebra B₀ B₃]
    (φ : B' →ₐ[B₀] B'') (ψ : B'' →ₐ[B₀] B₃) (m : cartierObj X B') :
    cartierMap X ψ (cartierMap X φ m) = cartierMap X (ψ.comp φ) m :=
  X.cartierBaseChange_comp _ _ _ _ _ m

variable [CharP B' p] [CharP B'' p]

theorem cartierMap_mem_invariants (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i : ℕ) (φ : B' →ₐ[B₀] B'')
    {m : cartierObj X B'} (hm : m ∈ invariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i) :
    cartierMap X φ m ∈ invariants (X.map (algebraMap B₀ B'')) ((algebraMap B₀ B'').comp j) i := by
  refine ⟨X.cartierBaseChange_mem_gradedPiece j φ.toRingHom φ.comp_algebraMap i hm.1, ?_⟩
  rw [← cartierBaseChange_pi, hm.2, cartierBaseChange_verschiebung]

theorem cartierMap_mem_vPowRange (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i k : ℕ) (φ : B' →ₐ[B₀] B'')
    {m : cartierObj X B'} (hm : m ∈ vPowRange (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i k) :
    cartierMap X φ m ∈ vPowRange (X.map (algebraMap B₀ B'')) ((algebraMap B₀ B'').comp j) i k := by
  obtain ⟨g, hg, rfl⟩ := hm
  exact ⟨cartierMap X φ g, X.cartierBaseChange_mem_gradedPiece j φ.toRingHom φ.comp_algebraMap i hg,
    (X.cartierBaseChange_verschiebung_iterate φ.toRingHom φ.comp_algebraMap k g).symm⟩

theorem cartierMap_mem_preInvariants (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ)
    (φ : B' →ₐ[B₀] B'') {m : cartierObj X B'}
    (hm : m ∈ preInvariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i n) :
    cartierMap X φ m ∈ preInvariants (X.map (algebraMap B₀ B'')) ((algebraMap B₀ B'').comp j) i n := by
  refine ⟨X.cartierBaseChange_mem_gradedPiece j φ.toRingHom φ.comp_algebraMap i hm.1, ?_⟩
  have h := cartierMap_mem_vPowRange X j i (2 * n + 1) φ hm.2
  rwa [map_sub, cartierBaseChange_pi, cartierBaseChange_verschiebung] at h

def invariantsMap (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i : ℕ) (φ : B' →ₐ[B₀] B'') :
    ↥(invariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i) →+
      ↥(invariants (X.map (algebraMap B₀ B'')) ((algebraMap B₀ B'').comp j) i) :=
  ((cartierMap X φ).comp (AddSubgroup.subtype _)).codRestrict _
    fun m => cartierMap_mem_invariants X j i φ m.2

@[simp] theorem coe_invariantsMap (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i : ℕ) (φ : B' →ₐ[B₀] B'')
    (m : ↥(invariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i)) :
    (invariantsMap X j i φ m : cartierObj X B'') = cartierMap X φ m := rfl

def preInvariantsMap (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ) (φ : B' →ₐ[B₀] B'') :
    ↥(preInvariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i n) →+
      ↥(preInvariants (X.map (algebraMap B₀ B'')) ((algebraMap B₀ B'').comp j) i n) :=
  ((cartierMap X φ).comp (AddSubgroup.subtype _)).codRestrict _
    fun m => cartierMap_mem_preInvariants X j i n φ m.2

@[simp] theorem coe_preInvariantsMap (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ)
    (φ : B' →ₐ[B₀] B'') (m : ↥(preInvariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i n)) :
    (preInvariantsMap X j i n φ m : cartierObj X B'') = cartierMap X φ m := rfl

def truncMap (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ) (φ : B' →ₐ[B₀] B'') :
    truncInvariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i n →+
      truncInvariants (X.map (algebraMap B₀ B'')) ((algebraMap B₀ B'').comp j) i n :=
  QuotientAddGroup.map _ _ (preInvariantsMap X j i n φ) fun _ hm =>
    cartierMap_mem_vPowRange X j i (2 * n) φ hm

theorem truncMap_truncMk (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ) (φ : B' →ₐ[B₀] B'')
    (m₀ : ↥(preInvariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i n)) :
    truncMap X j i n φ (truncMk _ _ i n m₀) = truncMk _ _ i n (preInvariantsMap X j i n φ m₀) :=
  rfl

theorem truncMap_invariantsRed (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ) (φ : B' →ₐ[B₀] B'')
    (m : ↥(invariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i)) :
    truncMap X j i n φ (invariantsRed _ _ i n m) = invariantsRed _ _ i n (invariantsMap X j i φ m) :=
  rfl

omit [CharP B'' p] in

theorem invariantsMap_id (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i : ℕ)
    (m : ↥(invariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i)) :
    invariantsMap X j i (AlgHom.id B₀ B') m = m :=
  Subtype.ext (cartierMap_id X m.1)

theorem invariantsMap_comp (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i : ℕ) {B₃ : Type*}
    [CommRing B₃] [Algebra B₀ B₃] [CharP B₃ p] (φ : B' →ₐ[B₀] B'') (ψ : B'' →ₐ[B₀] B₃)
    (m : ↥(invariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i)) :
    invariantsMap X j i ψ (invariantsMap X j i φ m) = invariantsMap X j i (ψ.comp φ) m :=
  Subtype.ext (cartierMap_comp X φ ψ m.1)

omit [CharP B'' p] in

theorem truncMap_id (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ)
    (x : truncInvariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i n) :
    truncMap X j i n (AlgHom.id B₀ B') x = x := by
  obtain ⟨m, rfl⟩ := truncMk_surjective _ _ i n x
  exact (truncMap_truncMk X j i n _ m).trans (congrArg _ (Subtype.ext (cartierMap_id X m.1)))

theorem truncMap_comp (X : FormalODModule p B₀) (j : Zp2 p →+* B₀) (i n : ℕ) {B₃ : Type*}
    [CommRing B₃] [Algebra B₀ B₃] [CharP B₃ p] (φ : B' →ₐ[B₀] B'') (ψ : B'' →ₐ[B₀] B₃)
    (x : truncInvariants (X.map (algebraMap B₀ B')) ((algebraMap B₀ B').comp j) i n) :
    truncMap X j i n ψ (truncMap X j i n φ x) = truncMap X j i n (ψ.comp φ) x := by
  obtain ⟨m, rfl⟩ := truncMk_surjective _ _ i n x
  exact congrArg (truncMk _ _ i n) (Subtype.ext (cartierMap_comp X φ ψ m.1))

end Functor

section Transition

variable [CharP B p]

theorem preInvariants_succ_le (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ)
    (hV : ∀ g ∈ X.gradedPiece j i, verschiebung (verschiebung g) ∈ X.gradedPiece j i) :
    preInvariants X j i (n + 1) ≤ preInvariants X j i n := by
  intro m hm
  refine ⟨hm.1, ?_⟩
  obtain ⟨g, hg, hgm⟩ := hm.2
  refine ⟨verschiebung (verschiebung g), hV g hg, ?_⟩
  rw [← hgm, show 2 * (n + 1) + 1 = (2 * n + 1) + 2 by ring,
    Function.iterate_add_apply (⇑(verschiebung (p := p) (Φ := X.F))) (2 * n + 1) 2 g]
  rfl

theorem vPowRange_succ_le (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ)
    (hV : ∀ g ∈ X.gradedPiece j i, verschiebung (verschiebung g) ∈ X.gradedPiece j i) :
    vPowRange X j i (2 * (n + 1)) ≤ vPowRange X j i (2 * n) := by
  rintro m ⟨g, hg, hgm⟩
  refine ⟨verschiebung (verschiebung g), hV g hg, ?_⟩
  rw [← hgm, show 2 * (n + 1) = 2 * n + 2 by ring,
    Function.iterate_add_apply (⇑(verschiebung (p := p) (Φ := X.F))) (2 * n) 2 g]
  rfl

def truncTransition (X : FormalODModule p B) (j : Zp2 p →+* B) (i n : ℕ)
    (hV : ∀ g ∈ X.gradedPiece j i, verschiebung (verschiebung g) ∈ X.gradedPiece j i) :
    truncInvariants X j i (n + 1) →+ truncInvariants X j i n :=
  QuotientAddGroup.map _ _ (AddSubgroup.inclusion (preInvariants_succ_le X j i n hV))
    fun _ hm => vPowRange_succ_le X j i n hV hm

end Transition

end CritChart

end FormalODModule

end CerednikDrinfeld

end

Statements phrased using this module (12)