AlgebraicLocalization.lean

def valuationPreservingWithAbsRingEquiv
    (σ : L ≃ₐ[K] L) : WithAbs w.1 ≃+* WithAbs w.1

theorem valuationPreservingWithAbsRingEquiv_apply
    (σ : L ≃ₐ[K] L) (x : L) :
    WithAbs.equiv w.1
        (valuationPreservingWithAbsRingEquiv vK w σ
          ((WithAbs.equiv w.1).symm x)) = σ x

theorem valuationPreservingWithAbsRingEquiv_isometry
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x) :
    Isometry (valuationPreservingWithAbsRingEquiv vK w σ)

theorem valuationPreservingWithAbsRingEquiv_symm_isometry
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x) :
    Isometry (valuationPreservingWithAbsRingEquiv vK w σ).symm

def valuationPreservingCompletionRingEquiv
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x) :
    w.1.Completion ≃+* w.1.Completion

theorem valuationPreservingCompletionRingEquiv_toCompletion
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x) (x : L) :
    valuationPreservingCompletionRingEquiv vK w σ hσ
        (AbsoluteValue.toCompletion w.1 x) =
      AbsoluteValue.toCompletion w.1 (σ x)

theorem valuationPreservingCompletionRingEquiv_completionMap
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x)
    (x : vK.Completion) :
    valuationPreservingCompletionRingEquiv vK w σ hσ
        (AbsoluteValue.completionMap vK w.1 w.2 x) =
      AbsoluteValue.completionMap vK w.1 w.2 x

theorem valuationPreservingCompletionRingEquiv_mem_localization
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x)
    {z : w.1.Completion} (hz : z ∈ AbsoluteValue.algebraicLocalization vK w.1 w.2) :
    valuationPreservingCompletionRingEquiv vK w σ hσ z ∈
      AbsoluteValue.algebraicLocalization vK w.1 w.2

theorem valuationPreservingCompletionRingEquiv_symm_mem_localization
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x)
    {z : w.1.Completion} (hz : z ∈ AbsoluteValue.algebraicLocalization vK w.1 w.2) :
    (valuationPreservingCompletionRingEquiv vK w σ hσ).symm z ∈
      AbsoluteValue.algebraicLocalization vK w.1 w.2

def valuationPreservingLocalizationAlgEquiv
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
      AbsoluteValue.algebraicLocalization vK w.1 w.2 := by
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vK w.1 w.2
  let e := valuationPreservingCompletionRingEquiv vK w σ hσ
  exact
    { toFun := fun z =>
        ⟨e z, valuationPreservingCompletionRingEquiv_mem_localization
          vK w σ hσ z.property⟩
      invFun := fun z =>
        ⟨e.symm z,
          valuationPreservingCompletionRingEquiv_symm_mem_localization
            vK w σ hσ z.property⟩
      left_inv := fun z => by
        apply Subtype.ext
        exact e.symm_apply_apply z
      right_inv := fun z => by
        apply Subtype.ext
        exact e.apply_symm_apply z
      map_mul' := fun x y => by
        apply Subtype.ext
        exact e.map_mul x y
      map_add' := fun x y => by
        apply Subtype.ext
        exact e.map_add x y
      commutes' := fun x => by
        apply Subtype.ext
        exact valuationPreservingCompletionRingEquiv_completionMap
          vK w σ hσ x }

theorem valuationPreservingLocalizationAlgEquiv_toLocalization
    (σ : L ≃ₐ[K] L) (hσ : ∀ x : L, w.1 (σ x) = w.1 x) (x : L) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    valuationPreservingLocalizationAlgEquiv vK w σ hσ
        (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x) =
      AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 (σ x) := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  apply Subtype.ext
  exact valuationPreservingCompletionRingEquiv_toCompletion vK w σ hσ x

theorem absoluteValueDecompositionGroup_preserves_absoluteValue
    (σ : absoluteValueDecompositionGroup K w.1) (x : L) :
    w.1 ((σ : L ≃ₐ[K] L) x) = w.1 x

