feat(RingTheory/Perfectoid): Fontaine's theta map is surjective (#26384)

This PR continues the work from #22332.

Original PR: #22332

In this file, we show that when R is p-adically complete and Frob : R/p -> R/p is surjective, Fontaine's theta map is surjective.

Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>

Author: jjdishere

Mathlib.lean

@@ -4719,6 +4719,7 @@ public import Mathlib.LinearAlgebra.RootSystem.RootPositive
 public import Mathlib.LinearAlgebra.RootSystem.WeylGroup
 public import Mathlib.LinearAlgebra.SModEq
 public import Mathlib.LinearAlgebra.SModEq.Basic
+public import Mathlib.LinearAlgebra.SModEq.Pointwise
 public import Mathlib.LinearAlgebra.Semisimple
 public import Mathlib.LinearAlgebra.SesquilinearForm
 public import Mathlib.LinearAlgebra.SesquilinearForm.Basic

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -137,6 +137,11 @@ theorem toAddSubgroup_le : p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p' :=
 theorem toAddSubgroup_mono : Monotone (toAddSubgroup : Submodule R M → AddSubgroup M) :=
   toAddSubgroup_strictMono.monotone
 
+@[simp]
+theorem toAddSubgroup_toAddSubmonoid (p : Submodule R M) :
+    p.toAddSubgroup.toAddSubmonoid = p.toAddSubmonoid :=
+  rfl
+
 @[gcongr]
 protected alias ⟨_, _root_.GCongr.Submodule.toAddSubgroup_le⟩ := Submodule.toAddSubgroup_le
 

Mathlib/LinearAlgebra/SModEq/Basic.lean

@@ -21,8 +21,9 @@ open Submodule
 open Polynomial
 
 variable {R : Type*} [Ring R]
+variable {S : Type*} [Ring S]
 variable {A : Type*} [CommRing A]
-variable {M : Type*} [AddCommGroup M] [Module R M] (U U₁ U₂ : Submodule R M)
+variable {M : Type*} [AddCommGroup M] [Module R M] [Module S M] (U U₁ U₂ : Submodule R M)
 variable {x x₁ x₂ y y₁ y₂ z z₁ z₂ : M}
 variable {N : Type*} [AddCommGroup N] [Module R N] (V V₁ V₂ : Submodule R N)
 
@@ -54,6 +55,11 @@ theorem bot : x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y := by
 theorem mono (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) : x ≡ y [SMOD U₂] :=
   (Submodule.Quotient.eq U₂).2 <| HU <| (Submodule.Quotient.eq U₁).1 hxy
 
+lemma of_toAddSubgroup_le {U : Submodule R M} {V : Submodule S M}
+    (h : U.toAddSubgroup ≤ V.toAddSubgroup) {x y : M} (hxy : x ≡ y [SMOD U]) : x ≡ y [SMOD V] := by
+  simp only [SModEq, Submodule.Quotient.eq] at hxy ⊢
+  exact h hxy
+
 @[refl]
 protected theorem refl (x : M) : x ≡ x [SMOD U] :=
   @rfl _ _

Mathlib/LinearAlgebra/SModEq/Pointwise.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2025 Jiedong Jiang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jiedong Jiang
+-/
+module
+
+public import Mathlib.Algebra.Algebra.Operations
+public import Mathlib.LinearAlgebra.SModEq.Basic
+
+/-!
+# Pointwise lemmas for modular equivalence
+
+In this file, we record more lemmas about `SModEq` on elements
+of modules or rings.
+-/
+
+@[expose] public section
+
+open Submodule
+
+open Polynomial
+
+variable {R : Type*} [Ring R] {I : Ideal R}
+variable {M : Type*} [AddCommGroup M] [Module R M] {U : Submodule R M}
+variable {x y : M}
+
+namespace SModEq
+
+/--
+A variant of `SModEq.smul`, where the scalar belongs to an ideal.
+-/
+theorem smul' (hxy : x ≡ y [SMOD U])
+    {c : R} (hc : c ∈ I) : c • x ≡ c • y [SMOD (I • U)] := by
+  rw [SModEq.sub_mem] at hxy ⊢
+  rw [← smul_sub]
+  exact smul_mem_smul hc hxy
+
+end SModEq

Mathlib/RingTheory/AdicCompletion/Basic.lean

@@ -71,6 +71,32 @@ theorem IsHausdorff.eq_iff_smodEq [IsHausdorff I M] {x y : M} :
   apply IsHausdorff.haus' (I := I) (x - y)
   simpa [SModEq.sub_mem] using h
 
