ExtensionFactorClassification.lean

abbrev completionExtensionFactor_completionPolynomial
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) (f : K[X]) :
    vK.Completion[X]

abbrev CompletionExtensionFactorCompletionFactors
    {K : Type u} [Field K] (vK : AbsoluteValue K ℝ) (f : K[X])

theorem completionExtensionFactor_root_isIntegral
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0) : IsIntegral K α

theorem completionExtensionFactor_definingPolynomial_associated_minpoly
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0) :
    Associated f (minpoly K α)

theorem completionExtensionFactor_completionFactors_eq_minpolyFactors
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0) :
    polynomialDistinctNormalizedFactors
        (completionExtensionFactor_completionPolynomial vK f) =
      polynomialDistinctNormalizedFactors
        ((minpoly K α).map (algebraMap K vK.Completion))

def completionExtensionFactor_minpolyFactorsEquivCompletionFactors
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0) :
    DistinctNormalizedFactors
        ((minpoly K α).map (algebraMap K vK.Completion)) ≃
      CompletionExtensionFactorCompletionFactors vK f

abbrev CompletionExtensionFactorEmbeddingSetoid
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    Setoid (L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK)

def completionExtensionFactor_embeddingClassesEquivMinpolyFactors
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    Quotient (CompletionExtensionFactorEmbeddingSetoid vK α hα hgen) ≃
      DistinctNormalizedFactors
        ((minpoly K α).map (algebraMap K vK.Completion))

theorem completionExtensionFactor_embeddingSetoid_rel_iff_conjugate
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (τ τ' : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK) :
    (CompletionExtensionFactorEmbeddingSetoid vK α hα hgen).r τ τ' ↔
      AbsoluteValueExtensionConjugateOverCompletion vK τ τ'

def pullbackAbsoluteValueExtension
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (τ : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK) :
    AbsoluteValueExtension vK L

theorem completionExtensionFactor_pullback_eq_iff_embeddingSetoid_rel
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (τ τ' : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK) :
    absoluteValueExtension_pullback vK hvK τ =
        absoluteValueExtension_pullback vK hvK τ' ↔
      (CompletionExtensionFactorEmbeddingSetoid vK α hα hgen).r τ τ'

theorem completionExtensionFactor_extension_eq_pullback_embeddingOfExtension
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L) :
    w.1 = absoluteValueExtension_pullback vK hvK
      (absoluteValueExtension_embeddingOfExtension vK w)

def completionExtensionFactor_extensionsEquivEmbeddingClasses
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    AbsoluteValueExtension vK L ≃
      Quotient (CompletionExtensionFactorEmbeddingSetoid vK α hα hgen)

def completionExtensionFactor_extensionsEquivMinpolyFactors
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    AbsoluteValueExtension vK L ≃
      DistinctNormalizedFactors
        ((minpoly K α).map (algebraMap K vK.Completion))

def completionExtensionFactor_extensionsEquivCompletionFactorsAux
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    AbsoluteValueExtension vK L ≃
      CompletionExtensionFactorCompletionFactors vK f

def completionExtensionFactor_extensionFactor
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (α : L)
    (w : AbsoluteValueExtension vK L) : vK.Completion[X]

theorem completionExtensionFactor_extensionFactor_mem
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0)
    (w : AbsoluteValueExtension vK L) :
    completionExtensionFactor_extensionFactor vK α w ∈
      polynomialDistinctNormalizedFactors
        (completionExtensionFactor_completionPolynomial vK f)

def completionExtensionFactor_extensionToFactor
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0) :
    AbsoluteValueExtension vK L →
      CompletionExtensionFactorCompletionFactors vK f

theorem completionExtensionFactor_embeddingOfExtension_minpoly
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [Algebra.IsAlgebraic K L]
    (vK : AbsoluteValue K ℝ) (α : L)
    (w : AbsoluteValueExtension vK L) :
    minpoly vK.Completion
        (absoluteValueExtension_embeddingOfExtension vK w α) =
      completionExtensionFactor_extensionFactor vK α w

