CompletionAdic.lean

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

abbrev standardDVFCompletionValuationSubringMaximalIdeal
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    Ideal (standardDVFCompletionValuationSubring V K)

def standardDVRToCompletionValuationSubringMap
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    V →+* (standardDVFCompletionCompleteDVF V K).valuationSubring

def standardDVFCompletionValuationSubringAlgebra
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    Algebra V (standardDVFCompletionCompleteDVF V K).valuationSubring

theorem coe_standardDVRToCompletionValuationSubringMap
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] (x : V) :
    ((standardDVRToCompletionValuationSubringMap V K x :
        (standardDVFCompletionCompleteDVF V K).valuationSubring) :
      standardDVFCompletionField V K) =
      standardDVFCompletionMap V K (algebraMap V K x)

theorem standardDVRToCompletion_maximalIdeal_map_eq
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    Ideal.map (algebraMap V target.valuationSubring)
        (IsLocalRing.maximalIdeal V) =
      target.maximalIdeal := by
  dsimp only
  let base := standardDVFOfDVR V K
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra K (standardDVFCompletionField V K) :=
    standardDVFCompletionAlgebra V K
  let : base.valuation.HasExtension target.valuation :=
    standardDVFCompletion_hasExtension V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  let e : V ≃+* base.valuationSubring :=
    IsDiscreteValuationRing.equivValuationSubring (A := V) (K := K)
  let g : base.valuationSubring →+* target.valuationSubring :=
    algebraMap base.valuationSubring target.valuationSubring
  calc
    Ideal.map (algebraMap V target.valuationSubring)
          (IsLocalRing.maximalIdeal V) =
        Ideal.map (g.comp e.toRingHom)
          (IsLocalRing.maximalIdeal V) := rfl
    _ = Ideal.map g
          (Ideal.map e.toRingHom (IsLocalRing.maximalIdeal V)) := by
      exact (Ideal.map_map e.toRingHom g).symm
    _ = Ideal.map g base.maximalIdeal :=
      congrArg (Ideal.map g)
        (IsLocalRing.map_ringEquiv_maximalIdeal e)
    _ = target.maximalIdeal :=
      standardDVFCompletion_maximalIdeal_map_eq V K

theorem standardDVRToCompletion_isLocalHom
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    IsLocalHom (algebraMap V target.valuationSubring) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  have hmax : Ideal.map (algebraMap V target.valuationSubring)
      (IsLocalRing.maximalIdeal V) = target.maximalIdeal :=
    standardDVRToCompletion_maximalIdeal_map_eq V K
  exact ((IsLocalRing.local_hom_TFAE
    (algebraMap V target.valuationSubring)).out 3 1).mp hmax.le

theorem standardDVRToCompletion_maximalIdeal_pow_comap
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] (n : ℕ) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    (target.maximalIdeal ^ n).comap
        (algebraMap V target.valuationSubring) =
      IsLocalRing.maximalIdeal V ^ n := by
  dsimp only
  let base := standardDVFOfDVR V K
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra K (standardDVFCompletionField V K) :=
    standardDVFCompletionAlgebra V K
  let : base.valuation.HasExtension target.valuation :=
    standardDVFCompletion_hasExtension V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  let : Module.FaithfullyFlat
      base.valuationSubring target.valuationSubring :=
    standardDVFCompletion_faithfullyFlat V K
  let e : V ≃+* base.valuationSubring :=
    IsDiscreteValuationRing.equivValuationSubring (A := V) (K := K)
  let g : base.valuationSubring →+* target.valuationSubring :=
    algebraMap base.valuationSubring target.valuationSubring
  have hmap : Ideal.map g base.maximalIdeal = target.maximalIdeal :=
    standardDVFCompletion_maximalIdeal_map_eq V K
  have hemap :
      Ideal.map e.toRingHom (IsLocalRing.maximalIdeal V) =
        base.maximalIdeal :=
    IsLocalRing.map_ringEquiv_maximalIdeal e
  calc
    (target.maximalIdeal ^ n).comap
          (algebraMap V target.valuationSubring) =
        ((Ideal.map g (base.maximalIdeal ^ n)).comap g).comap
          e.toRingHom := by
      rw [Ideal.comap_comap, Ideal.map_pow, hmap]
      rfl
    _ = (base.maximalIdeal ^ n).comap e.toRingHom := by
      rw [Ideal.comap_map_eq_self_of_faithfullyFlat]
    _ = IsLocalRing.maximalIdeal V ^ n := by
      rw [← hemap, ← Ideal.map_pow]
      ext x
      change e x ∈
          Ideal.map e.toRingHom (IsLocalRing.maximalIdeal V ^ n) ↔
        x ∈ IsLocalRing.maximalIdeal V ^ n
      exact Ideal.apply_mem_of_equiv_iff

