Generator.lean

def localizedCompletionDecompositionGroupFintype
    (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L) :
    Fintype (absoluteValueDecompositionGroup K w.1)

def localizedCompletionGaloisGenerator
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L)
    (hgen : ∀ τ : L ≃ₐ[K] L,
      τ ∈ Subgroup.zpowers σ) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    LocalizedCompletion vK w ≃ₐ[vK.Completion]
      LocalizedCompletion vK w :=
  (decompositionGroupEquivAlgebraicLocalizationAut
    vK hvK w)
      (subgroupGeneratorOfGenerator
        (absoluteValueDecompositionGroup K w.1) σ hgen)

theorem localizedCompletionGaloisGenerator_generates
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L)
    (hgen : ∀ τ : L ≃ₐ[K] L,
      τ ∈ Subgroup.zpowers σ) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI : Algebra vK.Completion w.1.Completion :=
      AbsoluteValue.completionAlgebra vK w.1 w.2
    ∀ τ : LocalizedCompletion vK w ≃ₐ[vK.Completion]
        LocalizedCompletion vK w,
      τ ∈ Subgroup.zpowers
        (localizedCompletionGaloisGenerator
          vK hvK w σ hgen) := by
  let := localizedCompletionBaseAlgebra vK w
  let H := absoluteValueDecompositionGroup K w.1
  let e :=
    decompositionGroupEquivAlgebraicLocalizationAut
      vK hvK w
  let δ :=
    subgroupGeneratorOfGenerator H σ hgen
  intro τ
  rw [show localizedCompletionGaloisGenerator
      vK hvK w σ hgen = e δ from rfl]
  change τ ∈ Subgroup.zpowers (e.toMonoidHom δ)
  rw [← MonoidHom.map_zpowers e.toMonoidHom δ]
  refine ⟨e.symm τ, ?_, e.apply_symm_apply τ⟩
  exact subgroupGeneratorOfGenerator_generates
    H σ hgen (e.symm τ)