DecompositionField.lean

abbrev absoluteValueDecompositionField (w : AbsoluteValue L ℝ) :
    IntermediateField K L

theorem mem_absoluteValueDecompositionField_iff
    (w : AbsoluteValue L ℝ) (x : L) :
    x ∈ absoluteValueDecompositionField K w ↔
      ∀ σ ∈ absoluteValueDecompositionGroup K w, σ x = x

theorem absoluteValueDecompositionGroup_isClosed
    [Algebra.IsAlgebraic K L] (w : AbsoluteValue L ℝ) :
    IsClosed (absoluteValueDecompositionGroup K w : Set (L ≃ₐ[K] L)) where
  isOpen_compl := isOpen_iff_mem_nhds.mpr fun σ hσ => by
    rw [Set.mem_compl_iff, SetLike.mem_coe,
      mem_absoluteValueDecompositionGroup_iff] at hσ
    rcases Classical.not_forall.mp hσ with ⟨x, hx⟩
    let E : IntermediateField K L := IntermediateField.adjoin K {x}
    let : FiniteDimensional K E :=
      IntermediateField.adjoin.finiteDimensional
        (Algebra.IsIntegral.isIntegral x)
    apply mem_nhds_iff.mpr
    refine ⟨σ • (E.fixingSubgroup : Set (L ≃ₐ[K] L)), ?_, ?_, ?_⟩
    · intro τ hτ
      rcases Set.mem_smul_set.mp hτ with ⟨g, hg, rfl⟩
      rw [Set.mem_compl_iff, SetLike.mem_coe,
        mem_absoluteValueDecompositionGroup_iff]
      intro hmem
      apply hx
      have hgx : g x = x :=
        (IntermediateField.mem_fixingSubgroup_iff E g).mp hg x
          (IntermediateField.subset_adjoin (F := K) (S := {x}) (by simp))
      simpa [AlgEquiv.mul_apply, hgx] using hmem x
    · exact E.fixingSubgroup_isOpen.smul σ
    · exact ⟨1, E.fixingSubgroup.one_mem, by simp⟩

theorem absoluteValueDecompositionField_fixingSubgroup_eq
    [IsGalois K L] (w : AbsoluteValue L ℝ) :
    (absoluteValueDecompositionField K w).fixingSubgroup =
      absoluteValueDecompositionGroup K w