theorem standardDVRToCompletion_exists_approx_mod_maximalIdeal_pow
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (n : ℕ)
    (y : (standardDVFCompletionCompleteDVF V K).valuationSubring) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    ∃ x : V,
      algebraMap V target.valuationSubring x - y ∈
        target.maximalIdeal ^ n := by
  dsimp only
  let v := (IsDiscreteValuationRing.maximalIdeal V).valuation K
  let base := standardDVFOfDVR V K
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra K (standardDVFCompletionField V K) :=
    standardDVFCompletionAlgebra V K
  let : base.valuation.HasExtension target.valuation :=
    standardDVFCompletion_hasExtension V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  let e : V ≃+* base.valuationSubring :=
    IsDiscreteValuationRing.equivValuationSubring (A := V) (K := K)
  rcases base.exists_uniformizer with ⟨pi, hpi⟩
  let piHat : target.valuationSubring :=
    ValuedExtension.integerMap base target.toDVF pi
  have hpiHat : target.valuation.IsUniformizer
      (piHat : standardDVFCompletionField V K) := by
    change target.valuation.IsUniformizer
      (((ValuedExtension.integerMap base target.toDVF) pi :
        target.valuationSubring) : standardDVFCompletionField V K)
    rw [ValuedExtension.integerMap_apply,
      standardDVFCompletion_algebraMap_apply]
    exact standardDVFCompletionMap_isUniformizer V K pi hpi
  let radius : standardDVFCompletionField V K :=
    ((piHat ^ n : target.valuationSubring) :
      standardDVFCompletionField V K)
  have hradius_ne :
      (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))) radius ≠ 0 := by
    rw [← standardDVFCompletionCompleteDVF_valuation V K]
    change target.valuation
      ((piHat : standardDVFCompletionField V K) ^ n) ≠ 0
    rw [map_pow]
    exact pow_ne_zero n hpiHat.val_ne_zero
  have hrestrict_radius_ne :
      (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))).restrict radius ≠ 0 := by
    simpa using hradius_ne
  let s : Set (standardDVFCompletionField V K) :=
    {z | (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ)))
        (z - (y : standardDVFCompletionField V K)) <
      (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))) radius}
  have hs : s ∈ nhds (y : standardDVFCompletionField V K) := by
    rw [Valued.mem_nhds]
    refine ⟨Units.mk0
      ((Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))).restrict radius)
      hrestrict_radius_ne, ?_⟩
    intro z hz
    change (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))).restrict
          (z - (y : standardDVFCompletionField V K)) <
        (Units.mk0
          ((Valued.v : Valuation (standardDVFCompletionField V K)
            (WithZero (Multiplicative ℤ))).restrict radius)
          hrestrict_radius_ne).1 at hz
    change (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ)))
          (z - (y : standardDVFCompletionField V K)) <
        (Valued.v : Valuation (standardDVFCompletionField V K)
          (WithZero (Multiplicative ℤ))) radius
    rw [Valuation.restrict_lt_iff_lt_embedding] at hz
    simpa using hz
  rcases UniformSpace.Completion.denseRange_coe.mem_nhds hs with
    ⟨a, ha⟩
  have ha_lt : (Valued.v : Valuation (standardDVFCompletionField V K)
      (WithZero (Multiplicative ℤ)))
      ((a : standardDVFCompletionField V K) -
        (y : standardDVFCompletionField V K)) <
      (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))) radius := ha
  have hradius_le_one :
      (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ))) radius ≤ 1 := by
    rw [← standardDVFCompletionCompleteDVF_valuation V K]
    change target.valuation
      ((piHat : standardDVFCompletionField V K) ^ n) ≤ 1
    rw [map_pow]
    exact pow_le_one₀ zero_le hpiHat.val_lt_one.le
  have ha_le : WithVal.valuation v a ≤ 1 := by
    have hy_le : (Valued.v : Valuation
        (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ)))
        (y : standardDVFCompletionField V K) ≤ 1 := by
      rw [← standardDVFCompletionCompleteDVF_valuation V K]
      exact y.2
    have hdiff_le_one : (Valued.v : Valuation
        (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ)))
        ((a : standardDVFCompletionField V K) -
          (y : standardDVFCompletionField V K)) ≤ 1 :=
      ha_lt.le.trans hradius_le_one
    have hsum_le : (Valued.v : Valuation
        (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ)))
        (a : standardDVFCompletionField V K) ≤ 1 := by
      calc
        (Valued.v : Valuation (standardDVFCompletionField V K)
            (WithZero (Multiplicative ℤ)))
              (a : standardDVFCompletionField V K) =
            (Valued.v : Valuation (standardDVFCompletionField V K)
              (WithZero (Multiplicative ℤ)))
              (((a : standardDVFCompletionField V K) -
                  (y : standardDVFCompletionField V K)) +
                (y : standardDVFCompletionField V K)) := by
          ring_nf
        _ ≤ max
              ((Valued.v : Valuation (standardDVFCompletionField V K)
                (WithZero (Multiplicative ℤ)))
                ((a : standardDVFCompletionField V K) -
                  (y : standardDVFCompletionField V K)))
              ((Valued.v : Valuation (standardDVFCompletionField V K)
                (WithZero (Multiplicative ℤ)))
                (y : standardDVFCompletionField V K)) :=
          (Valued.v : Valuation (standardDVFCompletionField V K)
            (WithZero (Multiplicative ℤ))).map_add _ _
        _ ≤ 1 := max_le hdiff_le_one hy_le
    have hva : (Valued.v : Valuation (standardDVFCompletionField V K)
        (WithZero (Multiplicative ℤ)))
        ((a : WithVal v) : standardDVFCompletionField V K) =
        WithVal.valuation v a := by
      exact Valued.valuedCompletion_apply (x := a)
    simpa only [hva] using hsum_le
  let xK : K := WithVal.equiv v a
  have hxK : v xK ≤ 1 := by
    change v (WithVal.equiv v a) ≤ 1
    simpa [WithVal.equiv_apply,
      WithVal.valuation_apply_eq_ofVal] using ha_le
  let xBase : base.valuationSubring := ⟨xK, hxK⟩
  let x : V := e.symm xBase
  have hmap :
      (((algebraMap V target.valuationSubring x :
          target.valuationSubring) :
        standardDVFCompletionField V K)) =
        (a : standardDVFCompletionField V K) := by
    change
      ((standardDVRToCompletionValuationSubringMap V K x :
          target.valuationSubring) : standardDVFCompletionField V K) =
        (a : standardDVFCompletionField V K)
    rw [coe_standardDVRToCompletionValuationSubringMap]
    change standardDVFCompletionMap V K
        (algebraMap V K (e.symm xBase)) =
      (a : standardDVFCompletionField V K)
    have hxBase : algebraMap V K (e.symm xBase) =
        (xBase : K) := by
      change (((e (e.symm xBase) : base.valuationSubring) : K)) =
        (xBase : K)
      rw [RingEquiv.apply_symm_apply]
    rw [hxBase]
    rfl
  refine ⟨x, ?_⟩
  rw [Valuation.mem_maximalIdeal_pow_iff_valuation_le_uniformizer_pow
    (val := target.valuation) (pi := piHat) (hpi := hpiHat) (n := n)]
  change target.valuation
      (((algebraMap V target.valuationSubring x :
          target.valuationSubring) : standardDVFCompletionField V K) -
        (y : standardDVFCompletionField V K)) ≤
    target.valuation
      ((piHat : standardDVFCompletionField V K) ^ n)
  rw [standardDVFCompletionCompleteDVF_valuation, hmap]
  exact ha_lt.le

