Neukirch–Uchida theorem

neukirch_uchida

Submitter: Junyan Xu.

Notes: Unavailable.

Source: Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1.

Informal solution: Unavailable.

theorem declaration uses `sorry`neukirch_uchida {K₁ K₂ K₁' K₂' : Type*} [Field K₁] [Field K₂] [Field K₁'] [Field K₂']
    [NumberField K₁] [NumberField K₂] [Algebra K₁ K₁'] [Algebra K₂ K₂'] [IsSepClosure K₁ K₁']
    [IsSepClosure K₂ K₂'] (ϕ : Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)) (he : IsHomeomorph ϕ) :
    ∃! σ : K₂' ≃+* K₁', (algebraMap K₂ K₂').range.map σ.toRingHom = (algebraMap K₁ K₁').range ∧
      ∀ g : Gal(K₁'/K₁), ϕ g = σ.trans (g.toRingEquiv.trans σ.symm) := byK₁:Type u_1K₂:Type u_2K₁':Type u_3K₂':Type u_4inst✝⁹:Field K₁inst✝⁸:Field K₂inst✝⁷:Field K₁'inst✝⁶:Field K₂'inst✝⁵:NumberField K₁inst✝⁴:NumberField K₂inst✝³:Algebra K₁ K₁'inst✝²:Algebra K₂ K₂'inst✝¹:IsSepClosure K₁ K₁'inst✝:IsSepClosure K₂ K₂'ϕ:Gal(K₁'/K₁) ≃* Gal(K₂'/K₂)he:IsHomeomorph ⇑ϕ⊢ ∃! σ,
  Subring.map σ.toRingHom (algebraMap K₂ K₂').range = (algebraMap K₁ K₁').range ∧
    ∀ (g : Gal(K₁'/K₁)), (ϕ g).toRingEquiv = σ.trans (g.toRingEquiv.trans σ.symm)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.