theorem completionExtensionFactor_completion_adjoin_eq_top
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK 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
    Algebra.adjoin vK.Completion
        ({AbsoluteValue.toCompletionAlgHom (K := K) w.1 α} :
          Set w.1.Completion) = ⊤ := by
  let pb : PowerBasis K L := PowerBasis.ofAdjoinEqTop hα hgen
  let : FiniteDimensional K L := pb.finite
  let : Algebra.IsAlgebraic K L := inferInstance
  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 : IsScalarTower K vK.Completion w.1.Completion :=
    AbsoluteValue.completion_isScalarTower vK w.1 w.2
  let ι : L →ₐ[K] w.1.Completion :=
    AbsoluteValue.toCompletionAlgHom (K := K) w.1
  let a : w.1.Completion := ι α
  have haK : IsIntegral K a := by
      exact IsIntegral.map_of_comp_eq (RingHom.id K) ι.toRingHom
        (by ext x; simp) hα
  have haKv : IsIntegral vK.Completion a :=
    IsIntegral.tower_top haK
  have hrange : Set.range
      (AbsoluteValue.toCompletion w.1) ⊆
      (IntermediateField.adjoin vK.Completion ({a} : Set w.1.Completion) :
        Set w.1.Completion) := by
    rintro _ ⟨x, rfl⟩
    change ι x ∈ IntermediateField.adjoin vK.Completion ({a} : Set _)
    have hx : x ∈ Algebra.adjoin K ({α} : Set L) := by
      rw [hgen]
      trivial
    induction hx using Algebra.adjoin_induction with
    | mem x hx =>
        rw [Set.mem_singleton_iff.mp hx]
        exact IntermediateField.mem_adjoin_simple_self vK.Completion a
    | algebraMap x =>
        rw [ι.commutes,
          IsScalarTower.algebraMap_apply K vK.Completion w.1.Completion]
        exact (IntermediateField.adjoin vK.Completion ({a} : Set _)).algebraMap_mem _
    | add x y _ _ hx hy =>
        simpa only [map_add] using
          (IntermediateField.adjoin vK.Completion ({a} : Set _)).add_mem hx hy
    | mul x y _ _ hx hy =>
        simpa only [map_mul] using
          (IntermediateField.adjoin vK.Completion ({a} : Set _)).mul_mem hx hy
  have hloc_le : AbsoluteValue.algebraicLocalization vK w.1 w.2 ≤
      IntermediateField.adjoin vK.Completion ({a} : Set _) := by
    exact IntermediateField.adjoin_le_iff.mpr hrange
  have hsimple : IntermediateField.adjoin vK.Completion ({a} : Set _) = ⊤ := by
    apply top_unique
    rw [← absoluteValueExtension_finiteLocalization_eq_top vK hvK w]
    exact hloc_le
  rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
      haKv.isAlgebraic,
    hsimple, IntermediateField.top_toSubalgebra]

def completionExtensionFactor_adjoinRootEquivCompletion
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK 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
    AdjoinRoot (completionExtensionFactor_extensionFactor vK α w) ≃ₐ[vK.Completion]
      w.1.Completion := 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
  letI : IsScalarTower K vK.Completion w.1.Completion :=
    AbsoluteValue.completion_isScalarTower vK w.1 w.2
  let ι : L →ₐ[K] w.1.Completion :=
    AbsoluteValue.toCompletionAlgHom (K := K) w.1
  let a : w.1.Completion := ι α
  have haK : IsIntegral K a := by
      exact IsIntegral.map_of_comp_eq (RingHom.id K) ι.toRingHom
        (by ext x; simp) hα
  have haKv : IsIntegral vK.Completion a :=
    IsIntegral.tower_top haK
  have htop : Algebra.adjoin vK.Completion ({a} : Set w.1.Completion) = ⊤ :=
    completionExtensionFactor_completion_adjoin_eq_top
      vK hvK α hα hgen w
  change AdjoinRoot (minpoly vK.Completion a) ≃ₐ[vK.Completion]
    w.1.Completion
  exact (@minpoly.equivAdjoin vK.Completion w.1.Completion _ _ _ _ _ _
    (Module.isTorsionFree_iff_algebraMap_injective.mpr
      (algebraMap vK.Completion w.1.Completion).injective) a haKv).trans
    ((Subalgebra.equivOfEq _ _ htop).trans Subalgebra.topEquiv)