theorem localizationAbsoluteValue_algEquiv
    (τ :
      letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
      letI : SMul K w.1.Completion := hK.toSMul
      letI := AbsoluteValue.completionAlgebra vK w.1 w.2
      AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
        AbsoluteValue.algebraicLocalization vK w.1 w.2)
    (x :
      letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
      letI : SMul K w.1.Completion := hK.toSMul
      letI := AbsoluteValue.completionAlgebra vK w.1 w.2
      AbsoluteValue.algebraicLocalization vK w.1 w.2) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    AbsoluteValue.algebraicLocalizationAbsoluteValue vK w.1 w.2 (τ x) =
      AbsoluteValue.algebraicLocalizationAbsoluteValue vK w.1 w.2 x := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vK w.1 w.2
  let vhat := AbsoluteValue.completionAbsoluteValue vK
  let wloc := AbsoluteValue.algebraicLocalizationAbsoluteValue vK w.1 w.2
  let : Algebra.IsAlgebraic vK.Completion E :=
    AbsoluteValue.algebraicLocalization_isAlgebraic vK w.1 w.2
  let R := AbsoluteValue.uniqueAlgebraicExtension
    (K := vK.Completion) (L := E) vhat
    (AbsoluteValue.completionAbsoluteValue_complete vK)
    (AbsoluteValue.completionAbsoluteValue_isNontrivial vK hvK)
  have hwloc : wloc = R.extension := by
    apply R.unique
    intro y
    exact AbsoluteValue.algebraicLocalizationAbsoluteValue_extends vK w.1 w.2 y
  let wconj : AbsoluteValue E ℝ :=
    wloc.comp (f := τ.toRingEquiv.toRingHom) τ.injective
  have hwconj : wconj = R.extension := by
    apply R.unique
    intro y
    change wloc (τ (algebraMap vK.Completion E y)) = vhat y
    rw [τ.commutes]
    exact AbsoluteValue.algebraicLocalizationAbsoluteValue_extends vK w.1 w.2 y
  have h := congrArg (fun q : AbsoluteValue E ℝ => q x)
    (hwconj.trans hwloc.symm)
  exact h

def localizationAlgEquivRestrict
    (τ :
      letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
      letI : SMul K w.1.Completion := hK.toSMul
      letI := AbsoluteValue.completionAlgebra vK w.1 w.2
      AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
        AbsoluteValue.algebraicLocalization vK w.1 w.2) : L ≃ₐ[K] L := by
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vK w.1 w.2
  let i : L →+* E := AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
  letI : Algebra K E := (i.comp (algebraMap K L)).toAlgebra
  let iAlg : L →ₐ[K] E :=
    { __ := i
      commutes' := fun x => by
        change i (algebraMap K L x) = (i.comp (algebraMap K L)) x
        rfl }
  letI : Algebra L E := i.toAlgebra
  letI : IsScalarTower K L E :=
    IsScalarTower.of_algebraMap_eq' rfl
  let τK : E ≃ₐ[K] E :=
    { __ := τ.toRingEquiv
      commutes' := fun x => by
        change τ (i (algebraMap K L x)) = i (algebraMap K L x)
        rw [AbsoluteValue.toAlgebraicLocalization_algebraMap, τ.commutes] }
  exact Normal.algHomEquivAut K E L (τK.toAlgHom.comp iAlg)