def standardDVRCompletionPowQuotientAlgHom
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] (n : ℕ) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    (V ⧸ (IsLocalRing.maximalIdeal V ^ n)) →ₐ[V]
      (target.valuationSubring ⧸ (target.maximalIdeal ^ n)) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  letI : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  exact Ideal.quotientMapₐ (target.maximalIdeal ^ n)
    (Algebra.ofId V target.valuationSubring) (by
      change IsLocalRing.maximalIdeal V ^ n ≤
        (target.maximalIdeal ^ n).comap
          (algebraMap V target.valuationSubring)
      rw [standardDVRToCompletion_maximalIdeal_pow_comap V K n])

theorem standardDVRCompletionPowQuotientAlgHom_apply_mk
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (n : ℕ) (x : V) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    standardDVRCompletionPowQuotientAlgHom V K n
        (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V ^ n) x) =
      Ideal.Quotient.mk (target.maximalIdeal ^ n)
        (algebraMap V target.valuationSubring x) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  change (Ideal.quotientMapₐ (target.maximalIdeal ^ n)
      (Algebra.ofId V target.valuationSubring) _)
        (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V ^ n) x) =
    Ideal.Quotient.mk (target.maximalIdeal ^ n)
      (algebraMap V target.valuationSubring x)
  rw [Ideal.quotient_map_mkₐ]
  rfl

