RootCompletionBaseChange.lean

theorem localizationAtPrime_maximalIdeal_eq_span_of_eq_span
    {R : Type uV} [CommRing R]
    (q : Ideal R) [q.IsPrime] (pi : R)
    (hq : q = Ideal.span ({pi} : Set R)) :
    IsLocalRing.maximalIdeal (Localization.AtPrime q) =
      Ideal.span
        ({algebraMap R (Localization.AtPrime q) pi} :
          Set (Localization.AtPrime q))

def standardDVRCompletionValuationSubringElement
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (x : V) : standardDVFCompletionValuationSubring V K

theorem standardDVRCompletionValuationSubringElement_isUniformizer
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (pi : V)
    (hpi : IsLocalRing.maximalIdeal V = Ideal.span ({pi} : Set V)) :
    let H := standardDVFCompletionCompleteDVF V K
    H.valuation.IsUniformizer
      (standardDVRCompletionValuationSubringElement V K pi :
        standardDVFCompletionField V K) := by
  dsimp only
  let H := standardDVFCompletionCompleteDVF V K
  let Vhat := H.valuationSubring
  let : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  let piHat : Vhat :=
    standardDVRCompletionValuationSubringElement V K pi
  have hspan : H.maximalIdeal = Ideal.span ({piHat} : Set Vhat) := by
    calc
      H.maximalIdeal =
          Ideal.map (algebraMap V Vhat) (IsLocalRing.maximalIdeal V) :=
        (standardDVRToCompletion_maximalIdeal_map_eq V K).symm
      _ = Ideal.map (algebraMap V Vhat) (Ideal.span ({pi} : Set V)) := by
        rw [hpi]
      _ = Ideal.span ({piHat} : Set Vhat) := by
        rw [Ideal.map_span, Set.image_singleton]
  exact Valuation.isUniformizer_of_maximalIdeal_eq_span H.valuation hspan

theorem
    exists_heightOneLocalizationElement_with_completed_uniformizer
    {D : Type uV} [CommRing D] [IsDomain D] [IsRegularLocalRing D]
    (hdim : ringKrullDim D = ((2 : ℕ∞) : WithBot ℕ∞))
    (q : Ideal D) [q.IsPrime] (hqHeight : q.height = 1) :
    let V := Localization.AtPrime q
    ∃ hV : IsDiscreteValuationRing V,
      letI : IsDiscreteValuationRing V := hV
      let K := FractionRing V
      ∃ pi : V,
        (standardDVFCompletionCompleteDVF V K).valuation.IsUniformizer
          (standardDVRCompletionValuationSubringElement V K pi :
            standardDVFCompletionField V K) := by
  dsimp only
  let V := Localization.AtPrime q
  let hV : IsDiscreteValuationRing V :=
    (open _root_.EtaleFundamentalGroups in
      isDiscreteValuationRing_localizationAtPrime_of_isRegularLocalRing_dimension_two
        hdim q hqHeight)
  refine ⟨hV, ?_⟩
  let : IsDiscreteValuationRing V := hV
  let K := FractionRing V
  obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible V
  refine ⟨pi, ?_⟩
  exact standardDVRCompletionValuationSubringElement_isUniformizer
    V K pi ((IsDiscreteValuationRing.irreducible_iff_uniformizer pi).mp hpi)

def standardDVRRootCompletionAlgEquiv
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (N : ℕ) (pi : V) :
    let Vhat := standardDVFCompletionValuationSubring V K
    letI : Algebra V Vhat :=
      standardDVFCompletionValuationSubringAlgebra V K
    Vhat ⊗[V] AdjoinRoot (X ^ N - C pi) ≃ₐ[Vhat]
      AdjoinRoot
        (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi)) := by
  dsimp only
  let Vhat := standardDVFCompletionValuationSubring V K
  letI : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  let p : V[X] := X ^ N - C pi
  let pHat : Vhat[X] :=
    X ^ N - C (standardDVRCompletionValuationSubringElement V K pi)
  exact (adjoinRootBaseChangeAlgEquiv p).trans
    (AdjoinRoot.algEquivOfEq Vhat _ _ (by
      simp [p, standardDVRCompletionValuationSubringElement]))

theorem standardDVRRootCompletionAlgEquiv_tmul_root
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (N : ℕ) (pi : V) :
    let Vhat := standardDVFCompletionValuationSubring V K
    letI : Algebra V Vhat :=
      standardDVFCompletionValuationSubringAlgebra V K
    standardDVRRootCompletionAlgEquiv V K N pi
        (1 ⊗ₜ[V] AdjoinRoot.root (X ^ N - C pi)) =
      AdjoinRoot.root
        (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi)) := by
  dsimp only
  let Vhat := standardDVFCompletionValuationSubring V K
  let : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  let p : V[X] := X ^ N - C pi
  let pHat : Vhat[X] :=
    X ^ N - C (standardDVRCompletionValuationSubringElement V K pi)
  change ((adjoinRootBaseChangeAlgEquiv p).trans
      (AdjoinRoot.algEquivOfEq Vhat _ _ _))
        (1 ⊗ₜ[V] AdjoinRoot.root p) = AdjoinRoot.root pHat
  rw [AlgEquiv.trans_apply, adjoinRootBaseChangeAlgEquiv_tmul_root,
    AdjoinRoot.algEquivOfEq_root]

