CurveCoverTorsor.lean

theorem appLE_congr_hom {S N : Scheme.{u}} {g g' : S ⟶ N}
    (hgg : g = g') (W : N.Opens) (V : S.Opens)
    (hg : V ≤ g ⁻¹ᵁ W) (hg' : V ≤ g' ⁻¹ᵁ W) :
    g.appLE W V hg = g'.appLE W V hg'

theorem app_of_appLE {S N : Scheme.{u}} (f : S ⟶ N)
    (W : N.Opens) (hf : f ⁻¹ᵁ W = ⊤) (s : Γ(N, W)) :
    f.app W s = S.presheaf.map (homOfLE le_top).op (f.appLE W ⊤ hf.ge s)

theorem appLE_of_app {S N : Scheme.{u}} (f : S ⟶ N)
    (W : N.Opens) (hf : f ⁻¹ᵁ W = ⊤) (s : Γ(N, W)) (t : Γ(S, ⊤))
    (hs : f.app W s = S.presheaf.map (homOfLE le_top).op t) :
    f.appLE W ⊤ hf.ge s = t

theorem point_preimage_top {Ω : Type u} [Field Ω]
    {X : Scheme.{u}} (ξ : Spec (.of Ω) ⟶ X) (V : X.Opens)
    (hξ : ξ default ∈ V) : ξ ⁻¹ᵁ V = ⊤

theorem appLE_baseScalar {K Ω : Type u} [Field K] [Field Ω]
    {X : Scheme.{u}} (c : X ⟶ Spec (.of K)) (ξ : Spec (.of Ω) ⟶ X)
    (V : X.Opens) (hξ : ξ ⁻¹ᵁ V = ⊤) (a : Γ(Spec (.of K), ⊤)) :
    ξ.appLE V ⊤ hξ.ge (c.appLE ⊤ V le_top a) = (ξ ≫ c).appTop a

theorem rootLift_preimage (hz : z ⁻¹ᵁ V = ⊤) (s : {s : Z ⟶ Y // s ≫ π = z}) :
    s.1 ⁻¹ᵁ (π ⁻¹ᵁ V) = ⊤

def rootLiftCoordinate (hz : z ⁻¹ᵁ V = ⊤) (T : Γ(Y, π ⁻¹ᵁ V))
    (s : {s : Z ⟶ Y // s ≫ π = z}) : Γ(Z, ⊤)

theorem rootLift_app_base (hz : z ⁻¹ᵁ V = ⊤) (v : Γ(X, V))
    (s : {s : Z ⟶ Y // s ≫ π = z}) :
    s.1.appLE (π ⁻¹ᵁ V) ⊤ (rootLift_preimage π V z hz s).ge (π.app V v) =
      z.appLE V ⊤ hz.ge v

theorem rootLiftCoordinate_pow (hz : z ⁻¹ᵁ V = ⊤)
    (T : Γ(Y, π ⁻¹ᵁ V)) (n : ℕ) (v : Γ(X, V))
    (hT : T ^ n = π.app V v) (s : {s : Z ⟶ Y // s ≫ π = z}) :
    rootLiftCoordinate π V z hz T s ^ n = z.appLE V ⊤ hz.ge v

theorem rootLiftCoordinate_comp (hz : z ⁻¹ᵁ V = ⊤)
    (T : Γ(Y, π ⁻¹ᵁ V)) (e : Y ⟶ Y) (he : e ≫ π = π)
    (hW : π ⁻¹ᵁ V ≤ e ⁻¹ᵁ (π ⁻¹ᵁ V)) (c : Γ(X, V))
    (hscale : e.appLE (π ⁻¹ᵁ V) (π ⁻¹ᵁ V) hW T = π.app V c * T)
    (s : {s : Z ⟶ Y // s ≫ π = z}) :
    rootLiftCoordinate π V z hz T
      ⟨s.1 ≫ e, (Category.assoc s.1 e π).trans ((congrArg (s.1 ≫ ·) he).trans s.2)⟩ =
      z.appLE V ⊤ hz.ge c * rootLiftCoordinate π V z hz T s

theorem rootLiftCoordinate_injective (hz : z ⁻¹ᵁ V = ⊤)
    (T : Γ(Y, π ⁻¹ᵁ V)) (n : ℕ) (v : Γ(X, V))
    (hT : T ^ n = π.app V v)
    (hlift : ∀ τ : Γ(Z, ⊤), Z.presheaf.map (homOfLE le_top).op τ ^ n = z.app V v →
      ∃! s : Z ⟶ Y, s ≫ π = z ∧ s.app (π ⁻¹ᵁ V) T =
        Z.presheaf.map (homOfLE le_top).op τ) :
    Function.Injective (rootLiftCoordinate π V z hz T)

theorem exists_rootLiftCoordinate (hz : z ⁻¹ᵁ V = ⊤)
    (T : Γ(Y, π ⁻¹ᵁ V)) (n : ℕ) (v : Γ(X, V))
    (hlift : ∀ τ : Γ(Z, ⊤), Z.presheaf.map (homOfLE le_top).op τ ^ n = z.app V v →
      ∃! s : Z ⟶ Y, s ≫ π = z ∧ s.app (π ⁻¹ᵁ V) T =
        Z.presheaf.map (homOfLE le_top).op τ)
    (τ : Γ(Z, ⊤)) (hτ : τ ^ n = z.appLE V ⊤ hz.ge v) :
    ∃ s : {s : Z ⟶ Y // s ≫ π = z}, rootLiftCoordinate π V z hz T s = τ

def fiberLiftEquiv {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ S) (W : FiniteEtale S) :
    (FiniteEtale.fiber ξ).obj W ≃ {s : Spec (.of Ω) ⟶ W.left // s ≫ W.hom = ξ}

theorem fiberLiftEquiv_naturality
    {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ S) {W W' : FiniteEtale S} (f : W ⟶ W')
    (x : (FiniteEtale.fiber ξ).obj W) :
    (fiberLiftEquiv ξ W' ((FiniteEtale.fiber ξ).map f x)).1 =
      (fiberLiftEquiv ξ W x).1 ≫ f.left

def pointScalar {K Ω : Type u} [Field K] [Field Ω]
    {X : Scheme.{u}} (c : X ⟶ Spec (.of K)) (ξ : Spec (.of Ω) ⟶ X) : K →+* Ω

theorem exists_kummerFiberCoordinate :
    let := M.kummerGeometricRootAction n u hn ξ
    ∃ q : (FiniteEtale.fiber ξ).obj (M.kummerCover n hn u) → Ω,
      Function.Injective q ∧ (∀ x, q x ≠ 0) ∧
      (∀ x y, q x ^ (n : ℕ) = q y ^ (n : ℕ)) ∧
      ∀ (ζ : rootsOfUnity (n : ℕ) K) x,
        q (ζ • x) = pointScalar M.toBase ξ ((ζ : Kˣ) : K) * q x := by
  let := M.kummerGeometricRootAction n u hn ξ
  let f := M.kummerGenericMap n u
  let π := f.fromNormalization
  let W := M.kummerCover n hn u
  obtain ⟨V, _hV, hxV, h, _hh, v, hv, T, hTpow, hTgen, hlift⟩ :=
    M.exists_kummer_root_chart n u hn (ξ default)
  have : Nonempty V := ⟨⟨ξ default, hxV⟩⟩
  have hξ : ξ ⁻¹ᵁ V = ⊤ := point_preimage_top ξ V hxV
  let l := fiberLiftEquiv ξ W
  let c : {s : Spec (.of Ω) ⟶ f.normalization // s ≫ π = ξ} → Γ(Spec (.of Ω), ⊤) :=
    rootLiftCoordinate π V ξ hξ T
  let q : (FiniteEtale.fiber ξ).obj W → Ω :=
    fun x => (Scheme.ΓSpecIso (.of Ω)).hom (c (l x))
  have hpow (x : (FiniteEtale.fiber ξ).obj W) :
      q x ^ (n : ℕ) = (Scheme.ΓSpecIso (.of Ω)).hom (ξ.appLE V ⊤ hξ.ge v) := by
    change ((Scheme.ΓSpecIso (.of Ω)).hom (c (l x))) ^ (n : ℕ) = _
    rw [← map_pow]
    exact congrArg (Scheme.ΓSpecIso (.of Ω)).hom
      (rootLiftCoordinate_pow π V ξ hξ T (n : ℕ) v hTpow (l x))
  have hvΩ : IsUnit ((Scheme.ΓSpecIso (.of Ω)).hom (ξ.appLE V ⊤ hξ.ge v)) :=
    (hv.map (ξ.appLE V ⊤ hξ.ge).hom).map (Scheme.ΓSpecIso (.of Ω)).hom.hom
  refine ⟨q, ?_, ?_, ?_, ?_⟩
  · intro x y hxy
    apply l.injective
    apply rootLiftCoordinate_injective π V ξ hξ T (n : ℕ) v hTpow (hlift _ ξ hξ)
    exact (Scheme.ΓSpecIso (.of Ω)).commRingCatIsoToRingEquiv.injective hxy
  · intro x hx
    apply hvΩ.ne_zero
    rw [← hpow x, hx, zero_pow n.ne_zero]
  · intro x y
    exact (hpow x).trans (hpow y).symm
  · intro ζ x
    let e := M.kummerNormalizationRootScale n u ζ
    have he : e.hom ≫ π = π :=
      EtaleFundamentalGroups.Inertia.normalizationSourceIso_hom_fromNormalization _ _ _ _
    have hpre : π ⁻¹ᵁ V ≤ e.hom ⁻¹ᵁ (π ⁻¹ᵁ V) := by
      rw [← Scheme.Hom.comp_preimage, he]
    have hscale := M.kummerNormalizationRootScale_localRoot n u V h T hTgen ζ
    have hcoord := rootLiftCoordinate_comp π V ξ hξ T e.hom he hpre
      (M.toBase.appLE ⊤ V le_top ((Scheme.ΓSpecIso (.of K)).inv ((ζ : Kˣ) : K)))
      hscale (l x)
    have hl : l (ζ • x) =
        ⟨(l x).1 ≫ e.hom,
          (Category.assoc _ _ _).trans ((congrArg ((l x).1 ≫ ·) he).trans (l x).2)⟩ := by
      apply Subtype.ext
      exact fiberLiftEquiv_naturality ξ (M.kummerCoverRootScale n u hn ζ).hom x
    change (Scheme.ΓSpecIso (.of Ω)).hom (c (l (ζ • x))) = _
    rw [hl]
    change (Scheme.ΓSpecIso (.of Ω)).hom
      (rootLiftCoordinate π V ξ hξ T _) = _
    apply (congrArg (Scheme.ΓSpecIso (.of Ω)).hom hcoord).trans
    apply (map_mul (Scheme.ΓSpecIso (.of Ω)).hom.hom _ _).trans
    exact congrArg (fun a : Γ(Spec (.of Ω), ⊤) =>
      (Scheme.ΓSpecIso (.of Ω)).hom a * q x)
      (appLE_baseScalar M.toBase ξ V hξ ((Scheme.ΓSpecIso (.of K)).inv ((ζ : Kˣ) : K)))

theorem kummerGeometricFiber_nonempty :
    Nonempty ((FiniteEtale.fiber ξ).obj (M.kummerCover n hn u))

theorem kummerGeometricRootAction_existsUnique [IsSepClosed K]
    (x y : (FiniteEtale.fiber ξ).obj (M.kummerCover n hn u)) :
    let := M.kummerGeometricRootAction n u hn ξ
    ∃! ζ : rootsOfUnity (n : ℕ) K, ζ • x = y := by
  let := M.kummerGeometricRootAction n u hn ξ
  obtain ⟨q, hqinj, hqzero, hqpow, hqscale⟩ := M.exists_kummerFiberCoordinate n u hn ξ
  obtain ⟨ζ, hζ, huniq⟩ := EtaleFundamentalGroups.Kummer.existsUnique_rootScale
    (pointScalar M.toBase ξ) n hn (q x) (q y) (hqzero x) (hqpow x y)
  refine ⟨ζ, hqinj ((hqscale ζ x).trans hζ), ?_⟩
  intro η hη
  apply huniq η
  exact (hqscale η x).symm.trans (congrArg q hη)

def kummerGeometricRootTorsor [IsSepClosed K] :
    Torsor (rootsOfUnity (n : ℕ) K)
      ((FiniteEtale.fiber ξ).obj (M.kummerCover n hn u))