theorem standardDVRCompletionPowQuotientAlgHom_injective
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] (n : ℕ) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    Function.Injective (standardDVRCompletionPowQuotientAlgHom V K n) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  intro a b hab
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective a
  obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective b
  rw [standardDVRCompletionPowQuotientAlgHom_apply_mk,
    standardDVRCompletionPowQuotientAlgHom_apply_mk,
    Ideal.Quotient.eq] at hab
  rw [Ideal.Quotient.eq]
  have hab' : algebraMap V target.valuationSubring (x - y) ∈
      target.maximalIdeal ^ n := by
    simpa using hab
  have hab'' : x - y ∈ (target.maximalIdeal ^ n).comap
      (algebraMap V target.valuationSubring) := hab'
  rwa [standardDVRToCompletion_maximalIdeal_pow_comap V K n] at hab''

theorem standardDVRCompletionPowQuotientAlgHom_surjective
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] (n : ℕ) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    Function.Surjective (standardDVRCompletionPowQuotientAlgHom V K n) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  intro q
  induction q using Quotient.inductionOn' with
  | _ y =>
      rcases standardDVRToCompletion_exists_approx_mod_maximalIdeal_pow
        V K n y with ⟨x, hx⟩
      refine ⟨Ideal.Quotient.mk
        (IsLocalRing.maximalIdeal V ^ n) x, ?_⟩
      change standardDVRCompletionPowQuotientAlgHom V K n
          (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V ^ n) x) =
        Ideal.Quotient.mk (target.maximalIdeal ^ n) y
      rw [standardDVRCompletionPowQuotientAlgHom_apply_mk]
      exact Ideal.Quotient.eq.mpr hx

def standardDVRCompletionPowQuotientAlgEquiv
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] (n : ℕ) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    (V ⧸ (IsLocalRing.maximalIdeal V ^ n)) ≃ₐ[V]
      (target.valuationSubring ⧸ (target.maximalIdeal ^ n)) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  letI : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  exact AlgEquiv.ofBijective
    (standardDVRCompletionPowQuotientAlgHom V K n)
    ⟨standardDVRCompletionPowQuotientAlgHom_injective V K n,
      standardDVRCompletionPowQuotientAlgHom_surjective V K n⟩

theorem standardDVRCompletionPowQuotientAlgEquiv_apply_mk
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (n : ℕ) (x : V) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    standardDVRCompletionPowQuotientAlgEquiv V K n
        (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V ^ n) x) =
      Ideal.Quotient.mk (target.maximalIdeal ^ n)
        (algebraMap V target.valuationSubring x) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  change standardDVRCompletionPowQuotientAlgHom V K n
      (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V ^ n) x) =
    Ideal.Quotient.mk (target.maximalIdeal ^ n)
      (algebraMap V target.valuationSubring x)
  exact standardDVRCompletionPowQuotientAlgHom_apply_mk V K n x