theorem completionExtensionFactor_adjoinRootEquivCompletion_root
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK 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
    completionExtensionFactor_adjoinRootEquivCompletion vK hvK α hα hgen w
        (AdjoinRoot.root (completionExtensionFactor_extensionFactor vK α w)) =
      AbsoluteValue.toCompletionAlgHom (K := K) w.1 α := 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 : IsScalarTower K vK.Completion w.1.Completion :=
    AbsoluteValue.completion_isScalarTower vK w.1 w.2
  let ι : L →ₐ[K] w.1.Completion :=
    AbsoluteValue.toCompletionAlgHom (K := K) w.1
  let a : w.1.Completion := ι α
  change ((AdjoinRoot.Minpoly.toAdjoin vK.Completion a)
      (AdjoinRoot.root (minpoly vK.Completion a)) : w.1.Completion) = a
  exact AdjoinRoot.Minpoly.coe_toAdjoin_mk_X
    (R := vK.Completion) (x := a)

theorem completionExtensionFactor_extensionFactor_eq_minpoly_of_pullback
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK L)
    (τ : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK)
    (hτ : w.1 = absoluteValueExtension_pullback vK hvK τ) :
    completionExtensionFactor_extensionFactor vK α w =
      minpoly vK.Completion (τ α)

def completionExtensionFactor_completionEquivSimpleRoot
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK L)
    (τ : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK)
    (hτ : w.1 = absoluteValueExtension_pullback vK hvK τ) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    w.1.Completion ≃ₐ[vK.Completion]
      IntermediateField.adjoin vK.Completion
        ({τ α} : Set (absoluteValueExtension_algebraicCompletionClosure vK)) := 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
  letI : IsScalarTower K vK.Completion w.1.Completion :=
    AbsoluteValue.completion_isScalarTower vK w.1 w.2
  have hfactor : completionExtensionFactor_extensionFactor vK α w =
      minpoly vK.Completion (τ α) :=
    completionExtensionFactor_extensionFactor_eq_minpoly_of_pullback
      vK hvK α hα hgen w τ hτ
  have hτα : IsIntegral vK.Completion (τ α) :=
    (Algebra.IsAlgebraic.isAlgebraic (τ α)).isIntegral
  exact (completionExtensionFactor_adjoinRootEquivCompletion
      vK hvK α hα hgen w).symm |>.trans
    ((AdjoinRoot.algEquivOfEq vK.Completion _ _ hfactor).trans
      (IntermediateField.adjoinRootEquivAdjoin vK.Completion hτα))

theorem completionExtensionFactor_completionEquivSimpleRoot_gen
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK L)
    (τ : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK)
    (hτ : w.1 = absoluteValueExtension_pullback vK hvK τ) :
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    completionExtensionFactor_completionEquivSimpleRoot
        vK hvK α hα hgen w τ hτ
        (AbsoluteValue.toCompletionAlgHom (K := K) w.1 α) =
      IntermediateField.AdjoinSimple.gen vK.Completion (τ α) := 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 : IsScalarTower K vK.Completion w.1.Completion :=
    AbsoluteValue.completion_isScalarTower vK w.1 w.2
  let e0 := completionExtensionFactor_adjoinRootEquivCompletion
    vK hvK α hα hgen w
  let hfactor : completionExtensionFactor_extensionFactor vK α w =
      minpoly vK.Completion (τ α) :=
    completionExtensionFactor_extensionFactor_eq_minpoly_of_pullback
      vK hvK α hα hgen w τ hτ
  let e1 := AdjoinRoot.algEquivOfEq vK.Completion _ _ hfactor
  have hτα : IsIntegral vK.Completion (τ α) :=
    (Algebra.IsAlgebraic.isAlgebraic (τ α)).isIntegral
  let e2 := IntermediateField.adjoinRootEquivAdjoin vK.Completion hτα
  have hinv : e0.symm
      (AbsoluteValue.toCompletionAlgHom (K := K) w.1 α) =
      AdjoinRoot.root (completionExtensionFactor_extensionFactor vK α w) := by
    apply e0.injective
    rw [e0.apply_symm_apply,
      completionExtensionFactor_adjoinRootEquivCompletion_root]
  change (e0.symm.trans (e1.trans e2))
      (AbsoluteValue.toCompletionAlgHom (K := K) w.1 α) = _
  rw [AlgEquiv.trans_apply, hinv, AlgEquiv.trans_apply,
    AdjoinRoot.algEquivOfEq_root,
    IntermediateField.adjoinRootEquivAdjoin_apply_root]

