HenselianAlgebraicRamificationRestriction.lean

theorem restrictNormal_ramification_mono
    (A : _root_.ValuationSubring L)
    (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)
    (σ : L ≃ₐ[K] L)
    (hσ : AlgEquiv.restrictNormalHom (F := K) (K₁ := L) F σ ∈
      ramificationGroupInAut K (A.comap F.toIntermediateField.val.toRingHom)) :
    AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E σ ∈
      ramificationGroupInAut K (A.comap E.toIntermediateField.val.toRingHom)

theorem exists_inertia_with_finite_ramification_and_restriction
    [IsGalois K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation]
    (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p]
    (τ : ramificationGroup K (A.comap E.toIntermediateField.val.toRingHom)) :
    ∃ σ : inertiaGroup K A,
      finiteInertiaRestriction A F σ ∈
        ramificationGroup K (A.comap F.toIntermediateField.val.toRingHom) ∧
      finiteInertiaRestriction A E σ = (τ : inertiaGroup K _)

theorem galoisPullback_ramificationGroupMap_surjective_of_isGalois_henselianRing
    [IsGalois K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation]
    (E : FiniteGaloisIntermediateField K L)
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p] :
    Function.Surjective
      (_root_.HilbertRamification.ValuationSubring.galoisPullback_ramificationGroupMap
        (RingHom.id K) E.toIntermediateField.val.toRingHom
        (by
          apply RingHom.ext
          intro a
          exact E.toIntermediateField.val.commutes a) A) := by
  intro τ
  let C : FiniteGaloisIntermediateField K L → Set (L ≃ₐ[K] L) := fun F =>
    {σ | σ ∈ inertiaGroupInAut K A ∧
      AlgEquiv.restrictNormalHom (F := K) (K₁ := L) F σ ∈
        ramificationGroupInAut K (A.comap F.toIntermediateField.val.toRingHom) ∧
      AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E σ =
        inertiaGroupToAut (K := K) (A.comap E.toIntermediateField.val.toRingHom) τ}
  have hclosed (F : FiniteGaloisIntermediateField K L) : IsClosed (C F) :=
    (inertiaGroupInAut_isClosed K A).inter
      (((ramificationGroupInAut_isClosed K
        (A.comap F.toIntermediateField.val.toRingHom)).preimage
          (InfiniteGalois.restrictNormalHom_continuous F.toIntermediateField)).inter
        (isClosed_eq
          (InfiniteGalois.restrictNormalHom_continuous E.toIntermediateField) continuous_const))
  have hnonempty (F : FiniteGaloisIntermediateField K L) : (C F).Nonempty := by
    obtain ⟨σ, hσR, hσE⟩ :=
      exists_inertia_with_finite_ramification_and_restriction V A E (F ⊔ E) le_sup_right p τ
    refine ⟨inertiaGroupToAut (K := K) A σ, ?_, ?_, ?_⟩
    · exact ⟨(σ : decompositionGroup K A), σ.property, rfl⟩
    · apply restrictNormal_ramification_mono A F (F ⊔ E) le_sup_left
      rw [← finiteInertiaRestriction_coe]
      exact ⟨finiteInertiaRestriction A (F ⊔ E) σ, hσR, rfl⟩
    · rw [← finiteInertiaRestriction_coe, hσE]
  have hdir : Directed (· ⊇ ·) C := by
    intro F₁ F₂
    refine ⟨F₁ ⊔ F₂, ?_, ?_⟩
    · intro σ hσ
      exact ⟨hσ.1,
        restrictNormal_ramification_mono A F₁ (F₁ ⊔ F₂) le_sup_left σ hσ.2.1, hσ.2.2⟩
    · intro σ hσ
      exact ⟨hσ.1,
        restrictNormal_ramification_mono A F₂ (F₁ ⊔ F₂) le_sup_right σ hσ.2.1, hσ.2.2⟩
  obtain ⟨σ, hσ⟩ :=
    IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed C hdir hnonempty
      (fun F => (hclosed F).isCompact) hclosed
  have hσF (F : FiniteGaloisIntermediateField K L) := Set.mem_iInter.mp hσ F
  obtain ⟨δ, hδ, hδσ⟩ := (hσF E).1
  let s : inertiaGroup K A := ⟨δ, hδ⟩
  have hsσ : inertiaGroupToAut (K := K) A s = σ := hδσ
  have hsR : s ∈ ramificationGroup K A :=
    (mem_ramificationGroup_iff_forall_finiteGalois_restrict K A s).mpr fun F => by
      rw [hsσ]
      exact (hσF F).2.1
  refine ⟨⟨s, hsR⟩, ?_⟩
  apply Subtype.ext
  apply Subtype.ext
  apply Subtype.ext
  change inertiaGroupToAut (K := K) (A.comap E.toIntermediateField.val.toRingHom)
      (finiteInertiaRestriction A E s) =
    inertiaGroupToAut (K := K) (A.comap E.toIntermediateField.val.toRingHom) τ
  rw [finiteInertiaRestriction_coe, hsσ]
  exact (hσF E).2.2