theorem standardDVRCompletionPowQuotientAlgEquiv_factorPow
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    {m n : ℕ} (hmn : m ≤ n)
    (x : V ⧸ (IsLocalRing.maximalIdeal V ^ n)) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    Ideal.Quotient.factorPow target.maximalIdeal hmn
        (standardDVRCompletionPowQuotientAlgEquiv V K n x) =
      standardDVRCompletionPowQuotientAlgEquiv V K m
        (Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal V) hmn x) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  induction x using Quotient.inductionOn' with
  | _ x =>
      change Ideal.Quotient.factorPow target.maximalIdeal hmn
          (standardDVRCompletionPowQuotientAlgEquiv V K n
            (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V ^ n) x)) =
        standardDVRCompletionPowQuotientAlgEquiv V K m
          (Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal V) hmn
            (Ideal.Quotient.mk (IsLocalRing.maximalIdeal V ^ n) x))
      rw [standardDVRCompletionPowQuotientAlgEquiv_apply_mk,
        Ideal.Quotient.factor_mk, Ideal.Quotient.factor_mk,
        standardDVRCompletionPowQuotientAlgEquiv_apply_mk]

theorem standardDVRCompletionPowQuotientAlgEquiv_symm_factorPow
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    {m n : ℕ} (hmn : m ≤ n) :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    ∀ x : target.valuationSubring ⧸ (target.maximalIdeal ^ n),
      Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal V) hmn
          ((standardDVRCompletionPowQuotientAlgEquiv V K n).symm x) =
        (standardDVRCompletionPowQuotientAlgEquiv V K m).symm
          (Ideal.Quotient.factorPow target.maximalIdeal hmn x) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let : Algebra V target.valuationSubring :=
    standardDVFCompletionValuationSubringAlgebra V K
  intro x
  apply (standardDVRCompletionPowQuotientAlgEquiv V K m).injective
  rw [AlgEquiv.apply_symm_apply,
    ← standardDVRCompletionPowQuotientAlgEquiv_factorPow V K hmn
      ((standardDVRCompletionPowQuotientAlgEquiv V K n).symm x),
    AlgEquiv.apply_symm_apply]

instance completionValuationSubringAlgebra : Algebra V V_hat

theorem factorPow_evalₐ
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n) (x : AdicCompletion I R) :
    Ideal.Quotient.factorPow I hmn (AdicCompletion.evalₐ I n x) =
      AdicCompletion.evalₐ I m x

def completionToValuationSubringQuotientRingHom
    (n : ℕ) :
    AdicCompletion I_V V →+* V_hat ⧸ (I_hat ^ n)

theorem completionToValuationSubringQuotientRingHom_compatible :
    ∀ {m n : ℕ} (hmn : m ≤ n),
      (Ideal.Quotient.factorPow I_hat hmn).comp
          (completionToValuationSubringQuotientRingHom V K n) =
        completionToValuationSubringQuotientRingHom V K m

def completionToValuationSubringCompletionRingHom :
    AdicCompletion I_V V →+* AdicCompletion I_hat V_hat

theorem evalₐ_completionToValuationSubringCompletionRingHom
    (n : ℕ) (x : AdicCompletion I_V V) :
    AdicCompletion.evalₐ I_hat n
        (completionToValuationSubringCompletionRingHom V K x) =
      standardDVRCompletionPowQuotientAlgEquiv V K n
        (AdicCompletion.evalₐ I_V n x)

def valuationSubringCompletionToQuotientRingHom
    (n : ℕ) :
    AdicCompletion I_hat V_hat →+* V ⧸ (I_V ^ n)

theorem valuationSubringCompletionToQuotientRingHom_compatible :
    ∀ {m n : ℕ} (hmn : m ≤ n),
      (Ideal.Quotient.factorPow I_V hmn).comp
          (valuationSubringCompletionToQuotientRingHom V K n) =
        valuationSubringCompletionToQuotientRingHom V K m

def valuationSubringCompletionToCompletionRingHom :
    AdicCompletion I_hat V_hat →+* AdicCompletion I_V V

theorem evalₐ_valuationSubringCompletionToCompletionRingHom
    (n : ℕ) (x : AdicCompletion I_hat V_hat) :
    AdicCompletion.evalₐ I_V n
        (valuationSubringCompletionToCompletionRingHom V K x) =
      (standardDVRCompletionPowQuotientAlgEquiv V K n).symm
        (AdicCompletion.evalₐ I_hat n x)