theorem completionExtensionFactor_completionEquivSimpleRoot_coe
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (α : L) (hα : IsIntegral K α)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK L)
    (τ : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK)
    (hτ : w.1 = absoluteValueExtension_pullback vK hvK τ)
    (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
    ((completionExtensionFactor_completionEquivSimpleRoot
        vK hvK α hα hgen w τ hτ
        (AbsoluteValue.toCompletionAlgHom (K := K) w.1 x) :
      IntermediateField.adjoin vK.Completion
        ({τ α} : Set (absoluteValueExtension_algebraicCompletionClosure vK))) :
      absoluteValueExtension_algebraicCompletionClosure vK) = τ x := by
  let pb : PowerBasis K L := PowerBasis.ofAdjoinEqTop hα hgen
  let : FiniteDimensional K L := pb.finite
  let : Algebra.IsAlgebraic K L := inferInstance
  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 : IsScalarTower K vK.Completion w.1.Completion :=
    AbsoluteValue.completion_isScalarTower vK w.1 w.2
  let E := IntermediateField.adjoin vK.Completion
    ({τ α} : Set (absoluteValueExtension_algebraicCompletionClosure vK))
  let e : w.1.Completion ≃ₐ[vK.Completion] E :=
    completionExtensionFactor_completionEquivSimpleRoot
      vK hvK α hα hgen w τ hτ
  let ι : L →ₐ[K] w.1.Completion :=
    AbsoluteValue.toCompletionAlgHom (K := K) w.1
  let φ : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK :=
    ((E.val.comp e.toAlgHom).restrictScalars K).comp ι
  have hpbgen : pb.gen = α := by simp [pb]
  have hφ : φ = τ := by
    apply pb.algHom_ext
    rw [hpbgen]
    change ((e (ι α) : E) :
      absoluteValueExtension_algebraicCompletionClosure vK) = τ α
    rw [completionExtensionFactor_completionEquivSimpleRoot_gen]
    rfl
  exact DFunLike.congr_fun hφ x

theorem completionExtensionFactor_extensionsEquivCompletionFactorsAux_apply
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (w : AbsoluteValueExtension vK L) :
    (completionExtensionFactor_extensionsEquivCompletionFactorsAux
        vK hvK hf hroot hgen w).1 =
      completionExtensionFactor_extensionFactor vK α w

def completionExtensionFactor_extensionEquivFactors
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    AbsoluteValueExtension vK L ≃
      CompletionExtensionFactorCompletionFactors vK f

theorem completionExtensionFactor_factor_irreducible_monic_dvd_minpoly
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0)
    (g : CompletionExtensionFactorCompletionFactors vK f) :
    Irreducible g.1 ∧ g.1.Monic ∧
      g.1 ∣ (minpoly K α).map (algebraMap K vK.Completion)

theorem completionExtensionFactor_factorRoot_mem_mappedMinpoly
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    β ∈ ((minpoly K α).map (algebraMap K vK.Completion)).rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)

def completionExtensionFactor_embeddingOfFactorRoot
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK

theorem completionExtensionFactor_embeddingOfFactorRoot_apply
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    completionExtensionFactor_embeddingOfFactorRoot
      vK hf hroot hgen g β hβ α = β

def completionExtensionFactor_extensionOfFactorRoot
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    AbsoluteValueExtension vK L

theorem completionExtensionFactor_extensionOfFactorRoot_eq_pullback
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    (completionExtensionFactor_extensionOfFactorRoot
        vK hvK hf hroot hgen g β hβ).1 =
      absoluteValueExtension_pullback vK hvK
        (completionExtensionFactor_embeddingOfFactorRoot
          vK hf hroot hgen g β hβ)

theorem completionExtensionFactor_extensionOfFactorRoot_factor
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    completionExtensionFactor_extensionFactor vK α
        (completionExtensionFactor_extensionOfFactorRoot
          vK hvK hf hroot hgen g β hβ) = g.1

theorem completionExtensionFactor_extensionOfFactorRoot_eq_equiv_symm
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    completionExtensionFactor_extensionOfFactorRoot
        vK hvK hf hroot hgen g β hβ =
      (completionExtensionFactor_extensionEquivFactors
        vK hvK hf hroot hgen).symm g

theorem completionExtensionFactor_factor_eq_minpoly_root
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) {α : L} {f : K[X]}
    (hf : Irreducible f) (hroot : Polynomial.aeval α f = 0)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    g.1 = minpoly vK.Completion β

