OpenCurveCoverLocalAction.lean

theorem appLE_commutation {S N : Scheme.{u}}
    (f : S ⟶ N) (eS : S ⟶ S) (eN : N ⟶ N) (hc : f ≫ eN = eS ≫ f)
    (W : N.Opens) (hW : W ≤ eN ⁻¹ᵁ W) (hf : ⊤ ≤ f ⁻¹ᵁ W) :
    eN.appLE W W hW ≫ f.appLE W ⊤ hf =
      f.appLE W ⊤ hf ≫ eS.appTop

theorem appLE_injective_of_preimage_top {S N : Scheme.{u}} (f : S ⟶ N)
    [IsSchemeTheoreticallyDominant f] [QuasiCompact f]
    (W : N.Opens) (hf : f ⁻¹ᵁ W = ⊤) :
    Function.Injective (f.appLE W ⊤ hf.ge)

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 section_map_eq_of_generic {S N : Scheme.{u}}
    (f : S ⟶ N) [IsSchemeTheoreticallyDominant f] [QuasiCompact f]
    (eS : S ⟶ S) (eN : N ⟶ N) (hc : f ≫ eN = eS ≫ f)
    (W : N.Opens) (hW : W ≤ eN ⁻¹ᵁ W) (hf : f ⁻¹ᵁ W = ⊤)
    (s t : Γ(N, W)) (ρ : Γ(S, ⊤))
    (hs : f.appLE W ⊤ hf.ge s = ρ)
    (ht : f.appLE W ⊤ hf.ge t = eS.appTop ρ) :
    eN.appLE W W hW s = t

theorem hasValue_baseScalar (V : X.Opens) (a : K) :
    HasValue V
      ((j ≫ M.toBase).appLE ⊤ V le_top ((Scheme.ΓSpecIso (.of K)).inv a))
      (baseToFunctionField (j ≫ M.toBase) a)

theorem genericRootScale_appTop (ζ : rootsOfUnity (n : ℕ) K)
    (a : AdjoinRoot (Polynomial.X ^ (n : ℕ) -
      Polynomial.C (j.functionFieldMap hj (M.ffEquiv (w.val : F))) : Polynomial X.functionField)) :
    (Scheme.ΓSpecIso _).hom
      ((kummerGenericRootScale M S n w j hj ζ).hom.appTop ((Scheme.ΓSpecIso _).inv a)) =
        kummerRootScale (n : ℕ) (j.functionFieldMap hj (M.ffEquiv (w.val : F)))
          (restrictRootsOfUnity (baseToFunctionField (j ≫ M.toBase)) (n : ℕ) ζ) a

theorem genericRootScale_rootSection (ζ : rootsOfUnity (n : ℕ) K)
    (h : X.functionField) :
    let A := AdjoinRoot (Polynomial.X ^ (n : ℕ) -
      Polynomial.C (j.functionFieldMap hj (M.ffEquiv (w.val : F))) : Polynomial X.functionField)
    (kummerGenericRootScale M S n w j hj ζ).hom.appTop
        ((Scheme.ΓSpecIso (.of A)).inv
          (algebraMap X.functionField A h⁻¹ * AdjoinRoot.root _)) =
      (Scheme.ΓSpecIso (.of A)).inv
        (algebraMap X.functionField A (baseToFunctionField (j ≫ M.toBase) ((ζ : Kˣ) : K)) *
          (algebraMap X.functionField A h⁻¹ * AdjoinRoot.root _)) := by
  intro A
  apply (Scheme.ΓSpecIso (.of A)).commRingCatIsoToRingEquiv.injective
  change (Scheme.ΓSpecIso (.of A)).hom
      ((kummerGenericRootScale M S n w j hj ζ).hom.appTop
        ((Scheme.ΓSpecIso (.of A)).inv
          (algebraMap X.functionField A h⁻¹ * AdjoinRoot.root _))) =
    (Scheme.ΓSpecIso (.of A)).hom ((Scheme.ΓSpecIso (.of A)).inv
      (algebraMap X.functionField A (baseToFunctionField (j ≫ M.toBase) ((ζ : Kˣ) : K)) *
        (algebraMap X.functionField A h⁻¹ * AdjoinRoot.root _)))
  rw [genericRootScale_appTop, Iso.inv_hom_id_apply, map_mul,
    AlgHom.commutes, kummerRootScale_root]
  exact (mul_left_comm _ _ _).symm