theorem localizationAlgEquivRestrict_toLocalization
    (τ :
      letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
      letI : SMul K w.1.Completion := hK.toSMul
      letI := AbsoluteValue.completionAlgebra vK w.1 w.2
      AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
        AbsoluteValue.algebraicLocalization vK w.1 w.2)
    (x : L) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
        (localizationAlgEquivRestrict vK w τ x) =
      τ (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x) := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  let E := AbsoluteValue.algebraicLocalization vK w.1 w.2
  let i : L →+* E := AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
  let : Algebra K E := (i.comp (algebraMap K L)).toAlgebra
  let iAlg : L →ₐ[K] E :=
    { __ := i
      commutes' := fun x => by
        change i (algebraMap K L x) = (i.comp (algebraMap K L)) x
        rfl }
  let : Algebra L E := i.toAlgebra
  let : IsScalarTower K L E :=
    IsScalarTower.of_algebraMap_eq' rfl
  let τK : E ≃ₐ[K] E :=
    { __ := τ.toRingEquiv
      commutes' := fun y => by
        change τ (i (algebraMap K L y)) = i (algebraMap K L y)
        rw [AbsoluteValue.toAlgebraicLocalization_algebraMap, τ.commutes] }
  change i (Normal.algHomEquivAut K E L (τK.toAlgHom.comp iAlg) x) =
    τ (i x)
  simpa [iAlg, τK, AlgHom.restrictNormal', RingHom.algebraMap_toAlgebra] using
    ((τK.toAlgHom.comp iAlg).restrictNormal_commutes L x)

def localizationToDecompositionGroup
    (τ :
      letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
      letI : SMul K w.1.Completion := hK.toSMul
      letI := AbsoluteValue.completionAlgebra vK w.1 w.2
      AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
        AbsoluteValue.algebraicLocalization vK w.1 w.2) :
    absoluteValueDecompositionGroup K w.1 := by
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  let σ := localizationAlgEquivRestrict vK w τ
  refine ⟨σ, ?_⟩
  intro x
  have habs : w.1 (σ x) = w.1 x := by
    calc
      w.1 (σ x) = AbsoluteValue.algebraicLocalizationAbsoluteValue vK w.1 w.2
          (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 (σ x)) :=
        (AbsoluteValue.algebraicLocalizationAbsoluteValue_toAlgebraicLocalization vK w.1 w.2 (σ
          x)).symm
      _ = AbsoluteValue.algebraicLocalizationAbsoluteValue vK w.1 w.2
          (τ (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x)) := by
        rw [localizationAlgEquivRestrict_toLocalization]
      _ = AbsoluteValue.algebraicLocalizationAbsoluteValue vK w.1 w.2
          (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x) :=
        localizationAbsoluteValue_algEquiv vK hvK w τ _
      _ = w.1 x :=
        AbsoluteValue.algebraicLocalizationAbsoluteValue_toAlgebraicLocalization vK w.1 w.2 x
  rw [habs]

def decompositionGroupToLocalization
    (σ : absoluteValueDecompositionGroup K w.1) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
      AbsoluteValue.algebraicLocalization vK w.1 w.2 :=
  valuationPreservingLocalizationAlgEquiv vK w (σ : L ≃ₐ[K] L)
    (absoluteValueDecompositionGroup_preserves_absoluteValue vK hvK w σ)

theorem decompositionGroupToLocalization_toLocalization
    (σ : absoluteValueDecompositionGroup K w.1) (x : L) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    decompositionGroupToLocalization vK hvK w σ
        (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x) =
      AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 ((σ : L ≃ₐ[K] L) x) :=
  valuationPreservingLocalizationAlgEquiv_toLocalization vK w
    (σ : L ≃ₐ[K] L)
    (absoluteValueDecompositionGroup_preserves_absoluteValue vK hvK w σ) x

theorem localizationToDecompositionGroup_decompositionGroupToLocalization
    (σ : absoluteValueDecompositionGroup K w.1) :
    localizationToDecompositionGroup vK hvK w
        (decompositionGroupToLocalization vK hvK w σ) = σ

theorem decompositionGroupToLocalization_localizationToDecompositionGroup
    (τ :
      letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
      letI : SMul K w.1.Completion := hK.toSMul
      letI := AbsoluteValue.completionAlgebra vK w.1 w.2
      AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
        AbsoluteValue.algebraicLocalization vK w.1 w.2) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    decompositionGroupToLocalization vK hvK w
        (localizationToDecompositionGroup vK hvK w τ) = τ := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  let i := AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
  let ρ := decompositionGroupToLocalization vK hvK w
    (localizationToDecompositionGroup vK hvK w τ)
  have hρ : ρ.toAlgHom = τ.toAlgHom := by
    apply IntermediateField.adjoin_algHom_ext
    intro z hz
    rcases hz with ⟨x, rfl⟩
    change ρ (i x) = τ (i x)
    rw [decompositionGroupToLocalization_toLocalization]
    change i (localizationAlgEquivRestrict vK w τ x) = τ (i x)
    exact localizationAlgEquivRestrict_toLocalization vK w τ x
  exact AlgEquiv.ext fun x => DFunLike.congr_fun hρ x

theorem decompositionGroupToLocalization_mul
    (σ τ : absoluteValueDecompositionGroup K w.1) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    decompositionGroupToLocalization vK hvK w (σ * τ) =
      decompositionGroupToLocalization vK hvK w σ *
        decompositionGroupToLocalization vK hvK w τ := by
  let hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  let : SMul K w.1.Completion := hK.toSMul
  let := AbsoluteValue.completionAlgebra vK w.1 w.2
  let i := AbsoluteValue.toAlgebraicLocalization vK w.1 w.2
  let ρL := decompositionGroupToLocalization vK hvK w (σ * τ)
  let ρR := decompositionGroupToLocalization vK hvK w σ *
    decompositionGroupToLocalization vK hvK w τ
  have hρ : ρL.toAlgHom = ρR.toAlgHom := by
    apply IntermediateField.adjoin_algHom_ext
    intro z hz
    rcases hz with ⟨x, rfl⟩
    change ρL (i x) = ρR (i x)
    calc
      ρL (i x) = i (((σ * τ : absoluteValueDecompositionGroup K w.1) :
          L ≃ₐ[K] L) x) :=
        decompositionGroupToLocalization_toLocalization vK hvK w (σ * τ) x
      _ = i ((σ : L ≃ₐ[K] L) ((τ : L ≃ₐ[K] L) x)) := rfl
      _ = decompositionGroupToLocalization vK hvK w σ
          (i ((τ : L ≃ₐ[K] L) x)) :=
        (decompositionGroupToLocalization_toLocalization
          vK hvK w σ ((τ : L ≃ₐ[K] L) x)).symm
      _ = decompositionGroupToLocalization vK hvK w σ
          (decompositionGroupToLocalization vK hvK w τ (i x)) := by
        exact congrArg (decompositionGroupToLocalization vK hvK w σ)
          (decompositionGroupToLocalization_toLocalization
            vK hvK w τ x).symm
      _ = ρR (i x) := rfl
  exact AlgEquiv.ext fun x => DFunLike.congr_fun hρ x

def decompositionGroupEquivAlgebraicLocalizationAut :
    absoluteValueDecompositionGroup K w.1 ≃*
      (letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
       letI : SMul K w.1.Completion := hK.toSMul
       letI := AbsoluteValue.completionAlgebra vK w.1 w.2
       AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
         AbsoluteValue.algebraicLocalization vK w.1 w.2) where
  toFun := decompositionGroupToLocalization vK hvK w
  invFun := localizationToDecompositionGroup vK hvK w
  left_inv := localizationToDecompositionGroup_decompositionGroupToLocalization
    vK hvK w
  right_inv :=
    decompositionGroupToLocalization_localizationToDecompositionGroup vK hvK w
  map_mul' := decompositionGroupToLocalization_mul vK hvK w

theorem localizationRamificationGroups_decompositionGroupEquiv_apply
    (σ : absoluteValueDecompositionGroup K w.1) :
    decompositionGroupEquivAlgebraicLocalizationAut vK hvK w σ =
      decompositionGroupToLocalization vK hvK w σ

theorem localizationRamificationGroups_decompositionGroupEquiv_symm_apply
    (τ :
      letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
      letI : SMul K w.1.Completion := hK.toSMul
      letI := AbsoluteValue.completionAlgebra vK w.1 w.2
      AbsoluteValue.algebraicLocalization vK w.1 w.2 ≃ₐ[vK.Completion]
        AbsoluteValue.algebraicLocalization vK w.1 w.2) :
    (decompositionGroupEquivAlgebraicLocalizationAut vK hvK w).symm τ =
      localizationToDecompositionGroup vK hvK w τ :=
  rfl

theorem localizationRamificationGroups_decompositionGroupEquiv_toLocalization
    (σ : absoluteValueDecompositionGroup K w.1) (x : L) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    decompositionGroupEquivAlgebraicLocalizationAut vK hvK w σ
        (AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 x) =
      AbsoluteValue.toAlgebraicLocalization vK w.1 w.2 ((σ : L ≃ₐ[K] L) x) :=
  decompositionGroupToLocalization_toLocalization vK hvK w σ x