def completionExtensionFactor_factorRootCompletionEquiv
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    let w := completionExtensionFactor_extensionOfFactorRoot
      vK hvK hf hroot hgen g β hβ
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    w.1.Completion ≃ₐ[vK.Completion]
      IntermediateField.adjoin vK.Completion
        ({β} : Set (absoluteValueExtension_algebraicCompletionClosure vK)) := by
  let hα := completionExtensionFactor_root_isIntegral hf hroot
  let w := completionExtensionFactor_extensionOfFactorRoot
    vK hvK hf hroot hgen g β hβ
  letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
  letI : SMul K w.1.Completion := hK.toSMul
  letI := AbsoluteValue.completionAlgebra vK w.1 w.2
  have hfactor : completionExtensionFactor_extensionFactor vK α w = g.1 :=
    completionExtensionFactor_extensionOfFactorRoot_factor
      vK hvK hf hroot hgen g β hβ
  have hmp : g.1 = minpoly vK.Completion β :=
    completionExtensionFactor_factor_eq_minpoly_root vK hf hroot g β hβ
  have hβint : IsIntegral vK.Completion β :=
    (Algebra.IsAlgebraic.isAlgebraic β).isIntegral
  exact (completionExtensionFactor_adjoinRootEquivCompletion
      vK hvK α hα hgen w).symm |>.trans
    ((AdjoinRoot.algEquivOfEq vK.Completion _ _ (hfactor.trans hmp)).trans
      (IntermediateField.adjoinRootEquivAdjoin vK.Completion hβint))

theorem completionExtensionFactor_factorRootCompletionEquiv_gen
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK)) :
    let w := completionExtensionFactor_extensionOfFactorRoot
      vK hvK hf hroot hgen g β hβ
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    completionExtensionFactor_factorRootCompletionEquiv
        vK hvK hf hroot hgen g β hβ
        (AbsoluteValue.toCompletionAlgHom (K := K) w.1 α) =
      IntermediateField.AdjoinSimple.gen vK.Completion β := by
  let hα := completionExtensionFactor_root_isIntegral hf hroot
  let w := completionExtensionFactor_extensionOfFactorRoot
    vK hvK hf hroot hgen g β hβ
  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 e0 := completionExtensionFactor_adjoinRootEquivCompletion
    vK hvK α hα hgen w
  let hpoly : completionExtensionFactor_extensionFactor vK α w =
      minpoly vK.Completion β :=
    (completionExtensionFactor_extensionOfFactorRoot_factor
      vK hvK hf hroot hgen g β hβ).trans
      (completionExtensionFactor_factor_eq_minpoly_root vK hf hroot g β hβ)
  let e1 := AdjoinRoot.algEquivOfEq vK.Completion _ _ hpoly
  have hβint : IsIntegral vK.Completion β :=
    (Algebra.IsAlgebraic.isAlgebraic β).isIntegral
  let e2 := IntermediateField.adjoinRootEquivAdjoin vK.Completion hβint
  have hinv : e0.symm
      (AbsoluteValue.toCompletionAlgHom (K := K) w.1 α) =
      AdjoinRoot.root (completionExtensionFactor_extensionFactor vK α w) := by
    apply e0.injective
    rw [e0.apply_symm_apply,
      completionExtensionFactor_adjoinRootEquivCompletion_root]
  change (e0.symm.trans (e1.trans e2))
      (AbsoluteValue.toCompletionAlgHom (K := K) w.1 α) = _
  rw [AlgEquiv.trans_apply, hinv, AlgEquiv.trans_apply,
    AdjoinRoot.algEquivOfEq_root,
    IntermediateField.adjoinRootEquivAdjoin_apply_root]