theorem kummerNormalizationRootScale_localRoot
    (V : X.Opens) [Nonempty V]
    (h : X.functionField)
    (T : Γ((M.openKummerGenericMap S n w j hj).normalization,
      (M.openKummerGenericMap S n w j hj).fromNormalization ⁻¹ᵁ V))
    (hT : (M.openKummerGenericMap S n w j hj).toNormalization.app
      ((M.openKummerGenericMap S n w j hj).fromNormalization ⁻¹ᵁ V) T =
        (Spec (.of (AdjoinRoot (Polynomial.X ^ (n : ℕ) -
          Polynomial.C (j.functionFieldMap hj (M.ffEquiv (w.val : F))) : Polynomial
              X.functionField)))).presheaf.map
          (homOfLE le_top).op ((Scheme.ΓSpecIso _).inv
            (algebraMap X.functionField _ h⁻¹ * AdjoinRoot.root _)))
    (ζ : rootsOfUnity (n : ℕ) K) :
    let f := M.openKummerGenericMap S n w j hj
    let e := kummerNormalizationRootScale M S n w j hj ζ
    let W := f.fromNormalization ⁻¹ᵁ V
    let hW : W ≤ e.hom ⁻¹ᵁ W := by
      change f.fromNormalization ⁻¹ᵁ V ≤ e.hom ⁻¹ᵁ (f.fromNormalization ⁻¹ᵁ V)
      have hover : e.hom ≫ f.fromNormalization = f.fromNormalization :=
        EtaleFundamentalGroups.Inertia.normalizationSourceIso_hom_fromNormalization _ _ _ _
      rw [← Scheme.Hom.comp_preimage, hover]
    e.hom.appLE W W hW T = f.fromNormalization.app V
      ((j ≫ M.toBase).appLE ⊤ V le_top ((Scheme.ΓSpecIso (.of K)).inv ((ζ : Kˣ) : K))) * T := by
  intro f e W hW
  let A := AdjoinRoot (Polynomial.X ^ (n : ℕ) -
    Polynomial.C (j.functionFieldMap hj (M.ffEquiv (w.val : F))) : Polynomial X.functionField)
  let c : Γ(X, V) :=
    (j ≫ M.toBase).appLE ⊤ V le_top ((Scheme.ΓSpecIso (.of K)).inv ((ζ : Kˣ) : K))
  let q : X.functionField := baseToFunctionField (j ≫ M.toBase) ((ζ : Kˣ) : K)
  let ρ : A := algebraMap X.functionField A h⁻¹ * AdjoinRoot.root _
  have hf : f.toNormalization ⁻¹ᵁ W = ⊤ := by
    change f.toNormalization ⁻¹ᵁ (f.fromNormalization ⁻¹ᵁ V) = ⊤
    rw [← Scheme.Hom.comp_preimage, Scheme.Hom.toNormalization_fromNormalization]
    exact preimage_eq_top (CommRingCat.ofHom (algebraMap X.functionField A)) V
  have : IsSchemeTheoreticallyDominant f.toNormalization := ⟨f.ker_toNormalization⟩
  have hs : f.toNormalization.appLE W ⊤ hf.ge T = (Scheme.ΓSpecIso (.of A)).inv ρ :=
    appLE_of_app f.toNormalization W hf T _ hT
  have hcval : HasValue V c q := hasValue_baseScalar M j V ((ζ : Kˣ) : K)
  have hfV : f ⁻¹ᵁ V = ⊤ :=
    preimage_eq_top (CommRingCat.ofHom (algebraMap X.functionField A)) V
  have hcapp : f.app V c = (Spec (.of A)).presheaf.map (homOfLE le_top).op
      ((Scheme.ΓSpecIso (.of A)).inv (algebraMap X.functionField A q)) := by
    have happ := ConcreteCategory.congr_hom
      (app_eq (CommRingCat.ofHom (algebraMap X.functionField A)) V) c
    change f.app V c = (Spec (.of A)).presheaf.map (homOfLE le_top).op
      ((Scheme.ΓSpecIso (.of A)).inv
        (algebraMap X.functionField A (X.germToFunctionField V c))) at happ
    exact happ.trans (congrArg (fun r => (Spec (.of A)).presheaf.map (homOfLE le_top).op
      ((Scheme.ΓSpecIso (.of A)).inv (algebraMap X.functionField A r)))
        hcval.germToFunctionField_eq)
  have hcgeneric : f.appLE V ⊤ hfV.ge c =
      (Scheme.ΓSpecIso (.of A)).inv (algebraMap X.functionField A q) :=
    appLE_of_app f V hfV c _ hcapp
  have hcomp := Scheme.Hom.appLE_comp_appLE f.toNormalization f.fromNormalization
    V W ⊤ le_rfl hf.ge
  have hmid {g g' : Spec (.of A) ⟶ X} (hgg : g = g')
      (hg : ⊤ ≤ g ⁻¹ᵁ V) (hg' : ⊤ ≤ g' ⁻¹ᵁ V) :
      g.appLE V ⊤ hg = g'.appLE V ⊤ hg' := by
    subst g'
    rfl
  have hcomp' : f.fromNormalization.app V ≫ f.toNormalization.appLE W ⊤ hf.ge =
      f.appLE V ⊤ hfV.ge :=
    (congrArg (fun m => m ≫ f.toNormalization.appLE W ⊤ hf.ge)
      f.fromNormalization.app_eq_appLE).trans
      (hcomp.trans (hmid f.toNormalization_fromNormalization _ _))
  have hcf : f.toNormalization.appLE W ⊤ hf.ge (f.fromNormalization.app V c) =
      (Scheme.ΓSpecIso (.of A)).inv (algebraMap X.functionField A q) :=
    (ConcreteCategory.congr_hom hcomp' c).trans hcgeneric
  apply section_map_eq_of_generic f.toNormalization
    (kummerGenericRootScale M S n w j hj ζ).hom e.hom
    (toNormalization_kummerNormalizationRootScale M S n w j hj ζ) W hW hf T
    (f.fromNormalization.app V c * T) ((Scheme.ΓSpecIso (.of A)).inv ρ) hs
  calc
    f.toNormalization.appLE W ⊤ hf.ge (f.fromNormalization.app V c * T) =
        f.toNormalization.appLE W ⊤ hf.ge (f.fromNormalization.app V c) *
          f.toNormalization.appLE W ⊤ hf.ge T := map_mul _ _ _
    _ = (Scheme.ΓSpecIso (.of A)).inv (algebraMap X.functionField A q) *
        (Scheme.ΓSpecIso (.of A)).inv ρ := congrArg₂ (· * ·) hcf hs
    _ = (Scheme.ΓSpecIso (.of A)).inv (algebraMap X.functionField A q * ρ) :=
      (map_mul (Scheme.ΓSpecIso (.of A)).inv.hom _ _).symm
    _ = (kummerGenericRootScale M S n w j hj ζ).hom.appTop
        ((Scheme.ΓSpecIso (.of A)).inv ρ) := (genericRootScale_rootSection M S n w j hj ζ h).symm