def standardDVRRootCompletionAlgebra
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (N : ℕ) (pi : V) :
    let Vhat := standardDVFCompletionValuationSubring V K
    letI : Algebra V Vhat :=
      standardDVFCompletionValuationSubringAlgebra V K
    Algebra (AdjoinRoot (X ^ N - C pi))
      (AdjoinRoot
        (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))) := by
  dsimp only
  let Vhat := standardDVFCompletionValuationSubring V K
  let Rn := AdjoinRoot (X ^ N - C pi)
  let Rhat := AdjoinRoot
    (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))
  letI : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  exact
    ((standardDVRRootCompletionAlgEquiv V K N pi).toRingHom.comp
      (Algebra.TensorProduct.includeRight : Rn →ₐ[V] Vhat ⊗[V] Rn).toRingHom).toAlgebra

def standardDVRRootCompletionAlgEquivOverRoot
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (N : ℕ) (pi : V) :
    let Vhat := standardDVFCompletionValuationSubring V K
    let Rn := AdjoinRoot (X ^ N - C pi)
    let Rhat := AdjoinRoot
      (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))
    letI : Algebra V Vhat :=
      standardDVFCompletionValuationSubringAlgebra V K
    letI : Algebra Rn (Vhat ⊗[V] Rn) :=
      Algebra.TensorProduct.rightAlgebra
    letI : Algebra Rn Rhat :=
      standardDVRRootCompletionAlgebra V K N pi
    (Vhat ⊗[V] Rn) ≃ₐ[Rn] Rhat := by
  dsimp only
  let Vhat := standardDVFCompletionValuationSubring V K
  let Rn := AdjoinRoot (X ^ N - C pi)
  let Rhat := AdjoinRoot
    (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))
  letI : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  letI : Algebra Rn (Vhat ⊗[V] Rn) :=
    Algebra.TensorProduct.rightAlgebra
  letI : Algebra Rn Rhat :=
    standardDVRRootCompletionAlgebra V K N pi
  exact AlgEquiv.ofRingEquiv (R := Rn)
    (f := (standardDVRRootCompletionAlgEquiv V K N pi).toRingEquiv)
    (fun _ ↦ rfl)

theorem standardDVRRootCompletionAlgebra_map_root
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (N : ℕ) (pi : V) :
    let Vhat := standardDVFCompletionValuationSubring V K
    let Rn := AdjoinRoot (X ^ N - C pi)
    let Rhat := AdjoinRoot
      (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))
    letI : Algebra V Vhat :=
      standardDVFCompletionValuationSubringAlgebra V K
    letI : Algebra Rn Rhat :=
      standardDVRRootCompletionAlgebra V K N pi
    algebraMap Rn Rhat (AdjoinRoot.root (X ^ N - C pi)) =
      AdjoinRoot.root
        (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi)) := by
  dsimp only
  let Vhat := standardDVFCompletionValuationSubring V K
  let Rn := AdjoinRoot (X ^ N - C pi)
  let Rhat := AdjoinRoot
    (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))
  let : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  let : Algebra Rn Rhat :=
    standardDVRRootCompletionAlgebra V K N pi
  change standardDVRRootCompletionAlgEquiv V K N pi
      (1 ⊗ₜ[V] AdjoinRoot.root (X ^ N - C pi)) = _
  exact standardDVRRootCompletionAlgEquiv_tmul_root V K N pi

theorem standardDVRRootCompletion_faithfullyFlat
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (N : ℕ) (pi : V) :
    let Vhat := standardDVFCompletionValuationSubring V K
    let Rn := AdjoinRoot (X ^ N - C pi)
    let Rhat := AdjoinRoot
      (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))
    letI : Algebra V Vhat :=
      standardDVFCompletionValuationSubringAlgebra V K
    letI : Algebra Rn Rhat :=
      standardDVRRootCompletionAlgebra V K N pi
    Module.FaithfullyFlat Rn Rhat := by
  dsimp only
  let Vhat := standardDVFCompletionValuationSubring V K
  let Rn := AdjoinRoot (X ^ N - C pi)
  let Rhat := AdjoinRoot
    (X ^ N - C (standardDVRCompletionValuationSubringElement V K pi))
  let : Algebra V Vhat :=
    standardDVFCompletionValuationSubringAlgebra V K
  let T := Vhat ⊗[V] Rn
  let T' := Rn ⊗[V] Vhat
  let : Module.FaithfullyFlat V Vhat :=
    standardDVRCompletionValuationSubring_faithfullyFlat
      (V := V) (K := K)
  let : Algebra Rn T := Algebra.TensorProduct.rightAlgebra
  let : Algebra Rn Rhat :=
    standardDVRRootCompletionAlgebra V K N pi
  let : Module.FaithfullyFlat Rn T' := inferInstance
  let eComm : T ≃ₐ[Rn] T' :=
    AlgEquiv.ofRingEquiv (R := Rn)
      (f := (Algebra.TensorProduct.comm V Vhat Rn).toRingEquiv)
      (fun _ ↦ rfl)
  let : Module.FaithfullyFlat Rn T :=
    Module.FaithfullyFlat.of_linearEquiv
      (R := Rn) (M := T') eComm.toLinearEquiv
  let eRoot : T ≃ₐ[Rn] Rhat :=
    standardDVRRootCompletionAlgEquivOverRoot V K N pi
  exact Module.FaithfullyFlat.of_linearEquiv
    (R := Rn) (M := T) eRoot.symm.toLinearEquiv