theorem completionExtensionFactor_factorRootCompletionEquiv_coe
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤)
    (g : CompletionExtensionFactorCompletionFactors vK f)
    (β : absoluteValueExtension_algebraicCompletionClosure vK)
    (hβ : β ∈ g.1.rootSet
      (absoluteValueExtension_algebraicCompletionClosure vK))
    (x : L) :
    let τ := completionExtensionFactor_embeddingOfFactorRoot
      vK hf hroot hgen g β hβ
    let w := completionExtensionFactor_extensionOfFactorRoot
      vK hvK hf hroot hgen g β hβ
    letI hK := AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
    letI : SMul K w.1.Completion := hK.toSMul
    letI := AbsoluteValue.completionAlgebra vK w.1 w.2
    ((completionExtensionFactor_factorRootCompletionEquiv
        vK hvK hf hroot hgen g β hβ
        (AbsoluteValue.toCompletionAlgHom (K := K) w.1 x) :
      IntermediateField.adjoin vK.Completion
        ({β} : Set (absoluteValueExtension_algebraicCompletionClosure vK))) :
      absoluteValueExtension_algebraicCompletionClosure vK) = τ x := by
  let hα := completionExtensionFactor_root_isIntegral hf hroot
  let pb : PowerBasis K L := PowerBasis.ofAdjoinEqTop hα hgen
  let : FiniteDimensional K L := pb.finite
  let : Algebra.IsAlgebraic K L := inferInstance
  let τ := completionExtensionFactor_embeddingOfFactorRoot
    vK hf hroot hgen g β hβ
  let w := completionExtensionFactor_extensionOfFactorRoot
    vK hvK hf hroot hgen g β hβ
  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 : IsScalarTower K vK.Completion w.1.Completion :=
    AbsoluteValue.completion_isScalarTower vK w.1 w.2
  let E := IntermediateField.adjoin vK.Completion
    ({β} : Set (absoluteValueExtension_algebraicCompletionClosure vK))
  let e : w.1.Completion ≃ₐ[vK.Completion] E :=
    completionExtensionFactor_factorRootCompletionEquiv
      vK hvK hf hroot hgen g β hβ
  let ι : L →ₐ[K] w.1.Completion :=
    AbsoluteValue.toCompletionAlgHom (K := K) w.1
  let φ : L →ₐ[K] absoluteValueExtension_algebraicCompletionClosure vK :=
    ((E.val.comp e.toAlgHom).restrictScalars K).comp ι
  have hpbgen : pb.gen = α := by simp [pb]
  have hφ : φ = τ := by
    apply pb.algHom_ext
    rw [hpbgen]
    change ((e (ι α) : E) :
      absoluteValueExtension_algebraicCompletionClosure vK) = τ α
    rw [completionExtensionFactor_factorRootCompletionEquiv_gen,
      completionExtensionFactor_embeddingOfFactorRoot_apply]
    rfl
  exact DFunLike.congr_fun hφ x

theorem completionExtensionFactor_classification
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    {α : L} {f : K[X]} (hf : Irreducible f)
    (hroot : Polynomial.aeval α f = 0)
    (hgen : Algebra.adjoin K ({α} : Set L) = ⊤) :
    Function.Bijective (completionExtensionFactor_extensionToFactor vK hf hroot) ∧
      ∀ (g : CompletionExtensionFactorCompletionFactors vK f)
        (β : absoluteValueExtension_algebraicCompletionClosure vK)
        (hβ : β ∈ g.1.rootSet
          (absoluteValueExtension_algebraicCompletionClosure vK)),
        let τ := completionExtensionFactor_embeddingOfFactorRoot
          vK hf hroot hgen g β hβ
        let w := completionExtensionFactor_extensionOfFactorRoot
          vK hvK hf hroot hgen g β hβ
        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 := completionExtensionFactor_factorRootCompletionEquiv
          vK hvK hf hroot hgen g β hβ
        τ α = β ∧
          w.1 = absoluteValueExtension_pullback vK hvK τ ∧
          w = (completionExtensionFactor_extensionEquivFactors
            vK hvK hf hroot hgen).symm g ∧
          completionExtensionFactor_extensionFactor vK α w = g.1 ∧
          ∀ x : L,
            ((e (AbsoluteValue.toCompletionAlgHom (K := K) w.1 x) :
              IntermediateField.adjoin vK.Completion
                ({β} : Set
                  (absoluteValueExtension_algebraicCompletionClosure vK))) :
              absoluteValueExtension_algebraicCompletionClosure vK) = τ x := by
  constructor
  · exact (completionExtensionFactor_extensionEquivFactors
      vK hvK hf hroot hgen).bijective
  · intro g β hβ
    dsimp only
    refine ⟨completionExtensionFactor_embeddingOfFactorRoot_apply
        vK hf hroot hgen g β hβ,
      completionExtensionFactor_extensionOfFactorRoot_eq_pullback
        vK hvK hf hroot hgen g β hβ,
      completionExtensionFactor_extensionOfFactorRoot_eq_equiv_symm
        vK hvK hf hroot hgen g β hβ,
      completionExtensionFactor_extensionOfFactorRoot_factor
        vK hvK hf hroot hgen g β hβ, ?_⟩
    intro x
    exact completionExtensionFactor_factorRootCompletionEquiv_coe
      vK hvK hf hroot hgen g β hβ x