+theorem IsHausdorff.map_algebraMap_iff [CommRing S] [Algebra R S] :
+    IsHausdorff (I.map (algebraMap R S)) S ↔ IsHausdorff I S := by
+  simp only [isHausdorff_iff, smul_eq_mul, Ideal.mul_top, Ideal.smul_top_eq_map]
+  congr!
+  simp only [← Ideal.map_pow]
+  rfl
+
+theorem IsHausdorff.of_map [CommRing S] [Module S M] {J : Ideal S} [Algebra R S]
+    [IsScalarTower R S M] (hIJ : I.map (algebraMap R S) ≤ J) [IsHausdorff J M] :
+    IsHausdorff I M := by
+  refine ⟨fun x h ↦ IsHausdorff.haus ‹_› x fun n ↦ ?_⟩
+  apply SModEq.of_toAddSubgroup_le
+      (U := (I ^ n • ⊤ : Submodule R M)) (V := (J ^ n • ⊤ : Submodule S M))
+  · rw [← AddSubgroup.toAddSubmonoid_le]
+    simp only [Submodule.toAddSubgroup_toAddSubmonoid, Submodule.smul_toAddSubmonoid,
+      Submodule.top_toAddSubmonoid]
+    rw [AddSubmonoid.smul_le]
+    intro r hr m _
+    rw [← algebraMap_smul S r m]
+    apply AddSubmonoid.smul_mem_smul
+    · have := Ideal.mem_map_of_mem (algebraMap R S) hr
+      simp only [Ideal.map_pow] at this
+      apply Ideal.pow_right_mono (I := I.map (algebraMap R S)) hIJ n this
+    · trivial
+  · exact h n
+
 variable (I) in
 theorem IsHausdorff.funext {M : Type*} [IsHausdorff I N] {f g : M → N}
     (h : ∀ n m, Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (f m) =

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

@@ -5,9 +5,10 @@ Authors: Judith Ludwig, Christian Merten
 -/
 module
 
+public import Mathlib.Algebra.DirectSum.Basic
+public import Mathlib.LinearAlgebra.SModEq.Pointwise
 public import Mathlib.RingTheory.AdicCompletion.Basic
 public import Mathlib.RingTheory.AdicCompletion.Algebra
-public import Mathlib.Algebra.DirectSum.Basic
 
 /-!
 # Functoriality of adic completions
@@ -197,6 +198,9 @@ theorem map_zero : map I (0 : M →ₗ[R] N) = 0 := by
   ext
   simp
 
+theorem map_of (f : M →ₗ[R] N) (x : M) : map I f (of I M x) = of I N (f x) :=
+  rfl
+
 /-- A linear equiv induces a linear equiv on adic completions. -/
 def congr (f : M ≃ₗ[R] N) :
     AdicCompletion I M ≃ₗ[AdicCompletion I R] AdicCompletion I N :=
@@ -360,4 +364,102 @@ end Pi
 
 end Families
 
+open Submodule
+
+variable {I}
+
+theorem exists_smodEq_pow_add_one_smul {f : M →ₗ[R] N}
+    (h : Function.Surjective (mkQ (I • ⊤) ∘ₗ f)) {y : N} {n : ℕ}
+    (hy : y ∈ (I ^ n • ⊤ : Submodule R N)) :
+    ∃ x ∈ (I ^ n • ⊤ : Submodule R M), f x ≡ y [SMOD (I ^ (n + 1) • ⊤ : Submodule R N)] := by
+  induction hy using smul_induction_on' with
+  | smul r hr y _ =>
+    obtain ⟨x, hx⟩ := h (mkQ _ y)
+    use r • x, smul_mem_smul hr mem_top
+    simp only [coe_comp, Function.comp_apply, mkQ_apply, ← SModEq.def, map_smul] at ⊢ hx
+    rw [pow_succ, ← smul_smul]
+    exact SModEq.smul' hx hr
+  | add y1 hy1 y2 hy2 ih1 ih2 =>
+    obtain ⟨x1, hx1, hx1'⟩ := ih1
+    obtain ⟨x2, hx2, hx2'⟩ := ih2
+    use x1 + x2, add_mem hx1 hx2
+    simp only [map_add]
+    exact SModEq.add hx1' hx2'
+
+theorem exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top {f : M →ₗ[R] N}
+    (h : Function.Surjective (mkQ (I • ⊤) ∘ₗ f)) {x : M} {y : N} {n : ℕ}
+    (hxy : f x ≡ y [SMOD (I ^ n • ⊤ : Submodule R N)]) :
+    ∃ x' : M, x ≡ x' [SMOD (I ^ n • ⊤ : Submodule R M)] ∧
+    f x' ≡ y [SMOD (I ^ (n + 1) • ⊤ : Submodule R N)] := by
+  obtain ⟨z, hz, hz'⟩ :=
+    exists_smodEq_pow_add_one_smul h (y := y - f x) (SModEq.sub_mem.mp hxy.symm)
+  use x + z
+  constructor
+  · simpa [SModEq.sub_mem]
+  · simpa [SModEq.sub_mem, sub_sub_eq_add_sub, add_comm] using hz'
+
+theorem exists_smodEq_pow_smul_top_and_mkQ_eq {f : M →ₗ[R] N}
+    (h : Function.Surjective (mkQ (I • ⊤) ∘ₗ f)) {x : M} {n : ℕ}
+    {y : N ⧸ (I ^ n • ⊤ : Submodule R N)} {y' : N ⧸ (I ^ (n + 1) • ⊤ : Submodule R N)}
+    (hyy' : factor (pow_smul_top_le I N n.le_succ) y' = y) (hxy : mkQ _ (f x) = y) :
+    ∃ x' : M, x ≡ x' [SMOD (I ^ n • ⊤ : Submodule R M)] ∧ mkQ _ (f x') = y' := by
+  obtain ⟨y0, hy0⟩ := mkQ_surjective _ y'
+  have : f x ≡ y0 [SMOD (I ^ n • ⊤ : Submodule R N)] := by
+    rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
+        hy0, hyy', hxy]
+  obtain ⟨x', hxx', hx'y0⟩ :=
+    exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top h this
+  use x', hxx'
+  rwa [mkQ_apply, hx'y0]
+
+theorem map_surjective_of_mkQ_comp_surjective {f : M →ₗ[R] N}
+    (h : Function.Surjective (mkQ (I • ⊤) ∘ₗ f)) : Function.Surjective (map I f) := by
+  intro y
+  suffices h : ∃ x : ℕ → M, ∀ n, x n ≡ x (n + 1) [SMOD (I ^ n • ⊤ : Submodule R M)] ∧
+      Submodule.Quotient.mk (f (x n)) = eval I _ n y by
+    obtain ⟨x, hx⟩ := h
+    use AdicCompletion.mk I M ⟨x, fun h ↦
+        eq_factor_of_eq_factor_succ (fun _ _ ↦ pow_smul_top_le I M) _ (fun n ↦ (hx n).1) h⟩
+    ext n
+    simp [hx n]
+  let x : (n : ℕ) → {m : M // Submodule.Quotient.mk (f m) = eval I _ n y} := fun n ↦ by
+    induction n with
+    | zero =>
+      use 0
+      apply_fun (Submodule.Quotient.equiv (I ^ 0 • ⊤) ⊤ (.refl R N) (by simp)).toEquiv
+      exact Subsingleton.elim _ _
+    | succ n xn =>
+      choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
+          (y' := eval _ _ (n + 1) y) (by simp) xn.2
+      exact ⟨z, hz.2⟩
+  exact ⟨fun n ↦ (x n).val, fun n ↦ ⟨(Classical.choose_spec (exists_smodEq_pow_smul_top_and_mkQ_eq
+      h (y' := eval I _ (n + 1) y) (by simp) (x n).2)).1, (x n).property⟩⟩
+
 end AdicCompletion
+
+open AdicCompletion Submodule
+
+variable {I}
+
+theorem surjective_of_mkQ_comp_surjective [IsPrecomplete I M] [IsHausdorff I N]
+    {f : M →ₗ[R] N} (h : Function.Surjective (mkQ (I • ⊤) ∘ₗ f)) : Function.Surjective f := by
+  intro y
+  obtain ⟨x', hx'⟩ := AdicCompletion.map_surjective_of_mkQ_comp_surjective h (of I N y)
+  obtain ⟨x, hx⟩ := of_surjective I M x'
+  use x
+  rwa [← of_inj (I := I), ← map_of, hx]
+
+variable {S : Type*} [CommRing S] (f : R →+* S)
+
+theorem surjective_of_mk_map_comp_surjective [IsPrecomplete I R] [haus : IsHausdorff (I.map f) S]
+    (h : Function.Surjective ((Ideal.Quotient.mk (I.map f)).comp f)) :
+    Function.Surjective f := by
+  let _ := f.toAlgebra
+  let fₗ := (Algebra.ofId R S).toLinearMap
+  change Function.Surjective ((restrictScalars R (I.map f)).mkQ ∘ₗ fₗ) at h
+  have : I • ⊤ = restrictScalars R (Ideal.map f I) := by
+    simp only [Ideal.smul_top_eq_map, restrictScalars_inj]
+    rfl
+  have _ := IsHausdorff.map_algebraMap_iff.mp haus
+  apply surjective_of_mkQ_comp_surjective (I := I) (f := fₗ)
+  rwa [Ideal.smul_top_eq_map]

Mathlib/RingTheory/Perfection.lean

@@ -183,6 +183,28 @@ theorem coeff_iterate_frobeniusEquiv_symm (f : Ring.Perfection R p) (n m : ℕ)
   | succ m ih =>
     simp [ih, ← add_assoc]
 
+theorem coeff_surjective (h : Function.Surjective (frobenius R p)) (n : ℕ) :
+    Function.Surjective (Perfection.coeff R p n) := by
+  intro x
+  refine ⟨⟨fun m ↦ if h : n ≤ m then ?_ else x ^ p ^ (n - m), ?_⟩, ?_⟩
+  · induction h using Nat.leRec with
+    | refl =>
+      exact x
+    | le_succ_of_le hle xk =>
+      choose x hx using h xk
+      use x
+  · intro m
+    obtain (h1 | h1 | h1) : n ≤ m ∨ n = m + 1 ∨ ¬ n ≤ m + 1 := by cutsat
+    · have h1' : n ≤ m + 1 := by cutsat
+      simp only [h1', ↓reduceDIte, h1, Nat.leRec_succ, ← frobenius_def]
+      exact Classical.choose_spec (h _)
+    · subst h1
+      simp [← frobenius_def]
+    · have h1' : ¬ n ≤ m := by cutsat
+      have : n - m = (n - (m + 1)) + 1 := by cutsat
+      simp [h1, h1', this, pow_succ, pow_mul]
+  · simp
+
 variable (R p)
 
 /-- Given rings `R` and `S` of characteristic `p`, with `R` being perfect,

Mathlib/RingTheory/Perfectoid/FontaineTheta.lean

@@ -5,6 +5,7 @@ Authors: Jiedong Jiang
 -/
 module
 
+public import Mathlib.RingTheory.AdicCompletion.Functoriality
 public import Mathlib.RingTheory.AdicCompletion.RingHom
 public import Mathlib.RingTheory.Perfectoid.Untilt
 public import Mathlib.RingTheory.WittVector.TeichmullerSeries
@@ -16,9 +17,13 @@ homomorphism from the Witt vector `𝕎 R♭` of the tilt of a perfectoid ring `
 to `R` itself. Our definition of `θ` does not require that `R` is perfectoid in the first place.
 We only need `R` to be `p`-adically complete.
 
-## Main definitions
+## Main Definitions
 * `fontaineTheta` : Fontaine's θ map, which is a ring homomorphism from `𝕎 R♭` to `R`.
 
+## Main Theorems
+* `fontaineTheta_teichmuller` : `θ([x])` is the untilt of `x`.
+* `fontaineTheta_surjective` : Fontaine's θ map is surjective.
+
 ## TODO
 Establish that our definition (explicit construction of `θ mod p ^ n`) agrees with the
 deformation-theoretic approach via the cotangent complex, as in
@@ -182,3 +187,26 @@ theorem fontaineTheta_teichmuller (x : R♭) : fontaineTheta R p (teichmuller p
   · simp [SModEq, mk_pow_fontaineTheta]
 
 end WittVector
+
+variable [Fact ¬IsUnit (p : R)] [IsAdicComplete (span {(p : R)}) R]
+
+/-- If the Frobenius map is surjective on `R/pR`, then the Fontaine's θ map is surjective. -/
+theorem surjective_fontaineTheta (hF : Function.Surjective (frobenius (ModP R p) p)) :
+    Function.Surjective (fontaineTheta R p) := by
+  have : Ideal.map (fontaineTheta R p) (span {(p : 𝕎 R♭)}) = 𝔭 := by
+    simp [map_span]
+  have _ : IsHausdorff ((span {(p : 𝕎 R♭)}).map (fontaineTheta R p)) R := by
+    rw [this]
+    infer_instance
+  apply surjective_of_mk_map_comp_surjective (fontaineTheta R p) (I := span {(p : 𝕎 R♭)})
+  simp only [RingHom.coe_comp]
+  suffices h : Function.Surjective (Ideal.Quotient.mk 𝔭 ∘ fontaineTheta R p) by
+    rwa [Ideal.map_span, Set.image_singleton, map_natCast]
+  have : Ideal.Quotient.mk 𝔭 ∘ fontaineTheta R p = (fun x ↦
+      PreTilt.coeff 0 x) ∘ fun (x : 𝕎 R♭) ↦ (x.coeff 0) := by
+    ext
+    simp [mk_fontaineTheta]
+  rw [this]
+  apply Function.Surjective.comp
+  · exact Perfection.coeff_surjective hF 0
+  · exact WittVector.coeff_surjective 0

Mathlib/RingTheory/WittVector/Defs.lean

@@ -80,6 +80,10 @@ theorem ext {x y : 𝕎 R} (h : ∀ n, x.coeff n = y.coeff n) : x = y := by
   simp only at h
   simp [funext_iff, h]
 
+theorem coeff_surjective (n : ℕ) :
+    Function.Surjective (fun (x : 𝕎 R) ↦ x.coeff n) :=
+  fun x ↦ ⟨(mk p fun _ ↦ x), rfl⟩
+
 variable (p)
 
 @[simp]