theorem completionToValuationSubring_comp_fromValuationSubring :
    (completionToValuationSubringCompletionRingHom V K).comp
        (valuationSubringCompletionToCompletionRingHom V K) =
      RingHom.id (AdicCompletion I_hat V_hat)

theorem valuationSubringToCompletion_comp_fromCompletion :
    (valuationSubringCompletionToCompletionRingHom V K).comp
        (completionToValuationSubringCompletionRingHom V K) =
      RingHom.id (AdicCompletion I_V V)

def standardDVRAdicCompletionEquivValuationSubringCompletion :
    AdicCompletion I_V V ≃ₐ[V] AdicCompletion I_hat V_hat

theorem evalₐ_standardDVRAdicCompletionEquivValuationSubringCompletion
    (n : ℕ) (x : AdicCompletion I_V V) :
    AdicCompletion.evalₐ I_hat n
        (standardDVRAdicCompletionEquivValuationSubringCompletion V K x) =
      standardDVRCompletionPowQuotientAlgEquiv V K n
        (AdicCompletion.evalₐ I_V n x)

instance completionValuationSubringIsAdicComplete :
    IsAdicComplete I_hat V_hat

def valuationSubringCompletionEquivSelf :
    AdicCompletion I_hat V_hat ≃ₐ[V] V_hat

def standardDVRAdicCompletionEquivCompletionValuationSubring :
    AdicCompletion I_V V ≃ₐ[V] V_hat

theorem standardDVRAdicCompletionEquivCompletionValuationSubring_apply_of
    (x : V) :
    standardDVRAdicCompletionEquivCompletionValuationSubring V K
        (AdicCompletion.of I_V V x) =
      algebraMap V V_hat x

theorem standardDVRToCompletion_residueFieldMap_bijective :
    let target := standardDVFCompletionCompleteDVF V K
    letI : Algebra V target.valuationSubring :=
      standardDVFCompletionValuationSubringAlgebra V K
    letI : IsLocalHom (algebraMap V target.valuationSubring) :=
      standardDVRToCompletion_isLocalHom V K
    Function.Bijective
      (IsLocalRing.ResidueField.map
        (algebraMap V target.valuationSubring)) := by
  dsimp only
  let target := standardDVFCompletionCompleteDVF V K
  let T := target.valuationSubring
  let : Algebra V T :=
    standardDVFCompletionValuationSubringAlgebra V K
  let : IsLocalHom (algebraMap V T) :=
    standardDVRToCompletion_isLocalHom V K
  constructor
  · exact RingHom.injective _
  · intro z
    obtain ⟨y, rfl⟩ := IsLocalRing.residue_surjective z
    let e₀ := standardDVRCompletionPowQuotientAlgEquiv V K 1
    obtain ⟨x, hx⟩ := e₀.surjective
      (Ideal.Quotient.mk (target.maximalIdeal ^ 1) y)
    obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x
    refine ⟨IsLocalRing.residue V a, ?_⟩
    rw [IsLocalRing.ResidueField.map_residue]
    change Ideal.Quotient.mk target.maximalIdeal
        (algebraMap V T a) = Ideal.Quotient.mk target.maximalIdeal y
    have hx' : Ideal.Quotient.mk (target.maximalIdeal ^ 1)
          (algebraMap V T a) =
        Ideal.Quotient.mk (target.maximalIdeal ^ 1) y := by
      simpa only [e₀,
        standardDVRCompletionPowQuotientAlgEquiv_apply_mk] using hx
    exact Ideal.Quotient.eq.mpr <| by
      simpa only [pow_one] using Ideal.Quotient.eq.mp hx'

theorem quotient_mk_standardDVRAdicCompletionEquivCompletionValuationSubring
    (n : ℕ) (x : AdicCompletion I_V V) :
    Ideal.Quotient.mk (I_hat ^ n)
        (standardDVRAdicCompletionEquivCompletionValuationSubring V K x) =
      standardDVRCompletionPowQuotientAlgEquiv V K n
        (AdicCompletion.evalₐ I_V n x)